:: by Edmund Woronowicz

::

:: Received April 14, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

registration

let X, Y be set ;

cluster -> Relation-like Element of bool [:X,Y:];

coherence

for b_{1} being Subset of [:X,Y:] holds b_{1} is Relation-like
;

end;
cluster -> Relation-like Element of bool [:X,Y:];

coherence

for b

registration

let X, Y be set ;

cluster -> X -defined Y -valued Element of bool [:X,Y:];

coherence

for b_{1} being Relation of X,Y holds

( b_{1} is X -defined & b_{1} is Y -valued )

end;
cluster -> X -defined Y -valued Element of bool [:X,Y:];

coherence

for b

( b

proof end;

theorem :: RELSET_1:1

canceled;

theorem :: RELSET_1:2

canceled;

theorem :: RELSET_1:3

canceled;

definition

canceled;

let X, Y be set ;

let R be Relation of X,Y;

let Z be set ;

:: original: c=

redefine pred R c= Z means :: RELSET_1:def 2

for x being Element of X

for y being Element of Y st [x,y] in R holds

[x,y] in Z;

compatibility

( R c= Z iff for x being Element of X

for y being Element of Y st [x,y] in R holds

[x,y] in Z )

end;
let X, Y be set ;

let R be Relation of X,Y;

let Z be set ;

:: original: c=

redefine pred R c= Z means :: RELSET_1:def 2

for x being Element of X

for y being Element of Y st [x,y] in R holds

[x,y] in Z;

compatibility

( R c= Z iff for x being Element of X

for y being Element of Y st [x,y] in R holds

[x,y] in Z )

proof end;

:: deftheorem RELSET_1:def 1 :

canceled;

:: deftheorem defines c= RELSET_1:def 2 :

for X, Y being set

for R being Relation of X,Y

for Z being set holds

( R c= Z iff for x being Element of X

for y being Element of Y st [x,y] in R holds

[x,y] in Z );

definition

let X, Y be set ;

let P, R be Relation of X,Y;

:: original: =

redefine pred P = R means :: RELSET_1:def 3

for x being Element of X

for y being Element of Y holds

( [x,y] in P iff [x,y] in R );

compatibility

( P = R iff for x being Element of X

for y being Element of Y holds

( [x,y] in P iff [x,y] in R ) )

end;
let P, R be Relation of X,Y;

:: original: =

redefine pred P = R means :: RELSET_1:def 3

for x being Element of X

for y being Element of Y holds

( [x,y] in P iff [x,y] in R );

compatibility

( P = R iff for x being Element of X

for y being Element of Y holds

( [x,y] in P iff [x,y] in R ) )

proof end;

:: deftheorem defines = RELSET_1:def 3 :

for X, Y being set

for P, R being Relation of X,Y holds

( P = R iff for x being Element of X

for y being Element of Y holds

( [x,y] in P iff [x,y] in R ) );

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 by XBOOLE_1:1;

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

A is Relation of X,Y by XBOOLE_1:1;

theorem :: RELSET_1:5

canceled;

theorem :: RELSET_1:6

for a, X, Y 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 )

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

proof end;

theorem :: RELSET_1:9

canceled;

theorem :: RELSET_1:10

canceled;

theorem :: RELSET_1:11

proof end;

theorem :: RELSET_1:12

canceled;

theorem :: RELSET_1:13

proof end;

theorem :: RELSET_1:14

proof end;

theorem :: RELSET_1:15

canceled;

theorem :: RELSET_1:16

canceled;

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

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

R is Relation of X1,Y1

proof end;

registration

let X be set ;

let R, S be X -defined Relation;

cluster R \/ S -> X -defined ;

coherence

R \/ S is X -defined

end;
let R, S be X -defined Relation;

cluster R \/ S -> X -defined ;

coherence

R \/ S is X -defined

proof end;

registration

let X be set ;

let R be X -defined Relation;

let S be Relation;

cluster R /\ S -> X -defined ;

coherence

R /\ S is X -defined

coherence

R \ S is X -defined ;

end;
let R be X -defined Relation;

let S be Relation;

cluster R /\ S -> X -defined ;

coherence

R /\ S is X -defined

proof end;

cluster R \ S -> X -defined ;coherence

R \ S is X -defined ;

registration

let X be set ;

let R, S be X -valued Relation;

cluster R \/ S -> X -valued ;

coherence

R \/ S is X -valued

end;
let R, S be X -valued Relation;

cluster R \/ S -> X -valued ;

coherence

R \/ S is X -valued

proof end;

registration

let X be set ;

let R be X -valued Relation;

let S be Relation;

cluster R /\ S -> X -valued ;

coherence

R /\ S is X -valued

coherence

R \ S is X -valued ;

end;
let R be X -valued Relation;

let S be Relation;

cluster R /\ S -> X -valued ;

coherence

R /\ S is X -valued

proof end;

cluster R \ S -> X -valued ;coherence

R \ S is X -valued ;

definition

let X, Y be set ;

let R be Relation of X,Y;

:: original: proj1

redefine func dom R -> Subset of X;

coherence

proj1 R is Subset of X by RELAT_1:def 18;

:: original: proj2

redefine func rng R -> Subset of Y;

coherence

proj2 R is Subset of Y by RELAT_1:def 19;

end;
let R be Relation of X,Y;

:: original: proj1

redefine func dom R -> Subset of X;

coherence

proj1 R is Subset of X by RELAT_1:def 18;

:: original: proj2

redefine func rng R -> Subset of Y;

coherence

proj2 R is Subset of Y by RELAT_1:def 19;

theorem :: RELSET_1:18

canceled;

theorem :: RELSET_1:19

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 )

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 )

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

R ~ is Relation of Y,X

end;
let R be Relation of X,Y;

:: original: ~

redefine func R ~ -> Relation of Y,X;

coherence

R ~ is Relation of Y,X

proof 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

P * R is Relation of X,Z

end;
let P be Relation of X,Y1;

let R be Relation of Y2,Z;

:: original: *

redefine func P * R -> Relation of X,Z;

coherence

P * R is Relation of X,Z

proof end;

theorem :: RELSET_1:24

proof end;

theorem :: RELSET_1:25

registration

let A be empty set ;

let B be set ;

cluster -> empty Element of bool [:A,B:];

coherence

for b_{1} being Relation of A,B holds b_{1} is empty

coherence

for b_{1} being Relation of B,A holds b_{1} is empty

end;
let B be set ;

cluster -> empty Element of bool [:A,B:];

coherence

for b

proof end;

cluster -> empty Element of bool [:B,A:];coherence

for b

proof end;

theorem :: RELSET_1:26

canceled;

theorem :: RELSET_1:27

canceled;

theorem Th28: :: RELSET_1:28

proof end;

theorem :: RELSET_1:29

theorem Th30: :: RELSET_1:30

proof end;

theorem :: RELSET_1:31

proof end;

theorem :: RELSET_1:32

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

R | A is Relation of X,Y

end;
let R be Relation of X,Y;

let A be set ;

:: original: |

redefine func R | A -> Relation of X,Y;

coherence

R | A is Relation of X,Y

proof 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

B | R is Relation of X,Y

end;
let R be Relation of X,Y;

:: original: |

redefine func B | R -> Relation of X,Y;

coherence

B | R is Relation of X,Y

proof end;

theorem :: RELSET_1:33

proof end;

theorem :: RELSET_1:34

proof end;

theorem :: RELSET_1:35

proof end;

theorem :: RELSET_1:36

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

R .: A is Subset of Y

redefine func R " A -> Subset of X;

coherence

R " A is Subset of X

end;
let R be Relation of X,Y;

let A be set ;

:: original: .:

redefine func R .: A -> Subset of Y;

coherence

R .: A is Subset of Y

proof end;

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

coherence

R " A is Subset of X

proof end;

theorem :: RELSET_1:37

canceled;

theorem Th38: :: RELSET_1:38

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 )

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_{1}() -> set , F_{2}() -> set , P_{1}[ set , set ] } :

RelOnSetEx{ F

ex R being Relation of F_{1}(),F_{2}() st

for x, y being set holds

( [x,y] in R iff ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] ) )

for x, y being set holds

( [x,y] in R iff ( x in F

proof end;

registration
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

canceled;

theorem :: RELSET_1:46

canceled;

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 )

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 set holds

( y in rng R iff ex x being Element of D st [x,y] in R )

for R being Relation of D,E

for y being set 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 st dom R <> {} holds

ex y being Element of E st y in rng R

for R being Relation of D,E st 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 st rng R <> {} holds

ex x being Element of D st x in dom R

for R being Relation of D,E st 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, z being set holds

( [x,z] in P * R iff ex y being Element of E st

( [x,y] in P & [y,z] in R ) )

for P being Relation of D,E

for R being Relation of E,F

for x, z being set 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 ) )

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 ) )

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_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set , set ] } :

RelOnDomEx{ F

ex R being Relation of F_{1}(),F_{2}() st

for x being Element of F_{1}()

for y being Element of F_{2}() holds

( [x,y] in R iff P_{1}[x,y] )

for x being Element of F

for y being Element of F

( [x,y] in R iff P

proof end;

begin

scheme :: RELSET_1:sch 3

Sch3{ F_{1}() -> set , F_{2}() -> Subset of F_{1}(), F_{3}( set ) -> set } :

Sch3{ F

ex R being Relation of F_{2}() st

for i being Element of F_{1}() st i in F_{2}() holds

Im (R,i) = F_{3}(i)

provided
for i being Element of F

Im (R,i) = F

proof end;

theorem :: RELSET_1:54

for N being set

for R, S being Relation of N st ( for i being set st i in N holds

Im (R,i) = Im (S,i) ) holds

R = S

for R, S being Relation of N st ( for i being set st i in N holds

Im (R,i) = Im (S,i) ) holds

R = S

proof end;

scheme :: RELSET_1:sch 4

Sch4{ F_{1}() -> set , F_{2}() -> set , P_{1}[ set , set ], F_{3}() -> Relation of F_{1}(),F_{2}(), F_{4}() -> Relation of F_{1}(),F_{2}() } :

provided

Sch4{ F

provided

A1:
for p being Element of F_{1}()

for q being Element of F_{2}() holds

( [p,q] in F_{3}() iff P_{1}[p,q] )
and

A2: for p being Element of F_{1}()

for q being Element of F_{2}() holds

( [p,q] in F_{4}() iff P_{1}[p,q] )

for q being Element of F

( [p,q] in F

A2: for p being Element of F

for q being Element of F

( [p,q] in F

proof end;

registration

let X, Y, Z be set ;

let f be Relation of [:X,Y:],Z;

cluster proj1 f -> Relation-like ;

coherence

dom f is Relation-like ;

end;
let f be Relation of [:X,Y:],Z;

cluster proj1 f -> Relation-like ;

coherence

dom f is Relation-like ;

registration

let X, Y, Z be set ;

let f be Relation of X,[:Y,Z:];

cluster proj2 f -> Relation-like ;

coherence

rng f is Relation-like ;

end;
let f be Relation of X,[:Y,Z:];

cluster proj2 f -> Relation-like ;

coherence

rng f is Relation-like ;

theorem :: RELSET_1:55

proof end;

registration

let R be non empty Relation;

let Y be non empty Subset of (dom R);

cluster R | Y -> non empty ;

coherence

not R | Y is empty

end;
let Y be non empty Subset of (dom R);

cluster R | Y -> non empty ;

coherence

not R | Y is empty

proof end;

registration

let R be non empty Relation;

let Y be non empty Subset of (dom R);

cluster R .: Y -> non empty ;

coherence

not R .: Y is empty

end;
let Y be non empty Subset of (dom R);

cluster R .: Y -> non empty ;

coherence

not R .: Y is empty

proof end;

registration

let X, Y be set ;

cluster empty Relation-like X -defined Y -valued Element of bool [:X,Y:];

existence

ex b_{1} being Relation of X,Y st b_{1} is empty

end;
cluster empty Relation-like X -defined Y -valued Element of bool [:X,Y:];

existence

ex b

proof end;