:: Relations and Their Basic Properties
:: by Edmund Woronowicz
::
:: Received March 15, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users


begin

definition
let IT be set ;
attr IT is Relation-like means :Def1: :: RELAT_1:def 1
 for x being set st x in IT holds
ex y, z being set st x = [y,z];
end;

:: deftheorem Def1 defines Relation-like RELAT_1:def 1 :
for IT being set holds
( IT is Relation-like iff for x being set st x in IT holds
ex y, z being set st x = [y,z] );

registration
cluster empty -> Relation-like set ;
coherence
for b1 being set st b1 is empty holds
b1 is Relation-like
proof end;
end;

definition
mode Relation is Relation-like set ;
end;

theorem :: RELAT_1:1
canceled;

theorem :: RELAT_1:2
canceled;

registration
let R be Relation;
cluster -> Relation-like Element of bool R;
coherence
for b1 being Subset of R holds b1 is Relation-like
proof end;
end;

scheme :: RELAT_1:sch 1
RelExistence{ F1() -> set , F2() -> set , P1[ set , set ] } :
ex R being Relation st
for x, y being set holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) )
proof end;

Lm1: for x, y, X being set st [x,y] in X holds
( x in union (union X) & y in union (union X) )
proof end;

definition
let P, R be Relation;
redefine pred P = R means :: RELAT_1:def 2
 for a, b being set holds
( [a,b] in P iff [a,b] in R );
compatibility
( P = R iff for a, b being set holds
( [a,b] in P iff [a,b] in R ) )
proof end;
end;

:: deftheorem defines = RELAT_1:def 2 :
for P, R being Relation holds
( P = R iff for a, b being set holds
( [a,b] in P iff [a,b] in R ) );

registration
let P be Relation;
let X be set ;
cluster P /\ X -> Relation-like ;
coherence
P /\ X is Relation-like
proof end;
cluster P \ X -> Relation-like ;
coherence
P \ X is Relation-like ;
end;

registration
let P, R be Relation;
cluster P \/ R -> Relation-like ;
coherence
P \/ R is Relation-like
proof end;
end;

registration
let R, S be Relation;
cluster R \+\ S -> Relation-like ;
coherence
R \+\ S is Relation-like ;
end;

registration
let a, b be set ;
cluster {[a,b]} -> Relation-like ;
coherence
{[a,b]} is Relation-like
proof end;
cluster [:a,b:] -> Relation-like ;
coherence
[:a,b:] is Relation-like
proof end;
end;

registration
let a, b, c, d be set ;
cluster {[a,b],[c,d]} -> Relation-like ;
coherence
{[a,b],[c,d]} is Relation-like
proof end;
end;

theorem :: RELAT_1:3
canceled;

theorem :: RELAT_1:4
canceled;

theorem :: RELAT_1:5
canceled;

theorem :: RELAT_1:6
canceled;

definition
let P be Relation;
let A be set ;
redefine pred P c= A means :: RELAT_1:def 3
 for a, b being set st [a,b] in P holds
[a,b] in A;
compatibility
( P c= A iff for a, b being set st [a,b] in P holds
[a,b] in A )
proof end;
end;

:: deftheorem defines c= RELAT_1:def 3 :
for P being Relation
for A being set holds
( P c= A iff for a, b being set st [a,b] in P holds
[a,b] in A );

definition
let R be set ;
func proj1 R -> set means :Def4: :: RELAT_1:def 4
 for x being set holds
( x in it iff ex y being set st [x,y] in R );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex y being set st [x,y] in R )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y being set st [x,y] in R ) ) & ( for x being set holds
( x in b2 iff ex y being set st [x,y] in R ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines proj1 RELAT_1:def 4 :
for R, b2 being set holds
( b2 = proj1 R iff for x being set holds
( x in b2 iff ex y being set st [x,y] in R ) );

notation
let R be Relation;
synonym dom R for proj1 R;
end;

theorem :: RELAT_1:7
canceled;

theorem :: RELAT_1:8
canceled;

theorem :: RELAT_1:9
canceled;

theorem :: RELAT_1:10
canceled;

theorem :: RELAT_1:11
canceled;

theorem :: RELAT_1:12
canceled;

theorem Th13: :: RELAT_1:13
for P, R being Relation holds dom (P \/ R) = (dom P) \/ (dom R)
proof end;

theorem Th14: :: RELAT_1:14
for P, R being Relation holds dom (P /\ R) c= (dom P) /\ (dom R)
proof end;

theorem :: RELAT_1:15
for P, R being Relation holds (dom P) \ (dom R) c= dom (P \ R)
proof end;

definition
let R be set ;
func proj2 R -> set means :Def5: :: RELAT_1:def 5
 for y being set holds
( y in it iff ex x being set st [x,y] in R );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ex x being set st [x,y] in R )
proof end;
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st [x,y] in R ) ) & ( for y being set holds
( y in b2 iff ex x being set st [x,y] in R ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines proj2 RELAT_1:def 5 :
for R, b2 being set holds
( b2 = proj2 R iff for y being set holds
( y in b2 iff ex x being set st [x,y] in R ) );

notation
let R be Relation;
synonym rng R for proj2 R;
end;

theorem :: RELAT_1:16
canceled;

theorem :: RELAT_1:17
canceled;

theorem :: RELAT_1:18
for x being set
for R being Relation st x in dom R holds
ex y being set st y in rng R
proof end;

theorem :: RELAT_1:19
for y being set
for R being Relation st y in rng R holds
ex x being set st x in dom R
proof end;

theorem :: RELAT_1:20
for x, y being set
for R being Relation st [x,y] in R holds
( x in dom R & y in rng R ) by Def4, Def5;

theorem Th21: :: RELAT_1:21
for R being Relation holds R c= [:(dom R),(rng R):]
proof end;

theorem :: RELAT_1:22
for R being Relation holds R /\ [:(dom R),(rng R):] = R by Th21, XBOOLE_1:28;

theorem Th23: :: RELAT_1:23
for x, y being set
for R being Relation st R = {[x,y]} holds
( dom R = {x} & rng R = {y} )
proof end;

theorem :: RELAT_1:24
for a, b, x, y being set
for R being Relation st R = {[a,b],[x,y]} holds
( dom R = {a,x} & rng R = {b,y} )
proof end;

theorem Th25: :: RELAT_1:25
for P, R being Relation st P c= R holds
( dom P c= dom R & rng P c= rng R )
proof end;

theorem Th26: :: RELAT_1:26
for P, R being Relation holds rng (P \/ R) = (rng P) \/ (rng R)
proof end;

theorem Th27: :: RELAT_1:27
for P, R being Relation holds rng (P /\ R) c= (rng P) /\ (rng R)
proof end;

theorem :: RELAT_1:28
for P, R being Relation holds (rng P) \ (rng R) c= rng (P \ R)
proof end;

definition
let R be Relation;
func field R -> set equals :: RELAT_1:def 6
(dom R) \/ (rng R);
coherence
(dom R) \/ (rng R) is set ;
end;

:: deftheorem defines field RELAT_1:def 6 :
for R being Relation holds field R = (dom R) \/ (rng R);

theorem :: RELAT_1:29
canceled;

theorem :: RELAT_1:30
for a, b being set
for R being Relation st [a,b] in R holds
( a in field R & b in field R )
proof end;

theorem :: RELAT_1:31
for P, R being Relation st P c= R holds
field P c= field R
proof end;

theorem Th32: :: RELAT_1:32
for x, y being set holds field {[x,y]} = {x,y}
proof end;

theorem :: RELAT_1:33
for P, R being Relation holds field (P \/ R) = (field P) \/ (field R)
proof end;

theorem :: RELAT_1:34
for P, R being Relation holds field (P /\ R) c= (field P) /\ (field R)
proof end;

definition
let R be Relation;
func R ~ -> Relation means :Def7: :: RELAT_1:def 7
 for x, y being set holds
( [x,y] in it iff [y,x] in R );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff [y,x] in R )
proof end;
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff [y,x] in R ) ) & ( for x, y being set holds
( [x,y] in b2 iff [y,x] in R ) ) holds
b1 = b2
proof end;
involutiveness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff [y,x] in b2 ) ) holds
for x, y being set holds
( [x,y] in b2 iff [y,x] in b1 ) ;
end;

:: deftheorem Def7 defines ~ RELAT_1:def 7 :
for R, b2 being Relation holds
( b2 = R ~ iff for x, y being set holds
( [x,y] in b2 iff [y,x] in R ) );

theorem :: RELAT_1:35
canceled;

theorem :: RELAT_1:36
canceled;

theorem Th37: :: RELAT_1:37
for R being Relation holds
( rng R = dom (R ~) & dom R = rng (R ~) )
proof end;

theorem :: RELAT_1:38
for R being Relation holds field R = field (R ~)
proof end;

theorem :: RELAT_1:39
for P, R being Relation holds (P /\ R) ~ = (P ~) /\ (R ~)
proof end;

theorem :: RELAT_1:40
for P, R being Relation holds (P \/ R) ~ = (P ~) \/ (R ~)
proof end;

theorem :: RELAT_1:41
for P, R being Relation holds (P \ R) ~ = (P ~) \ (R ~)
proof end;

definition
let P, R be Relation;
func P * R -> Relation means :Def8: :: RELAT_1:def 8
 for x, y being set holds
( [x,y] in it iff ex z being set st
( [x,z] in P & [z,y] in R ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ex z being set st
( [x,z] in P & [z,y] in R ) )
proof end;
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines * RELAT_1:def 8 :
for P, R, b3 being Relation holds
( b3 = P * R iff for x, y being set holds
( [x,y] in b3 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) );

theorem :: RELAT_1:42
canceled;

theorem :: RELAT_1:43
canceled;

theorem Th44: :: RELAT_1:44
for P, R being Relation holds dom (P * R) c= dom P
proof end;

theorem Th45: :: RELAT_1:45
for P, R being Relation holds rng (P * R) c= rng R
proof end;

theorem :: RELAT_1:46
for R, P being Relation st rng R c= dom P holds
dom (R * P) = dom R
proof end;

theorem :: RELAT_1:47
for P, R being Relation st dom P c= rng R holds
rng (R * P) = rng P
proof end;

theorem Th48: :: RELAT_1:48
for P, R, Q being Relation st P c= R holds
Q * P c= Q * R
proof end;

theorem Th49: :: RELAT_1:49
for P, Q, R being Relation st P c= Q holds
P * R c= Q * R
proof end;

theorem :: RELAT_1:50
for P, R, Q, S being Relation st P c= R & Q c= S holds
P * Q c= R * S
proof end;

theorem :: RELAT_1:51
for P, R, Q being Relation holds P * (R \/ Q) = (P * R) \/ (P * Q)
proof end;

theorem :: RELAT_1:52
for P, R, Q being Relation holds P * (R /\ Q) c= (P * R) /\ (P * Q)
proof end;

theorem :: RELAT_1:53
for P, R, Q being Relation holds (P * R) \ (P * Q) c= P * (R \ Q)
proof end;

theorem :: RELAT_1:54
for P, R being Relation holds (P * R) ~ = (R ~) * (P ~)
proof end;

theorem Th55: :: RELAT_1:55
for P, R, Q being Relation holds (P * R) * Q = P * (R * Q)
proof end;

registration
cluster non empty Relation-like set ;
existence
not for b1 being Relation holds b1 is empty
proof end;
end;

registration
let f be non empty Relation;
cluster proj1 f -> non empty ;
coherence
not dom f is empty
proof end;
cluster proj2 f -> non empty ;
coherence
not rng f is empty
proof end;
end;

theorem Th56: :: RELAT_1:56
for R being Relation st ( for x, y being set holds not [x,y] in R ) holds
R = {}
proof end;

theorem :: RELAT_1:57
canceled;

theorem :: RELAT_1:58
canceled;

theorem :: RELAT_1:59
canceled;

theorem Th60: :: RELAT_1:60
( dom {} = {} & rng {} = {} )
proof end;

theorem :: RELAT_1:61
canceled;

theorem Th62: :: RELAT_1:62
for R being Relation holds
( {} * R = {} & R * {} = {} )
proof end;

registration
let X be empty set ;
cluster proj1 X -> empty ;
coherence
dom X is empty by Th60;
cluster proj2 X -> empty ;
coherence
rng X is empty by Th60;
let R be Relation;
cluster X * R -> empty ;
coherence
X * R is empty by Th62;
cluster R * X -> empty ;
coherence
R * X is empty by Th62;
end;

theorem :: RELAT_1:63
field {} = {} ;

theorem Th64: :: RELAT_1:64
for R being Relation st ( dom R = {} or rng R = {} ) holds
R = {} ;

theorem :: RELAT_1:65
for R being Relation holds
( dom R = {} iff rng R = {} ) by Th60, Th64;

registration
let X be empty set ;
cluster X ~ -> empty ;
coherence
X ~ is empty
proof end;
end;

theorem :: RELAT_1:66
{} ~ = {} ;

theorem :: RELAT_1:67
for R, P being Relation st rng R misses dom P holds
R * P = {}
proof end;

definition
let R be Relation;
attr R is non-empty means :Def9: :: RELAT_1:def 9
 not {} in rng R;
end;

:: deftheorem Def9 defines non-empty RELAT_1:def 9 :
for R being Relation holds
( R is non-empty iff not {} in rng R );

registration
cluster Relation-like non-empty set ;
existence
ex b1 being Relation st b1 is non-empty
proof end;
end;

registration
let R be Relation;
let S be non-empty Relation;
cluster R * S -> non-empty ;
coherence
R * S is non-empty
proof end;
end;

definition
let X be set ;
func id X -> Relation means :Def10: :: RELAT_1:def 10
 for x, y being set holds
( [x,y] in it iff ( x in X & x = y ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( x in X & x = y ) )
proof end;
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( x in X & x = y ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in X & x = y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines id RELAT_1:def 10 :
for X being set
for b2 being Relation holds
( b2 = id X iff for x, y being set holds
( [x,y] in b2 iff ( x in X & x = y ) ) );

theorem :: RELAT_1:68
canceled;

theorem :: RELAT_1:69
canceled;

theorem :: RELAT_1:70
canceled;

theorem Th71: :: RELAT_1:71
for X being set holds
( dom (id X) = X & rng (id X) = X )
proof end;

theorem :: RELAT_1:72
for X being set holds (id X) ~ = id X
proof end;

theorem :: RELAT_1:73
for X being set
for R being Relation st ( for x being set st x in X holds
[x,x] in R ) holds
id X c= R
proof end;

theorem Th74: :: RELAT_1:74
for x, y, X being set
for R being Relation holds
( [x,y] in (id X) * R iff ( x in X & [x,y] in R ) )
proof end;

theorem Th75: :: RELAT_1:75
for x, y, Y being set
for R being Relation holds
( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )
proof end;

theorem Th76: :: RELAT_1:76
for X being set
for R being Relation holds
( R * (id X) c= R & (id X) * R c= R )
proof end;

theorem Th77: :: RELAT_1:77
for X being set
for R being Relation st dom R c= X holds
(id X) * R = R
proof end;

theorem :: RELAT_1:78
for R being Relation holds (id (dom R)) * R = R by Th77;

theorem Th79: :: RELAT_1:79
for Y being set
for R being Relation st rng R c= Y holds
R * (id Y) = R
proof end;

theorem :: RELAT_1:80
for R being Relation holds R * (id (rng R)) = R by Th79;

theorem :: RELAT_1:81
id {} = {}
proof end;

theorem :: RELAT_1:82
for X being set
for P2, R, P1 being Relation st rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X holds
P1 = P2
proof end;

definition
let R be Relation;
let X be set ;
func R | X -> Relation means :Def11: :: RELAT_1:def 11
 for x, y being set holds
( [x,y] in it iff ( x in X & [x,y] in R ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( x in X & [x,y] in R ) )
proof end;
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( x in X & [x,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in X & [x,y] in R ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines | RELAT_1:def 11 :
for R being Relation
for X being set
for b3 being Relation holds
( b3 = R | X iff for x, y being set holds
( [x,y] in b3 iff ( x in X & [x,y] in R ) ) );

registration
let R be Relation;
let X be empty set ;
cluster R | X -> empty ;
coherence
R | X is empty
proof end;
end;

theorem :: RELAT_1:83
canceled;

theorem :: RELAT_1:84
canceled;

theorem :: RELAT_1:85
canceled;

theorem Th86: :: RELAT_1:86
for x, X being set
for R being Relation holds
( x in dom (R | X) iff ( x in X & x in dom R ) )
proof end;

theorem Th87: :: RELAT_1:87
for X being set
for R being Relation holds dom (R | X) c= X
proof end;

theorem Th88: :: RELAT_1:88
for X being set
for R being Relation holds R | X c= R
proof end;

theorem Th89: :: RELAT_1:89
for X being set
for R being Relation holds dom (R | X) c= dom R
proof end;

theorem Th90: :: RELAT_1:90
for X being set
for R being Relation holds dom (R | X) = (dom R) /\ X
proof end;

theorem :: RELAT_1:91
for X being set
for R being Relation st X c= dom R holds
dom (R | X) = X
proof end;

theorem :: RELAT_1:92
for X being set
for R, P being Relation holds (R | X) * P c= R * P by Th49, Th88;

theorem :: RELAT_1:93
for X being set
for P, R being Relation holds P * (R | X) c= P * R by Th48, Th88;

theorem :: RELAT_1:94
for X being set
for R being Relation holds R | X = (id X) * R
proof end;

theorem :: RELAT_1:95
for X being set
for R being Relation holds
( R | X = {} iff dom R misses X )
proof end;

theorem Th96: :: RELAT_1:96
for X being set
for R being Relation holds R | X = R /\ [:X,(rng R):]
proof end;

theorem Th97: :: RELAT_1:97
for X being set
for R being Relation st dom R c= X holds
R | X = R
proof end;

theorem :: RELAT_1:98
for R being Relation holds R | (dom R) = R by Th97;

theorem Th99: :: RELAT_1:99
for X being set
for R being Relation holds rng (R | X) c= rng R
proof end;

theorem Th100: :: RELAT_1:100
for X, Y being set
for R being Relation holds (R | X) | Y = R | (X /\ Y)
proof end;

theorem :: RELAT_1:101
for X being set
for R being Relation holds (R | X) | X = R | X
proof end;

theorem :: RELAT_1:102
for X, Y being set
for R being Relation st X c= Y holds
(R | X) | Y = R | X
proof end;

theorem :: RELAT_1:103
for Y, X being set
for R being Relation st Y c= X holds
(R | X) | Y = R | Y
proof end;

theorem Th104: :: RELAT_1:104
for X, Y being set
for R being Relation st X c= Y holds
R | X c= R | Y
proof end;

theorem Th105: :: RELAT_1:105
for X being set
for P, R being Relation st P c= R holds
P | X c= R | X
proof end;

theorem Th106: :: RELAT_1:106
for X, Y being set
for P, R being Relation st P c= R & X c= Y holds
P | X c= R | Y
proof end;

theorem Th107: :: RELAT_1:107
for X, Y being set
for R being Relation holds R | (X \/ Y) = (R | X) \/ (R | Y)
proof end;

theorem :: RELAT_1:108
for X, Y being set
for R being Relation holds R | (X /\ Y) = (R | X) /\ (R | Y)
proof end;

theorem Th109: :: RELAT_1:109
for X, Y being set
for R being Relation holds R | (X \ Y) = (R | X) \ (R | Y)
proof end;

registration
let R be empty Relation;
let X be set ;
cluster R | X -> empty ;
coherence
R | X is empty
proof end;
end;

theorem :: RELAT_1:110
for R being Relation holds R | {} = {} ;

theorem :: RELAT_1:111
for X being set holds {} | X = {} ;

theorem :: RELAT_1:112
for X being set
for P, R being Relation holds (P * R) | X = (P | X) * R
proof end;

definition
let Y be set ;
let R be Relation;
func Y | R -> Relation means :Def12: :: RELAT_1:def 12
 for x, y being set holds
( [x,y] in it iff ( y in Y & [x,y] in R ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( y in Y & [x,y] in R ) )
proof end;
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( y in Y & [x,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( y in Y & [x,y] in R ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines | RELAT_1:def 12 :
for Y being set
for R, b3 being Relation holds
( b3 = Y | R iff for x, y being set holds
( [x,y] in b3 iff ( y in Y & [x,y] in R ) ) );

registration
let R be Relation;
let X be empty set ;
cluster X | R -> empty ;
coherence
X | R is empty
proof end;
end;

theorem :: RELAT_1:113
canceled;

theorem :: RELAT_1:114
canceled;

theorem Th115: :: RELAT_1:115
for y, Y being set
for R being Relation holds
( y in rng (Y | R) iff ( y in Y & y in rng R ) )
proof end;

theorem Th116: :: RELAT_1:116
for Y being set
for R being Relation holds rng (Y | R) c= Y
proof end;

theorem Th117: :: RELAT_1:117
for Y being set
for R being Relation holds Y | R c= R
proof end;

theorem Th118: :: RELAT_1:118
for Y being set
for R being Relation holds rng (Y | R) c= rng R
proof end;

theorem Th119: :: RELAT_1:119
for Y being set
for R being Relation holds rng (Y | R) = (rng R) /\ Y
proof end;

theorem :: RELAT_1:120
for Y being set
for R being Relation st Y c= rng R holds
rng (Y | R) = Y
proof end;

theorem :: RELAT_1:121
for Y being set
for R, P being Relation holds (Y | R) * P c= R * P by Th49, Th117;

theorem :: RELAT_1:122
for Y being set
for P, R being Relation holds P * (Y | R) c= P * R by Th48, Th117;

theorem :: RELAT_1:123
for Y being set
for R being Relation holds Y | R = R * (id Y)
proof end;

theorem Th124: :: RELAT_1:124
for Y being set
for R being Relation holds Y | R = R /\ [:(dom R),Y:]
proof end;

theorem Th125: :: RELAT_1:125
for Y being set
for R being Relation st rng R c= Y holds
Y | R = R
proof end;

theorem :: RELAT_1:126
for R being Relation holds (rng R) | R = R by Th125;

theorem Th127: :: RELAT_1:127
for Y, X being set
for R being Relation holds Y | (X | R) = (Y /\ X) | R
proof end;

theorem :: RELAT_1:128
for Y being set
for R being Relation holds Y | (Y | R) = Y | R
proof end;

theorem :: RELAT_1:129
for X, Y being set
for R being Relation st X c= Y holds
Y | (X | R) = X | R
proof end;

theorem :: RELAT_1:130
for Y, X being set
for R being Relation st Y c= X holds
Y | (X | R) = Y | R
proof end;

theorem Th131: :: RELAT_1:131
for X, Y being set
for R being Relation st X c= Y holds
X | R c= Y | R
proof end;

theorem Th132: :: RELAT_1:132
for Y being set
for P1, P2 being Relation st P1 c= P2 holds
Y | P1 c= Y | P2
proof end;

theorem :: RELAT_1:133
for Y1, Y2 being set
for P1, P2 being Relation st P1 c= P2 & Y1 c= Y2 holds
Y1 | P1 c= Y2 | P2
proof end;

theorem :: RELAT_1:134
for X, Y being set
for R being Relation holds (X \/ Y) | R = (X | R) \/ (Y | R)
proof end;

theorem :: RELAT_1:135
for X, Y being set
for R being Relation holds (X /\ Y) | R = (X | R) /\ (Y | R)
proof end;

theorem :: RELAT_1:136
for X, Y being set
for R being Relation holds (X \ Y) | R = (X | R) \ (Y | R)
proof end;

theorem :: RELAT_1:137
for R being Relation holds {} | R = {} ;

theorem :: RELAT_1:138
for Y being set holds Y | {} = {}
proof end;

theorem :: RELAT_1:139
for Y being set
for P, R being Relation holds Y | (P * R) = P * (Y | R)
proof end;

theorem :: RELAT_1:140
for Y, X being set
for R being Relation holds (Y | R) | X = Y | (R | X)
proof end;

definition
let R be Relation;
let X be set ;
func R .: X -> set means :Def13: :: RELAT_1:def 13
 for y being set holds
( y in it iff ex x being set st
( [x,y] in R & x in X ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ex x being set st
( [x,y] in R & x in X ) )
proof end;
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st
( [x,y] in R & x in X ) ) ) & ( for y being set holds
( y in b2 iff ex x being set st
( [x,y] in R & x in X ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines .: RELAT_1:def 13 :
for R being Relation
for X, b3 being set holds
( b3 = R .: X iff for y being set holds
( y in b3 iff ex x being set st
( [x,y] in R & x in X ) ) );

theorem :: RELAT_1:141
canceled;

theorem :: RELAT_1:142
canceled;

theorem Th143: :: RELAT_1:143
for y, X being set
for R being Relation holds
( y in R .: X iff ex x being set st
( x in dom R & [x,y] in R & x in X ) )
proof end;

theorem Th144: :: RELAT_1:144
for X being set
for R being Relation holds R .: X c= rng R
proof end;

theorem :: RELAT_1:145
for X being set
for R being Relation holds R .: X = R .: ((dom R) /\ X)
proof end;

theorem Th146: :: RELAT_1:146
for R being Relation holds R .: (dom R) = rng R
proof end;

theorem :: RELAT_1:147
for X being set
for R being Relation holds R .: X c= R .: (dom R)
proof end;

theorem :: RELAT_1:148
for X being set
for R being Relation holds rng (R | X) = R .: X
proof end;

theorem :: RELAT_1:149
for R being Relation holds R .: {} = {}
proof end;

theorem :: RELAT_1:150
for X being set holds {} .: X = {}
proof end;

theorem :: RELAT_1:151
for X being set
for R being Relation holds
( R .: X = {} iff dom R misses X )
proof end;

theorem :: RELAT_1:152
for X being set
for R being Relation st X <> {} & X c= dom R holds
R .: X <> {}
proof end;

theorem :: RELAT_1:153
for X, Y being set
for R being Relation holds R .: (X \/ Y) = (R .: X) \/ (R .: Y)
proof end;

theorem :: RELAT_1:154
for X, Y being set
for R being Relation holds R .: (X /\ Y) c= (R .: X) /\ (R .: Y)
proof end;

theorem :: RELAT_1:155
for X, Y being set
for R being Relation holds (R .: X) \ (R .: Y) c= R .: (X \ Y)
proof end;

theorem Th156: :: RELAT_1:156
for X, Y being set
for R being Relation st X c= Y holds
R .: X c= R .: Y
proof end;

theorem Th157: :: RELAT_1:157
for X being set
for P, R being Relation st P c= R holds
P .: X c= R .: X
proof end;

theorem :: RELAT_1:158
for X, Y being set
for P, R being Relation st P c= R & X c= Y holds
P .: X c= R .: Y
proof end;

theorem :: RELAT_1:159
for X being set
for P, R being Relation holds (P * R) .: X = R .: (P .: X)
proof end;

theorem Th160: :: RELAT_1:160
for P, R being Relation holds rng (P * R) = R .: (rng P)
proof end;

theorem :: RELAT_1:161
for X, Y being set
for R being Relation holds (R | X) .: Y c= R .: Y by Th88, Th157;

theorem Th162: :: RELAT_1:162
for R being Relation
for X, Y being set st X c= Y holds
(R | Y) .: X = R .: X
proof end;

theorem :: RELAT_1:163
for X being set
for R being Relation holds (dom R) /\ X c= (R ~) .: (R .: X)
proof end;

definition
let R be Relation;
let Y be set ;
func R " Y -> set means :Def14: :: RELAT_1:def 14
 for x being set holds
( x in it iff ex y being set st
( [x,y] in R & y in Y ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex y being set st
( [x,y] in R & y in Y ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y being set st
( [x,y] in R & y in Y ) ) ) & ( for x being set holds
( x in b2 iff ex y being set st
( [x,y] in R & y in Y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines " RELAT_1:def 14 :
for R being Relation
for Y, b3 being set holds
( b3 = R " Y iff for x being set holds
( x in b3 iff ex y being set st
( [x,y] in R & y in Y ) ) );

theorem :: RELAT_1:164
canceled;

theorem :: RELAT_1:165
canceled;

theorem Th166: :: RELAT_1:166
for x, Y being set
for R being Relation holds
( x in R " Y iff ex y being set st
( y in rng R & [x,y] in R & y in Y ) )
proof end;

theorem Th167: :: RELAT_1:167
for Y being set
for R being Relation holds R " Y c= dom R
proof end;

theorem :: RELAT_1:168
for Y being set
for R being Relation holds R " Y = R " ((rng R) /\ Y)
proof end;

theorem Th169: :: RELAT_1:169
for R being Relation holds R " (rng R) = dom R
proof end;

theorem :: RELAT_1:170
for Y being set
for R being Relation holds R " Y c= R " (rng R)
proof end;

theorem :: RELAT_1:171
for R being Relation holds R " {} = {}
proof end;

theorem :: RELAT_1:172
for Y being set holds {} " Y = {}
proof end;

theorem :: RELAT_1:173
for Y being set
for R being Relation holds
( R " Y = {} iff rng R misses Y )
proof end;

theorem :: RELAT_1:174
for Y being set
for R being Relation st Y <> {} & Y c= rng R holds
R " Y <> {}
proof end;

theorem :: RELAT_1:175
for X, Y being set
for R being Relation holds R " (X \/ Y) = (R " X) \/ (R " Y)
proof end;

theorem :: RELAT_1:176
for X, Y being set
for R being Relation holds R " (X /\ Y) c= (R " X) /\ (R " Y)
proof end;

theorem :: RELAT_1:177
for X, Y being set
for R being Relation holds (R " X) \ (R " Y) c= R " (X \ Y)
proof end;

theorem Th178: :: RELAT_1:178
for X, Y being set
for R being Relation st X c= Y holds
R " X c= R " Y
proof end;

theorem Th179: :: RELAT_1:179
for Y being set
for P, R being Relation st P c= R holds
P " Y c= R " Y
proof end;

theorem :: RELAT_1:180
for X, Y being set
for P, R being Relation st P c= R & X c= Y holds
P " X c= R " Y
proof end;

theorem :: RELAT_1:181
for Y being set
for P, R being Relation holds (P * R) " Y = P " (R " Y)
proof end;

theorem Th182: :: RELAT_1:182
for P, R being Relation holds dom (P * R) = P " (dom R)
proof end;

theorem :: RELAT_1:183
for Y being set
for R being Relation holds (rng R) /\ Y c= (R ~) " (R " Y)
proof end;

begin

definition
let R be Relation;
attr R is empty-yielding means :Def15: :: RELAT_1:def 15
 rng R c= {{}};
end;

:: deftheorem Def15 defines empty-yielding RELAT_1:def 15 :
for R being Relation holds
( R is empty-yielding iff rng R c= {{}} );

theorem :: RELAT_1:184
for R being Relation holds
( R is empty-yielding iff for X being set st X in rng R holds
X = {} )
proof end;

theorem :: RELAT_1:185
for f, g being Relation
for A, B being set st f | A = g | A & f | B = g | B holds
f | (A \/ B) = g | (A \/ B)
proof end;

theorem :: RELAT_1:186
for X being set
for f, g being Relation st dom g c= X & g c= f holds
g c= f | X
proof end;

theorem :: RELAT_1:187
for f being Relation
for X being set st X misses dom f holds
f | X = {}
proof end;

theorem :: RELAT_1:188
for f, g being Relation
for A, B being set st A c= B & f | B = g | B holds
f | A = g | A
proof end;

theorem :: RELAT_1:189
for R, S being Relation holds R | (dom S) = R | (dom (S | (dom R)))
proof end;

registration
cluster empty Relation-like -> empty-yielding set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is empty-yielding
proof end;
end;

registration
let R be empty-yielding Relation;
let X be set ;
cluster R | X -> empty-yielding ;
coherence
R | X is empty-yielding
proof end;
end;

theorem :: RELAT_1:190
for X being set
for R being Relation st not R | X is empty-yielding holds
not R is empty-yielding ;

definition
let R be Relation;
let x be set ;
func Im (R,x) -> set equals :: RELAT_1:def 16
R .: {x};
correctness
coherence
R .: {x} is set ;
;
end;

:: deftheorem defines Im RELAT_1:def 16 :
for R being Relation
for x being set holds Im (R,x) = R .: {x};

scheme :: RELAT_1:sch 2
ExtensionalityR{ F1() -> Relation, F2() -> Relation, P1[ set , set ] } :
F1() = F2()
provided
A1: for a, b being set holds
( [a,b] in F1() iff P1[a,b] ) and
A2: for a, b being set holds
( [a,b] in F2() iff P1[a,b] )
proof end;

theorem :: RELAT_1:191
for X being set
for R being Relation holds dom (R | ((dom R) \ X)) = (dom R) \ X
proof end;

theorem :: RELAT_1:192
for X being set
for R being Relation holds R | X = R | ((dom R) /\ X)
proof end;

theorem :: RELAT_1:193
for X, Y being set holds dom [:X,Y:] c= X
proof end;

theorem :: RELAT_1:194
for X, Y being set holds rng [:X,Y:] c= Y
proof end;

theorem :: RELAT_1:195
for X, Y being set st X <> {} & Y <> {} holds
( dom [:X,Y:] = X & rng [:X,Y:] = Y )
proof end;

theorem :: RELAT_1:196
for R, Q being Relation st dom R = {} & dom Q = {} holds
R = Q
proof end;

theorem :: RELAT_1:197
for R, Q being Relation st rng R = {} & rng Q = {} holds
R = Q
proof end;

theorem :: RELAT_1:198
for R, Q, S being Relation st dom R = dom Q holds
dom (S * R) = dom (S * Q)
proof end;

theorem :: RELAT_1:199
for R, Q, S being Relation st rng R = rng Q holds
rng (R * S) = rng (Q * S)
proof end;

definition
let R be Relation;
let x be set ;
func Coim (R,x) -> set equals :: RELAT_1:def 17
R " {x};
coherence
R " {x} is set ;
end;

:: deftheorem defines Coim RELAT_1:def 17 :
for R being Relation
for x being set holds Coim (R,x) = R " {x};

registration
let R be trivial Relation;
cluster proj1 R -> trivial ;
coherence
dom R is trivial
proof end;
end;

registration
let R be trivial Relation;
cluster proj2 R -> trivial ;
coherence
rng R is trivial
proof end;
end;

theorem :: RELAT_1:200
for X being set
for R, S being Relation st rng R c= dom (S | X) holds
R * (S | X) = R * S
proof end;

theorem :: RELAT_1:201
for A being set
for Q, R being Relation st Q | A = R | A holds
Q .: A = R .: A
proof end;

definition
let X be set ;
let R be Relation;
attr R is X -defined means :Def18: :: RELAT_1:def 18
 dom R c= X;
attr R is X -valued means :Def19: :: RELAT_1:def 19
 rng R c= X;
end;

:: deftheorem Def18 defines -defined RELAT_1:def 18 :
for X being set
for R being Relation holds
( R is X -defined iff dom R c= X );

:: deftheorem Def19 defines -valued RELAT_1:def 19 :
for X being set
for R being Relation holds
( R is X -valued iff rng R c= X );

Lm2: for X, Y being set holds
( {} is X -defined & {} is Y -valued )
proof end;

registration
let X, Y be set ;
cluster Relation-like X -defined Y -valued set ;
existence
ex b1 being Relation st
( b1 is X -defined & b1 is Y -valued )
proof end;
end;

theorem :: RELAT_1:202
for D being set
for R being b1 -valued Relation
for y being set st y in rng R holds
y in D
proof end;

registration
let X, A be set ;
let R be A -valued Relation;
cluster R | X -> A -valued ;
coherence
R | X is A -valued
proof end;
end;

registration
let X, A be set ;
let R be A -defined Relation;
cluster R | X -> X -defined A -defined ;
coherence
( R | X is A -defined & R | X is X -defined )
proof end;
end;

registration
let X be set ;
cluster id X -> X -defined X -valued ;
coherence
( id X is X -defined & id X is X -valued )
proof end;
end;

registration
let A be set ;
let R be A -valued Relation;
let S be Relation;
cluster S * R -> A -valued ;
coherence
S * R is A -valued
proof end;
end;

registration
let A be set ;
let R be A -defined Relation;
let S be Relation;
cluster R * S -> A -defined ;
coherence
R * S is A -defined
proof end;
end;

theorem :: RELAT_1:203
for x, X, Y being set st x in X holds
Im ([:X,Y:],x) = Y
proof end;

theorem Th204: :: RELAT_1:204
for x, y being set
for R being Relation holds
( [x,y] in R iff y in Im (R,x) )
proof end;

theorem :: RELAT_1:205
for x being set
for R being Relation holds
( x in dom R iff Im (R,x) <> {} )
proof end;

theorem :: RELAT_1:206
for X, Y being set holds
( {} is X -defined & {} is Y -valued ) by Lm2;

registration
cluster empty Relation-like -> non-empty set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is non-empty
proof end;
end;

registration
let X be set ;
let R be X -defined Relation;
cluster -> X -defined Element of bool R;
coherence
for b1 being Subset of R holds b1 is X -defined
proof end;
end;

registration
let X be set ;
let R be X -valued Relation;
cluster -> X -valued Element of bool R;
coherence
for b1 being Subset of R holds b1 is X -valued
proof end;
end;

theorem :: RELAT_1:207
for X, Y being set
for R being Relation st X misses Y holds
(R | X) | Y = {}
proof end;

theorem :: RELAT_1:208
for x being set holds field {[x,x]} = {x}
proof end;

theorem Th209: :: RELAT_1:209
for X being set
for R being b1 -defined Relation holds R = R | X
proof end;

theorem :: RELAT_1:210
for X being set
for S being Relation
for R being b1 -defined Relation st R c= S holds
R c= S | X
proof end;

theorem Th211: :: RELAT_1:211
for X, A being set
for R being Relation st dom R c= X holds
R \ (R | A) = R | (X \ A)
proof end;

theorem Th212: :: RELAT_1:212
for A being set
for R being Relation holds dom (R \ (R | A)) = (dom R) \ A
proof end;

theorem :: RELAT_1:213
for A being set
for R being Relation holds (dom R) \ (dom (R | A)) = dom (R \ (R | A))
proof end;

theorem :: RELAT_1:214
for R, S being Relation st dom R misses dom S holds
R misses S
proof end;

theorem :: RELAT_1:215
for R, S being Relation st rng R misses rng S holds
R misses S
proof end;

theorem :: RELAT_1:216
for X, Y being set
for R being Relation st X c= Y holds
(R \ (R | Y)) | X = {}
proof end;

theorem :: RELAT_1:217
for X, Y being set st X c= Y holds
for R being b1 -defined Relation holds R is Y -defined
proof end;

theorem :: RELAT_1:218
for X, Y being set st X c= Y holds
for R being b1 -valued Relation holds R is Y -valued
proof end;

theorem :: RELAT_1:219
for R, S being Relation holds
( R c= S iff R c= S | (dom R) )
proof end;