:: Relations and Their Basic Properties
:: by Edmund Woronowicz
::
:: Received March 15, 1989
:: Copyright (c) 1990-2012 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 for 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;

registration
let R be Relation;
cluster -> Relation-like for 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;

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;

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

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

theorem Th1: :: RELAT_1:1
for P, R being Relation holds dom (P \/ R) = (dom P) \/ (dom R) by XTUPLE_0:23;

theorem Th2: :: RELAT_1:2
for P, R being Relation holds dom (P /\ R) c= (dom P) /\ (dom R) by XTUPLE_0:24;

theorem :: RELAT_1:3
for P, R being Relation holds (dom P) \ (dom R) c= dom (P \ R) by XTUPLE_0:25;

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

theorem :: RELAT_1:4
canceled;

theorem :: RELAT_1:5
canceled;

theorem :: RELAT_1:6
canceled;

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

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

theorem Th9: :: RELAT_1:9
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:10
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 Th11: :: RELAT_1:11
for P, R being Relation st P c= R holds
( dom P c= dom R & rng P c= rng R ) by XTUPLE_0:8, XTUPLE_0:9;

theorem Th12: :: RELAT_1:12
for P, R being Relation holds rng (P \/ R) = (rng P) \/ (rng R) by XTUPLE_0:27;

theorem Th13: :: RELAT_1:13
for P, R being Relation holds rng (P /\ R) c= (rng P) /\ (rng R) by XTUPLE_0:28;

theorem :: RELAT_1:14
for P, R being Relation holds (rng P) \ (rng R) c= rng (P \ R) by XTUPLE_0:29;

:: FIELD OF RELATION
definition
canceled;
canceled;
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 RELAT_1:def 4 :
canceled;

:: deftheorem RELAT_1:def 5 :
canceled;

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

theorem :: RELAT_1:15
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:16
for P, R being Relation st P c= R holds
field P c= field R
proof end;

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

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

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

:: CONVERSE RELATION
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 Th20: :: RELAT_1:20
for R being Relation holds
( rng R = dom (R ~) & dom R = rng (R ~) )
proof end;

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

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

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

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

:: COMPOSITION OF RELATIONS
definition
let P, R be set ;
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 being set
for 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 ) ) );

notation
let P, R be Relation;
synonym P * R for P (#) R;
end;

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

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

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

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

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

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

theorem :: RELAT_1:31
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:32
for P, R, Q being Relation holds P * (R \/ Q) = (P * R) \/ (P * Q)
proof end;

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

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

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

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

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

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

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

theorem Th38: :: RELAT_1:38
( dom {} = {} & rng {} = {} )
proof end;

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

registration
let X be empty set ;
cluster dom X -> empty ;
coherence
dom X is empty ;
cluster rng X -> empty ;
coherence
rng X is empty ;
let R be Relation;
cluster X (#) R -> empty ;
coherence
X * R is empty by Th39;
cluster R (#) X -> empty ;
coherence
R * X is empty by Th39;
end;

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

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

theorem :: RELAT_1:42
for R being Relation holds
( dom R = {} iff rng R = {} ) by Th38, Th41;

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

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

theorem :: RELAT_1:44
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 for 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;

:: IDENTITY RELATION
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 ) ) );

registration
let X be set ;
reduce dom (id X) to X;
reducibility
dom (id X) = X
proof end;
reduce rng (id X) to X;
reducibility
rng (id X) = X
proof end;
end;

theorem :: RELAT_1:45
for X being set holds
( dom (id X) = X & rng (id X) = X ) ;

registration
let X be set ;
reduce (id X) ~ to id X;
reducibility
(id X) ~ = id X
proof end;
end;

theorem :: RELAT_1:46
for X being set holds (id X) ~ = id X ;

theorem :: RELAT_1:47
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 Th48: :: RELAT_1:48
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 Th49: :: RELAT_1:49
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 Th50: :: RELAT_1:50
for X being set
for R being Relation holds
( R * (id X) c= R & (id X) * R c= R )
proof end;

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

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

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

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

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

theorem :: RELAT_1:56
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 Th57: :: RELAT_1:57
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 Th58: :: RELAT_1:58
for X being set
for R being Relation holds dom (R | X) c= X
proof end;

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

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

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

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

theorem :: RELAT_1:63
for X being set
for R, P being Relation holds (R | X) * P c= R * P by Th30, Th59;

theorem :: RELAT_1:64
for X being set
for P, R being Relation holds P * (R | X) c= P * R by Th29, Th59;

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

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

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

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

registration
let R be Relation;
reduce R | (dom R) to R;
reducibility
R | (dom R) = R by Th68;
end;

theorem :: RELAT_1:69
for R being Relation holds R | (dom R) = R ;

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

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

registration
let R be Relation;
let X be set ;
reduce (R | X) | X to R | X;
reducibility
(R | X) | X = R | X
proof end;
end;

theorem :: RELAT_1:72
for X being set
for R being Relation holds (R | X) | X = R | X ;

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

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

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

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

theorem Th77: :: RELAT_1:77
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 Th78: :: RELAT_1:78
for X, Y being set
for R being Relation holds R | (X \/ Y) = (R | X) \/ (R | Y)
proof end;

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

theorem Th80: :: RELAT_1:80
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:81
for R being Relation holds R | {} = {} ;

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

theorem :: RELAT_1:83
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 Th84: :: RELAT_1:84
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 Th85: :: RELAT_1:85
for Y being set
for R being Relation holds rng (Y |` R) c= Y
proof end;

theorem Th86: :: RELAT_1:86
for Y being set
for R being Relation holds Y |` R c= R
proof end;

theorem Th87: :: RELAT_1:87
for Y being set
for R being Relation holds rng (Y |` R) c= rng R
proof end;

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

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

theorem :: RELAT_1:90
for Y being set
for R, P being Relation holds (Y |` R) * P c= R * P by Th30, Th86;

theorem :: RELAT_1:91
for Y being set
for P, R being Relation holds P * (Y |` R) c= P * R by Th29, Th86;

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

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

theorem Th94: :: RELAT_1:94
for Y being set
for R being Relation st rng R c= Y holds
Y |` R = R
proof end;

registration
let R be Relation;
reduce (rng R) |` R to R;
reducibility
(rng R) |` R = R by Th94;
end;

theorem :: RELAT_1:95
for R being Relation holds (rng R) |` R = R ;

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

registration
let Y be set ;
let R be Relation;
reduce Y |` (Y |` R) to Y |` R;
reducibility
Y |` (Y |` R) = Y |` R
proof end;
end;

theorem :: RELAT_1:97
for Y being set
for R being Relation holds Y |` (Y |` R) = Y |` R ;

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

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

theorem Th100: :: RELAT_1:100
for X, Y being set
for R being Relation st X c= Y holds
X |` R c= Y |` R
proof end;

theorem Th101: :: RELAT_1:101
for Y being set
for P1, P2 being Relation st P1 c= P2 holds
Y |` P1 c= Y |` P2
proof end;

theorem :: RELAT_1:102
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:103
for X, Y being set
for R being Relation holds (X \/ Y) |` R = (X |` R) \/ (Y |` R)
proof end;

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

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

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

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

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

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

:: IMAGE OF SET IN RELATION
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 Th110: :: RELAT_1:110
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 Th111: :: RELAT_1:111
for X being set
for R being Relation holds R .: X c= rng R
proof end;

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

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

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

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

registration
let R be Relation;
let X be empty set ;
cluster R .: X -> empty ;
coherence
R .: X is empty
proof end;
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:116
canceled;

theorem :: RELAT_1:117
canceled;

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

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

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

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

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

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

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

theorem :: RELAT_1:125
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:126
for X being set
for P, R being Relation holds (P * R) .: X = R .: (P .: X)
proof end;

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

theorem :: RELAT_1:128
for X, Y being set
for R being Relation holds (R | X) .: Y c= R .: Y by Th59, Th124;

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

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

:: INVERSE IMAGE OF SET IN RELATION
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 Th131: :: RELAT_1:131
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 Th132: :: RELAT_1:132
for Y being set
for R being Relation holds R " Y c= dom R
proof end;

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

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

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

registration
let R be Relation;
let Y be empty set ;
cluster R " Y -> empty ;
coherence
R " Y is empty
proof end;
end;

registration
let R be empty Relation;
let Y be set ;
cluster R " Y -> empty ;
coherence
R " Y is empty
proof end;
end;

theorem :: RELAT_1:136
canceled;

theorem :: RELAT_1:137
canceled;

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

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

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

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

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

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

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

theorem :: RELAT_1:145
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:146
for Y being set
for P, R being Relation holds (P * R) " Y = P " (R " Y)
proof end;

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

theorem :: RELAT_1:148
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:149
for R being Relation holds
( R is empty-yielding iff for X being set st X in rng R holds
X = {} )
proof end;

:: from AMI_3
theorem :: RELAT_1:150
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:151
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:152
for f being Relation
for X being set st X misses dom f holds
f | X = {}
proof end;

:: from AMI_5
theorem :: RELAT_1:153
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;

:: missing, 2005.07.11, A.T.
theorem :: RELAT_1:154
for R, S being Relation holds R | (dom S) = R | (dom (S | (dom R)))
proof end;

:: missing, 2005.11.13, A.T.
registration
cluster empty Relation-like -> empty-yielding for 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:155
for X being set
for R being Relation st not R | X is empty-yielding holds
not R is empty-yielding ;

:: from EQREL_1 (Class), 2007.02.06
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};

:: missing, 2007.04.13, A.T.
:: from YELLOW_3, 2007.06.13, A.T.
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;

:: from SCMFSA6A, 2007.07.23, A.T.
theorem :: RELAT_1:156
for X being set
for R being Relation holds dom (R | ((dom R) \ X)) = (dom R) \ X
proof end;

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

:: missing, 2007.11.07, A.T.
theorem :: RELAT_1:158
for X, Y being set holds dom [:X,Y:] c= X
proof end;

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

:: from FUNCOP_1, 2008.02.19, A.T.
theorem :: RELAT_1:160
for X, Y being set st X <> {} & Y <> {} holds
( dom [:X,Y:] = X & rng [:X,Y:] = Y )
proof end;

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

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

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

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

:: from RELSET_2 (R"x, generalized), 2008.07.16, A.T.
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};

:: from NECKLACE, 2008.07.25, A.T.
registration
let R be trivial Relation;
cluster dom R -> trivial ;
coherence
dom R is trivial
proof end;
end;

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

:: comp. RFUNCT_2:34, CFCONT_1:31, 2008.08.07, A.T.
theorem :: RELAT_1:165
for X being set
for R, S being Relation st rng R c= dom (S | X) holds
R * (S | X) = R * S
proof end;

:: from LATTICE2, 2008.09.14, A.T.
theorem :: RELAT_1:166
for A being set
for Q, R being Relation st Q | A = R | A holds
Q .: A = R .: A
proof end;

:: new, 2009.01.21, A.T
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 );

Lm1: 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 for set ;
existence
ex b1 being Relation st
( b1 is X -defined & b1 is Y -valued )
proof end;
end;

:: from QC_LANG4, 2009.01.23, A.T
theorem :: RELAT_1:167
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;

:: new, 2009.02.07, A.T.
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;

:: 2009.02.16, A.T.
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;

:: 2009.02.16, A.T.
theorem :: RELAT_1:168
for x, X, Y being set st x in X holds
Im ([:X,Y:],x) = Y
proof end;

theorem Th169: :: RELAT_1:169
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:170
for x being set
for R being Relation holds
( x in dom R iff Im (R,x) <> {} )
proof end;

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

:: 2009.10.02, A.T.
registration
cluster empty Relation-like -> non-empty for 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 for 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 for Element of bool R;
coherence
for b1 being Subset of R holds b1 is X -valued
proof end;
end;

:: missing, 2010.01.02, A.T
theorem :: RELAT_1:172
for X, Y being set
for R being Relation st X misses Y holds
(R | X) | Y = {}
proof end;

:: from AMISTD_3, 2010.01.10, A.T.
theorem :: RELAT_1:173
for x being set holds field {[x,x]} = {x}
proof end;

registration
let X be set ;
let R be X -defined Relation;
reduce R | X to R;
reducibility
R | X = R
proof end;
end;

registration
let Y be set ;
let R be Y -valued Relation;
reduce Y |` R to R;
reducibility
Y |` R = R
proof end;
end;

theorem :: RELAT_1:174
for X being set
for R being b1 -defined Relation holds R = R | X ;

theorem :: RELAT_1:175
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;

:: missing, 2010.04.07, A.T.
theorem Th176: :: RELAT_1:176
for X, A being set
for R being Relation st dom R c= X holds
R \ (R | A) = R | (X \ A)
proof end;

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

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

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

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

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

theorem :: RELAT_1:182
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:183
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:184
for R, S being Relation holds
( R c= S iff R c= S | (dom R) )
proof end;

theorem :: RELAT_1:185
for X, Y being set
for R being b1 -defined b2 -valued Relation holds R c= [:X,Y:]
proof end;

:: new, 20011.06.11, A.T.
theorem Th186: :: RELAT_1:186
for X being set
for R being Relation holds dom (X |` R) c= dom R
proof end;

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

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

registration
let X be empty set ;
cluster Relation-like X -defined -> empty X -defined for set ;
coherence
for b1 being X -defined Relation holds b1 is empty
proof end;
cluster Relation-like X -valued -> empty X -valued for set ;
coherence
for b1 being X -valued Relation holds b1 is empty
proof end;
end;