:: RELSET_1 semantic presentation

definition

let X, Y be set ;
mode Relation of X,Y -> set means :Def1: :: RELSET_1:def 1
it c= [:X,Y:];
existence ;

end;

:: deftheorem Def1 defines Relation RELSET_1:def 1 :

definition

let X, Y be set ;
:: original: Relation
redefine mode Relation of X,Y -> Subset of [:X,Y:];
coherence by Def1;

end;

registration

let X, Y be set ;
cluster -> Relation-like Element of bool [:X,Y:];
coherence

proof end;

end;

theorem :: RELSET_1:1

canceled;

theorem :: RELSET_1:2

canceled;

theorem :: RELSET_1:3

canceled;

theorem :: RELSET_1:4

for A, X, Y being set
for R being Relation of X,Y st A c= R holds
A is Relation of X,Y

proof end;

theorem :: RELSET_1:5

canceled;

theorem :: RELSET_1:6

for X, Y, a being set
for R being Relation of X,Y st a in R holds
ex x, y being set st
( a = [x,y] & x in X & y in Y )

proof end;

theorem :: RELSET_1:7

canceled;

theorem :: RELSET_1:8

for X, Y, x, y being set st x in X & y in Y holds
{[x,y]} is Relation of X,Y

proof end;

theorem :: RELSET_1:9

for X being set
for R being Relation st dom R c= X holds
R is Relation of X, rng R

proof end;

theorem :: RELSET_1:10

for Y being set
for R being Relation st rng R c= Y holds
R is Relation of dom R,Y

proof end;

theorem :: RELSET_1:11

for X, Y being set
for R being Relation st dom R c= X & rng R c= Y holds
R is Relation of X,Y

proof end;

theorem Th12: :: RELSET_1:12

for X, Y being set
for R being Relation of X,Y holds
( dom R c= X & rng R c= Y )

proof end;

theorem Th13: :: RELSET_1:13

for X, X1, Y being set
for R being Relation of X,Y st dom R c= X1 holds
R is Relation of X1,Y

proof end;

theorem Th14: :: RELSET_1:14

for Y, Y1, X being set
for R being Relation of X,Y st rng R c= Y1 holds
R is Relation of X,Y1

proof end;

theorem :: RELSET_1:15

for X, X1, Y being set
for R being Relation of X,Y st X c= X1 holds
R is Relation of X1,Y

proof end;

theorem :: RELSET_1:16

for Y, Y1, X being set
for R being Relation of X,Y st Y c= Y1 holds
R is Relation of X,Y1

proof end;

theorem :: RELSET_1:17

for X, X1, Y, Y1 being set
for R being Relation of X,Y st X c= X1 & Y c= Y1 holds
R is Relation of X1,Y1

proof end;

definition

let X, Y be set ;
let P, R be Relation of X,Y;
:: original: \/
redefine func P \/ R -> Relation of X,Y;
coherence

proof end;

:: original: /\
redefine func P /\ R -> Relation of X,Y;
coherence

proof end;

:: original: \
redefine func P \ R -> Relation of X,Y;
coherence

proof end;

end;

definition

let X, Y be set ;
let R be Relation of X,Y;
:: original: dom
redefine func dom R -> Subset of X;
coherence by Th12;
:: original: rng
redefine func rng R -> Subset of Y;
coherence by Th12;

end;

theorem :: RELSET_1:18

canceled;

theorem :: RELSET_1:19

for X, Y being set
for R being Relation of X,Y holds field R c= X \/ Y

proof end;

theorem :: RELSET_1:20

canceled;

theorem :: RELSET_1:21

canceled;

theorem :: RELSET_1:22

for Y, X being set
for R being Relation of X,Y holds
( ( for x being set st x in X holds
ex y being set st [x,y] in R ) iff dom R = X )

proof end;

theorem :: RELSET_1:23

for X, Y being set
for R being Relation of X,Y holds
( ( for y being set st y in Y holds
ex x being set st [x,y] in R ) iff rng R = Y )

proof end;

definition

let X, Y be set ;
let R be Relation of X,Y;
:: original: ~
redefine func R ~ -> Relation of Y,X;
coherence

proof end;

end;

definition

let X, Y1, Y2, Z be set ;
let P be Relation of X,Y1;
let R be Relation of Y2,Z;
:: original: *
redefine func P * R -> Relation of X,Z;
coherence

proof end;

end;

theorem :: RELSET_1:24

for X, Y being set
for R being Relation of X,Y holds
( dom (R ~ ) = rng R & rng (R ~ ) = dom R )

proof end;

theorem :: RELSET_1:25

for X, Y being set holds {} is Relation of X,Y

proof end;

theorem :: RELSET_1:26

for X, Y being set
for R being Relation of X,Y st R is Relation of {} ,Y holds
R = {}

proof end;

theorem :: RELSET_1:27

for Y, X being set
for R being Relation of X,Y st R is Relation of X, {} holds
R = {}

proof end;

theorem Th28: :: RELSET_1:28

for X being set holds id X c= [:X,X:]

proof end;

theorem :: RELSET_1:29

for X being set holds id X is Relation of X,X

proof end;

theorem Th30: :: RELSET_1:30

for X, Y, A being set
for R being Relation of X,Y st id A c= R holds
( A c= dom R & A c= rng R )

proof end;

theorem :: RELSET_1:31

for Y, X being set
for R being Relation of X,Y st id X c= R holds
( X = dom R & X c= rng R )

proof end;

theorem :: RELSET_1:32

for X, Y being set
for R being Relation of X,Y st id Y c= R holds
( Y c= dom R & Y = rng R )

proof end;

definition

let X, Y be set ;
let R be Relation of X,Y;
let A be set ;
:: original: |
redefine func R | A -> Relation of X,Y;
coherence

proof end;

end;

definition

let X, Y, B be set ;
let R be Relation of X,Y;
:: original: |
redefine func B | R -> Relation of X,Y;
coherence

proof end;

end;

theorem :: RELSET_1:33

for X, X1, Y being set
for R being Relation of X,Y holds R | X1 is Relation of X1,Y

proof end;

theorem :: RELSET_1:34

for Y, X, X1 being set
for R being Relation of X,Y st X c= X1 holds
R | X1 = R

proof end;

theorem :: RELSET_1:35

for Y, Y1, X being set
for R being Relation of X,Y holds Y1 | R is Relation of X,Y1

proof end;

theorem :: RELSET_1:36

for X, Y, Y1 being set
for R being Relation of X,Y st Y c= Y1 holds
Y1 | R = R

proof end;

definition

let X, Y be set ;
let R be Relation of X,Y;
let A be set ;
:: original: .:
redefine func R .: A -> Subset of Y;
coherence

proof end;

:: original: "
redefine func R " A -> Subset of X;
coherence

proof end;

end;

theorem :: RELSET_1:37

canceled;

theorem Th38: :: RELSET_1:38

for X, Y being set
for R being Relation of X,Y holds
( R .: X = rng R & R " Y = dom R )

proof end;

theorem :: RELSET_1:39

for Y, X being set
for R being Relation of X,Y holds
( R .: (R " Y) = rng R & R " (R .: X) = dom R )

proof end;

scheme :: RELSET_1:sch 1
RelOnSetEx{ F₁() -> set , F₂() -> set , P₁[ set , set ] } :

ex R being Relation of F₁(),F₂() st
for x, y being set holds
( [x,y] in R iff ( x in F₁() & y in F₂() & P₁[x,y] ) )

proof end;

definition

let X be set ;
mode Relation of X is Relation of X,X;

end;

theorem :: RELSET_1:40

canceled;

theorem :: RELSET_1:41

canceled;

theorem :: RELSET_1:42

canceled;

theorem :: RELSET_1:43

canceled;

theorem :: RELSET_1:44

canceled;

theorem :: RELSET_1:45

for X being set
for R being Relation of X holds
( R * (id X) = R & (id X) * R = R )

proof end;

theorem :: RELSET_1:46

for D being non empty set holds id D <> {}

proof end;

theorem :: RELSET_1:47

for D, E being non empty set
for R being Relation of D,E
for x being Element of D holds
( x in dom R iff ex y being Element of E st [x,y] in R )

proof end;

theorem :: RELSET_1:48

for E, D being non empty set
for R being Relation of D,E
for y being Element of E holds
( y in rng R iff ex x being Element of D st [x,y] in R )

proof end;

theorem :: RELSET_1:49

for D, E being non empty set
for R being Relation of D,E
for x being Element of D st x in dom R holds
ex y being Element of E st y in rng R

proof end;

theorem :: RELSET_1:50

for E, D being non empty set
for R being Relation of D,E
for y being Element of E st y in rng R holds
ex x being Element of D st x in dom R

proof end;

theorem :: RELSET_1:51

for D, E, F being non empty set
for P being Relation of D,E
for R being Relation of E,F
for x being Element of D
for z being Element of F holds
( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )

proof end;

theorem :: RELSET_1:52

for E, D1, D being non empty set
for R being Relation of D,E
for y being Element of E holds
( y in R .: D1 iff ex x being Element of D st
( [x,y] in R & x in D1 ) )

proof end;

theorem :: RELSET_1:53

for D, D2, E being non empty set
for R being Relation of D,E
for x being Element of D holds
( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )

proof end;

scheme :: RELSET_1:sch 2
RelOnDomEx{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ] } :

ex R being Relation of F₁(),F₂() st
for x being Element of F₁()
for y being Element of F₂() holds
( [x,y] in R iff P₁[x,y] )

proof end;