:: Relations and Their Basic Properties
:: by Edmund Woronowicz
::
:: Copyright (c) 1990-2021 Association of Mizar Users

definition
let IT be set ;
attr IT is Relation-like means :Def1: :: RELAT_1:def 1
for x being object st x in IT holds
ex y, z being object 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 object st x in IT holds
ex y, z being object st x = [y,z] );

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

definition 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
by Def1;
end;

scheme :: RELAT_1:sch 1
RelExistence{ F1() -> set , F2() -> set , P1[ object , object ] } :
ex R being Relation st
for x, y being object 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 object holds
( [a,b] in P iff [a,b] in R );
compatibility
( P = R iff for a, b being object 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 object holds
( [a,b] in P iff [a,b] in R ) );

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

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

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

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

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

registration
let a, b, c, d be object ;
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 object st [a,b] in P holds
[a,b] in A;
compatibility
( P c= A iff for a, b being object 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 object st [a,b] in P holds
[a,b] in A );

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

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

theorem :: RELAT_1:1
canceled;

theorem :: RELAT_1:2
canceled;

theorem :: RELAT_1:3
canceled;

theorem :: RELAT_1:4
canceled;

theorem :: RELAT_1:5
canceled;

theorem :: RELAT_1:6
canceled;

::$CT 6 theorem Th1: :: 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 ; theorem Th3: :: RELAT_1:9 for x, y being object holds ( dom {[x,y]} = {x} & rng {[x,y]} = {y} ) proof end; theorem :: RELAT_1:10 for a, b, x, y being object holds ( dom {[a,b],[x,y]} = {a,x} & rng {[a,b],[x,y]} = {b,y} ) proof end; theorem :: RELAT_1:11 for P, R being Relation st P c= R holds ( dom P c= dom R & rng P c= rng R ) by ; theorem :: RELAT_1:12 for P, R being Relation holds rng (P \/ R) = (rng P) \/ (rng R) by XTUPLE_0:27; theorem :: 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 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 object 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 Th11: :: RELAT_1:17 for x, y being object holds field {[x,y]} = {x,y} proof end; theorem :: RELAT_1:18 for P, R being Relation holds field (P \/ R) = () \/ () proof end; theorem :: RELAT_1:19 for P, R being Relation holds field (P /\ R) c= () /\ () proof end; :: CONVERSE RELATION definition let R be Relation; func R ~ -> Relation means :Def5: :: RELAT_1:def 7 for x, y being object holds ( [x,y] in it iff [y,x] in R ); existence ex b1 being Relation st for x, y being object holds ( [x,y] in b1 iff [y,x] in R ) proof end; uniqueness for b1, b2 being Relation st ( for x, y being object holds ( [x,y] in b1 iff [y,x] in R ) ) & ( for x, y being object 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 object holds ( [x,y] in b1 iff [y,x] in b2 ) ) holds for x, y being object holds ( [x,y] in b2 iff [y,x] in b1 ) ; end; :: deftheorem Def5 defines ~ RELAT_1:def 7 : for R, b2 being Relation holds ( b2 = R ~ iff for x, y being object holds ( [x,y] in b2 iff [y,x] in R ) ); theorem Th14: :: 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 :Def6: :: RELAT_1:def 8 for x, y being object holds ( [x,y] in it iff ex z being object st ( [x,z] in P & [z,y] in R ) ); existence ex b1 being Relation st for x, y being object holds ( [x,y] in b1 iff ex z being object st ( [x,z] in P & [z,y] in R ) ) proof end; uniqueness for b1, b2 being Relation st ( for x, y being object holds ( [x,y] in b1 iff ex z being object st ( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being object holds ( [x,y] in b2 iff ex z being object st ( [x,z] in P & [z,y] in R ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def6 defines (#) RELAT_1:def 8 : for P, R being set for b3 being Relation holds ( b3 = P (#) R iff for x, y being object holds ( [x,y] in b3 iff ex z being object st ( [x,z] in P & [z,y] in R ) ) ); notation let P, R be Relation; synonym P * R for P (#) R; end; theorem Th19: :: RELAT_1:25 for P, R being Relation holds dom (P * R) c= dom P proof end; theorem Th20: :: RELAT_1:26 for P, R being Relation holds rng (P * R) c= rng R proof end; theorem :: RELAT_1:27 for P, R 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 Th23: :: RELAT_1:29 for P, Q, R being Relation st P c= R holds Q * P c= Q * R proof end; theorem Th24: :: 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, Q, R, S being Relation st P c= R & Q c= S holds P * Q c= R * S proof end; theorem :: RELAT_1:32 for P, Q, R being Relation holds P * (R \/ Q) = (P * R) \/ (P * Q) proof end; theorem :: RELAT_1:33 for P, Q, R being Relation holds P * (R /\ Q) c= (P * R) /\ (P * Q) proof end; theorem :: RELAT_1:34 for P, Q, R 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 Th30: :: RELAT_1:36 for P, Q, R 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 Th31: :: RELAT_1:37 for R being Relation st ( for x, y being object holds not [x,y] in R ) holds R = {} ; theorem Th32: :: RELAT_1:38 ( dom {} = {} & rng {} = {} ) ; theorem Th33: :: 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 Th33; cluster R (#) X -> empty ; coherence R * X is empty by Th33; end; theorem :: RELAT_1:40 theorem Th35: :: 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 ; 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 P, R being Relation st rng R misses dom P holds R * P = {} proof end; definition let R be Relation; attr R is non-empty means :Def7: :: RELAT_1:def 9 not {} in rng R; end; :: deftheorem Def7 defines non-empty RELAT_1:def 9 : for R being Relation holds ( R is non-empty iff not {} in rng R ); registration 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 :Def8: :: RELAT_1:def 10 for x, y being object holds ( [x,y] in it iff ( x in X & x = y ) ); existence ex b1 being Relation st for x, y being object holds ( [x,y] in b1 iff ( x in X & x = y ) ) proof end; uniqueness for b1, b2 being Relation st ( for x, y being object holds ( [x,y] in b1 iff ( x in X & x = y ) ) ) & ( for x, y being object holds ( [x,y] in b2 iff ( x in X & x = y ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def8 defines id RELAT_1:def 10 : for X being set for b2 being Relation holds ( b2 = id X iff for x, y being object 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 object st x in X holds [x,x] in R ) holds id X c= R proof end; theorem Th42: :: RELAT_1:48 for X being set for x, y being object for R being Relation holds ( [x,y] in (id X) * R iff ( x in X & [x,y] in R ) ) proof end; theorem Th43: :: RELAT_1:49 for Y being set for x, y being object for R being Relation holds ( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) ) proof end; theorem Th44: :: 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 Th45: :: 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 Th45; theorem Th47: :: 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 Th47; theorem :: RELAT_1:55 proof end; theorem :: RELAT_1:56 for X being set for P1, P2, R 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 :Def9: :: RELAT_1:def 11 for x, y being object holds ( [x,y] in it iff ( x in X & [x,y] in R ) ); existence ex b1 being Relation st for x, y being object 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 object holds ( [x,y] in b1 iff ( x in X & [x,y] in R ) ) ) & ( for x, y being object holds ( [x,y] in b2 iff ( x in X & [x,y] in R ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def9 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 object 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 Th51: :: RELAT_1:57 for X being set for x being object for R being Relation holds ( x in dom (R | X) iff ( x in X & x in dom R ) ) proof end; theorem :: RELAT_1:58 for X being set for R being Relation holds dom (R | X) c= X by Th51; theorem Th53: :: RELAT_1:59 for X being set for R being Relation holds R | X c= R by Def9; theorem :: RELAT_1:60 for X being set for R being Relation holds dom (R | X) c= dom R by Th51; theorem Th55: :: 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 P, R being Relation holds (R | X) * P c= R * P by ; theorem :: RELAT_1:64 for X being set for P, R being Relation holds P * (R | X) c= P * R by ; 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 Th61: :: RELAT_1:67 for X being set for R being Relation holds R | X = R /\ [:X,(rng R):] proof end; theorem Th62: :: 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 Th62; end; theorem :: RELAT_1:69 for R being Relation holds R | (dom R) = R ; theorem :: RELAT_1:70 for X being set for R being Relation holds rng (R | X) c= rng R by ; theorem Th65: :: 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 X, Y being set for R being Relation st Y c= X holds (R | X) | Y = R | Y proof end; theorem Th69: :: 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 Th70: :: 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 Th71: :: 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 Th72: :: 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 Th74: :: 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 :Def10: :: RELAT_1:def 12 for x, y being object holds ( [x,y] in it iff ( y in Y & [x,y] in R ) ); existence ex b1 being Relation st for x, y being object 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 object holds ( [x,y] in b1 iff ( y in Y & [x,y] in R ) ) ) & ( for x, y being object holds ( [x,y] in b2 iff ( y in Y & [x,y] in R ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def10 defines | RELAT_1:def 12 : for Y being set for R, b3 being Relation holds ( b3 = Y | R iff for x, y being object 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 Th78: :: RELAT_1:84 for Y being set for y being object for R being Relation holds ( y in rng (Y | R) iff ( y in Y & y in rng R ) ) proof end; theorem :: RELAT_1:85 for Y being set for R being Relation holds rng (Y | R) c= Y by Th78; theorem Th80: :: RELAT_1:86 for Y being set for R being Relation holds Y | R c= R by Def10; theorem :: RELAT_1:87 for Y being set for R being Relation holds rng (Y | R) c= rng R by ; theorem Th82: :: 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 P, R being Relation holds (Y | R) * P c= R * P by ; theorem :: RELAT_1:91 for Y being set for P, R being Relation holds P * (Y | R) c= P * R by ; theorem :: RELAT_1:92 for Y being set for R being Relation holds Y | R = R * (id Y) proof end; theorem Th87: :: RELAT_1:93 for Y being set for R being Relation holds Y | R = R /\ [:(dom R),Y:] proof end; theorem Th88: :: 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 Th88; end; theorem :: RELAT_1:95 for R being Relation holds (rng R) | R = R ; theorem Th90: :: RELAT_1:96 for X, Y 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 X, Y being set for R being Relation st Y c= X holds Y | (X | R) = Y | R proof end; theorem Th94: :: 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 Th95: :: 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 | {} = {} by Def10; 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 X, Y 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 :Def11: :: RELAT_1:def 13 for y being object holds ( y in it iff ex x being object st ( [x,y] in R & x in X ) ); existence ex b1 being set st for y being object holds ( y in b1 iff ex x being object st ( [x,y] in R & x in X ) ) proof end; uniqueness for b1, b2 being set st ( for y being object holds ( y in b1 iff ex x being object st ( [x,y] in R & x in X ) ) ) & ( for y being object holds ( y in b2 iff ex x being object st ( [x,y] in R & x in X ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def11 defines .: RELAT_1:def 13 : for R being Relation for X, b3 being set holds ( b3 = R .: X iff for y being object holds ( y in b3 iff ex x being object st ( [x,y] in R & x in X ) ) ); theorem Th104: :: RELAT_1:110 for X being set for y being object for R being Relation holds ( y in R .: X iff ex x being object st ( x in dom R & [x,y] in R & x in X ) ) proof end; theorem Th105: :: 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 Th107: :: 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; ::$CT 2
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 Th115: :: 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 Th116: :: 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 Th119: :: 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 ;

theorem Th121: :: 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 :Def12: :: RELAT_1:def 14
for x being object holds
( x in it iff ex y being object st
( [x,y] in R & y in Y ) );
existence
ex b1 being set st
for x being object holds
( x in b1 iff ex y being object st
( [x,y] in R & y in Y ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ex y being object st
( [x,y] in R & y in Y ) ) ) & ( for x being object holds
( x in b2 iff ex y being object st
( [x,y] in R & y in Y ) ) ) holds
b1 = b2
proof end;
end;

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

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

theorem Th124: :: 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 Th126: :: 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;

::\$CT 2
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 Th133: :: 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 Th134: :: 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 Th137: :: 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;

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

:: deftheorem Def13 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
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 ;
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 object ;
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 object holds Im (R,x) = R .: {x};

:: from YELLOW_3, 2007.06.13, A.T.
scheme :: RELAT_1:sch 2
ExtensionalityR{ F1() -> Relation, F2() -> Relation, P1[ object , object ] } :
F1() = F2()
provided
A1: for a, b being object holds
( [a,b] in F1() iff P1[a,b] ) and
A2: for a, b being object 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 Q, R being Relation st dom R = {} & dom Q = {} holds
R = Q ;

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

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

theorem :: RELAT_1:164
for Q, R, 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 object ;
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 object holds Coim (R,x) = R " {x};

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

registration
let R be trivial Relation;
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 :Def16: :: RELAT_1:def 18
dom R c= X;
attr R is X -valued means :Def17: :: RELAT_1:def 19
rng R c= X;
end;

:: deftheorem Def16 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 Def17 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 ;
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 object 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 )
;
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, Y being set
for x being object st x in X holds
Im ([:X,Y:],x) = Y
proof end;

theorem Th159: :: RELAT_1:169
for x, y being object
for R being Relation holds
( [x,y] in R iff y in Im (R,x) )
proof end;

theorem :: RELAT_1:170
for x being object
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
coherence
for b1 being Relation st b1 is empty holds
b1 is non-empty
;
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 object 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 Th166: :: RELAT_1:176
for A, X being set
for R being Relation st dom R c= X holds
R \ (R | A) = R | (X \ A)
proof end;

theorem Th167: :: 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 Th169: :: 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 Th175: :: 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 :: RELAT_1:186
for X being set
for R being Relation holds dom (X | R) c= dom R by ;

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 ;
coherence
for b1 being X -defined Relation holds b1 is empty
proof end;
coherence
for b1 being X -valued Relation holds b1 is empty
proof end;
end;

:: from PNPROC_1, 2012.02.20, A.T.
theorem :: RELAT_1:187
for X, Y being set
for P, R being Relation st X misses Y holds
P | X misses R | Y
proof end;

theorem :: RELAT_1:188
for Y being set
for R being Relation holds Y |` R c= R | (R " Y)
proof end;

theorem :: RELAT_1:189
for f being Relation
for x, y being object st dom f = {x} & rng f = {y} holds
f = {[x,y]}
proof end;

registration
let X, Y be set ;
let a1 be set , a2 be set ;
a1 -defined a2 -valued Relation ex b1 being set st
for b2 being X -defined Y -valued Relation holds b2 in b1
proof end;
end;