:: RELSET_1 semantic presentation begin definition let X, Y be set ; mode Relation of X,Y is Subset of [:X,Y:]; end; registration let X, Y be set ; cluster -> Relation-like for Element of bool [:X,Y:]; coherence for b1 being Subset of [:X,Y:] holds b1 is Relation-like ; end; registration let X, Y be set ; cluster -> X -defined Y -valued for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y holds ( b1 is X -defined & b1 is Y -valued ) proof let R be Relation of X,Y; ::_thesis: ( R is X -defined & R is Y -valued ) thus dom R c= X :: according to RELAT_1:def_18 ::_thesis: R is Y -valued proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom R or x in X ) assume x in dom R ; ::_thesis: x in X then ex y being set st [x,y] in R by XTUPLE_0:def_12; hence x in X by ZFMISC_1:87; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng R or y in Y ) assume y in rng R ; ::_thesis: y in Y then ex x being set st [x,y] in R by XTUPLE_0:def_13; hence y in Y by ZFMISC_1:87; ::_thesis: verum end; end; definition let X, Y be set ; let R be Relation of X,Y; let Z be set ; :: original: c= redefine predR c= Z means :: RELSET_1:def 1 for x being Element of X for y being Element of Y st [x,y] in R holds [x,y] in Z; compatibility ( R c= Z iff for x being Element of X for y being Element of Y st [x,y] in R holds [x,y] in Z ) proof thus ( R c= Z implies for x being Element of X for y being Element of Y st [x,y] in R holds [x,y] in Z ) ; ::_thesis: ( ( for x being Element of X for y being Element of Y st [x,y] in R holds [x,y] in Z ) implies R c= Z ) assume A1: for x being Element of X for y being Element of Y st [x,y] in R holds [x,y] in Z ; ::_thesis: R c= Z let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in R or [a,b] in Z ) assume A2: [a,b] in R ; ::_thesis: [a,b] in Z then reconsider a9 = a as Element of X by ZFMISC_1:87; reconsider b9 = b as Element of Y by A2, ZFMISC_1:87; [a9,b9] in Z by A1, A2; hence [a,b] in Z ; ::_thesis: verum end; end; :: deftheorem defines c= RELSET_1:def_1_:_ for X, Y being set for R being Relation of X,Y for Z being set holds ( R c= Z iff for x being Element of X for y being Element of Y st [x,y] in R holds [x,y] in Z ); definition let X, Y be set ; let P, R be Relation of X,Y; :: original: = redefine predP = R means :: RELSET_1:def 2 for x being Element of X for y being Element of Y holds ( [x,y] in P iff [x,y] in R ); compatibility ( P = R iff for x being Element of X for y being Element of Y holds ( [x,y] in P iff [x,y] in R ) ) proof thus ( P = R implies for x being Element of X for y being Element of Y holds ( [x,y] in P iff [x,y] in R ) ) ; ::_thesis: ( ( for x being Element of X for y being Element of Y holds ( [x,y] in P iff [x,y] in R ) ) implies P = R ) assume A1: for x being Element of X for y being Element of Y holds ( [x,y] in P iff [x,y] in R ) ; ::_thesis: P = R let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in P or [a,b] in R ) & ( not [a,b] in R or [a,b] in P ) ) hereby ::_thesis: ( not [a,b] in R or [a,b] in P ) assume A2: [a,b] in P ; ::_thesis: [a,b] in R then reconsider a9 = a as Element of X by ZFMISC_1:87; reconsider b9 = b as Element of Y by A2, ZFMISC_1:87; [a9,b9] in R by A1, A2; hence [a,b] in R ; ::_thesis: verum end; assume A3: [a,b] in R ; ::_thesis: [a,b] in P then reconsider a9 = a as Element of X by ZFMISC_1:87; reconsider b9 = b as Element of Y by A3, ZFMISC_1:87; [a9,b9] in P by A1, A3; hence [a,b] in P ; ::_thesis: verum end; end; :: deftheorem defines = RELSET_1:def_2_:_ for X, Y being set for P, R being Relation of X,Y holds ( P = R iff for x being Element of X for y being Element of Y holds ( [x,y] in P iff [x,y] in R ) ); theorem :: RELSET_1:1 for A, X, Y being set for R being Relation of X,Y st A c= R holds A is Relation of X,Y by XBOOLE_1:1; theorem :: RELSET_1:2 for a, X, Y being set for R being Relation of X,Y st a in R holds ex x, y being set st ( a = [x,y] & x in X & y in Y ) proof let a, X, Y be set ; ::_thesis: for R being Relation of X,Y st a in R holds ex x, y being set st ( a = [x,y] & x in X & y in Y ) let R be Relation of X,Y; ::_thesis: ( a in R implies ex x, y being set st ( a = [x,y] & x in X & y in Y ) ) assume A1: a in R ; ::_thesis: ex x, y being set st ( a = [x,y] & x in X & y in Y ) then consider x, y being set such that A2: a = [x,y] by RELAT_1:def_1; ( x in X & y in Y ) by A1, A2, ZFMISC_1:87; hence ex x, y being set st ( a = [x,y] & x in X & y in Y ) by A2; ::_thesis: verum end; theorem :: RELSET_1:3 for x, X, y, Y being set st x in X & y in Y holds {[x,y]} is Relation of X,Y proof let x, X, y, Y be set ; ::_thesis: ( x in X & y in Y implies {[x,y]} is Relation of X,Y ) assume ( x in X & y in Y ) ; ::_thesis: {[x,y]} is Relation of X,Y then [x,y] in [:X,Y:] by ZFMISC_1:87; hence {[x,y]} is Relation of X,Y by ZFMISC_1:31; ::_thesis: verum end; theorem :: RELSET_1:4 for X, Y being set for R being Relation st dom R c= X & rng R c= Y holds R is Relation of X,Y proof let X, Y be set ; ::_thesis: for R being Relation st dom R c= X & rng R c= Y holds R is Relation of X,Y let R be Relation; ::_thesis: ( dom R c= X & rng R c= Y implies R is Relation of X,Y ) assume ( dom R c= X & rng R c= Y ) ; ::_thesis: R is Relation of X,Y then ( R c= [:(dom R),(rng R):] & [:(dom R),(rng R):] c= [:X,Y:] ) by RELAT_1:7, ZFMISC_1:96; hence R is Relation of X,Y by XBOOLE_1:1; ::_thesis: verum end; theorem :: RELSET_1:5 for X, X1, Y being set for R being Relation of X,Y st dom R c= X1 holds R is Relation of X1,Y proof let X, X1, Y be set ; ::_thesis: for R being Relation of X,Y st dom R c= X1 holds R is Relation of X1,Y let R be Relation of X,Y; ::_thesis: ( dom R c= X1 implies R is Relation of X1,Y ) A1: rng R c= Y by RELAT_1:def_19; assume dom R c= X1 ; ::_thesis: R is Relation of X1,Y then ( R c= [:(dom R),(rng R):] & [:(dom R),(rng R):] c= [:X1,Y:] ) by A1, RELAT_1:7, ZFMISC_1:96; hence R is Relation of X1,Y by XBOOLE_1:1; ::_thesis: verum end; theorem :: RELSET_1:6 for Y, Y1, X being set for R being Relation of X,Y st rng R c= Y1 holds R is Relation of X,Y1 proof let Y, Y1, X be set ; ::_thesis: for R being Relation of X,Y st rng R c= Y1 holds R is Relation of X,Y1 let R be Relation of X,Y; ::_thesis: ( rng R c= Y1 implies R is Relation of X,Y1 ) A1: dom R c= X by RELAT_1:def_18; assume rng R c= Y1 ; ::_thesis: R is Relation of X,Y1 then ( R c= [:(dom R),(rng R):] & [:(dom R),(rng R):] c= [:X,Y1:] ) by A1, RELAT_1:7, ZFMISC_1:96; hence R is Relation of X,Y1 by XBOOLE_1:1; ::_thesis: verum end; theorem :: RELSET_1:7 for X, X1, Y, Y1 being set for R being Relation of X,Y st X c= X1 & Y c= Y1 holds R is Relation of X1,Y1 proof let X, X1, Y, Y1 be set ; ::_thesis: for R being Relation of X,Y st X c= X1 & Y c= Y1 holds R is Relation of X1,Y1 let R be Relation of X,Y; ::_thesis: ( X c= X1 & Y c= Y1 implies R is Relation of X1,Y1 ) assume ( X c= X1 & Y c= Y1 ) ; ::_thesis: R is Relation of X1,Y1 then [:X,Y:] c= [:X1,Y1:] by ZFMISC_1:96; hence R is Relation of X1,Y1 by XBOOLE_1:1; ::_thesis: verum end; registration let X be set ; let R, S be X -defined Relation; clusterR \/ S -> X -defined ; coherence R \/ S is X -defined proof A1: dom (R \/ S) = (dom R) \/ (dom S) by RELAT_1:1; ( dom R c= X & dom S c= X ) by RELAT_1:def_18; hence dom (R \/ S) c= X by A1, XBOOLE_1:8; :: according to RELAT_1:def_18 ::_thesis: verum end; end; registration let X be set ; let R be X -defined Relation; let S be Relation; clusterR /\ S -> X -defined ; coherence R /\ S is X -defined proof R /\ S c= R by XBOOLE_1:17; then ( dom R c= X & dom (R /\ S) c= dom R ) by RELAT_1:11, RELAT_1:def_18; hence dom (R /\ S) c= X by XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: verum end; clusterR \ S -> X -defined ; coherence R \ S is X -defined ; end; registration let X be set ; let R, S be X -valued Relation; clusterR \/ S -> X -valued ; coherence R \/ S is X -valued proof A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12; ( rng R c= X & rng S c= X ) by RELAT_1:def_19; hence rng (R \/ S) c= X by A1, XBOOLE_1:8; :: according to RELAT_1:def_19 ::_thesis: verum end; end; registration let X be set ; let R be X -valued Relation; let S be Relation; clusterR /\ S -> X -valued ; coherence R /\ S is X -valued proof R /\ S c= R by XBOOLE_1:17; then ( rng R c= X & rng (R /\ S) c= rng R ) by RELAT_1:11, RELAT_1:def_19; hence rng (R /\ S) c= X by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum end; clusterR \ S -> X -valued ; coherence R \ S is X -valued ; end; definition let X be set ; let R be X -defined Relation; :: original: dom redefine func dom R -> Subset of X; coherence dom R is Subset of X by RELAT_1:def_18; end; definition let X be set ; let R be X -valued Relation; :: original: rng redefine func rng R -> Subset of X; coherence rng R is Subset of X by RELAT_1:def_19; end; theorem :: RELSET_1:8 for X, Y being set for R being Relation of X,Y holds field R c= X \/ Y proof let X, Y be set ; ::_thesis: for R being Relation of X,Y holds field R c= X \/ Y let R be Relation of X,Y; ::_thesis: field R c= X \/ Y (dom R) \/ (rng R) c= X \/ Y by XBOOLE_1:13; hence field R c= X \/ Y ; ::_thesis: verum end; theorem :: RELSET_1:9 for Y, X being set for R being Relation of X,Y holds ( ( for x being set st x in X holds ex y being set st [x,y] in R ) iff dom R = X ) proof let Y, X be set ; ::_thesis: for R being Relation of X,Y holds ( ( for x being set st x in X holds ex y being set st [x,y] in R ) iff dom R = X ) let R be Relation of X,Y; ::_thesis: ( ( for x being set st x in X holds ex y being set st [x,y] in R ) iff dom R = X ) thus ( ( for x being set st x in X holds ex y being set st [x,y] in R ) implies dom R = X ) ::_thesis: ( dom R = X implies for x being set st x in X holds ex y being set st [x,y] in R ) proof assume A1: for x being set st x in X holds ex y being set st [x,y] in R ; ::_thesis: dom R = X now__::_thesis:_for_x_being_set_holds_ (_x_in_dom_R_iff_x_in_X_) let x be set ; ::_thesis: ( x in dom R iff x in X ) now__::_thesis:_(_x_in_X_implies_x_in_dom_R_) assume x in X ; ::_thesis: x in dom R then ex y being set st [x,y] in R by A1; hence x in dom R by XTUPLE_0:def_12; ::_thesis: verum end; hence ( x in dom R iff x in X ) ; ::_thesis: verum end; hence dom R = X by TARSKI:1; ::_thesis: verum end; thus ( dom R = X implies for x being set st x in X holds ex y being set st [x,y] in R ) by XTUPLE_0:def_12; ::_thesis: verum end; theorem :: RELSET_1:10 for X, Y being set for R being Relation of X,Y holds ( ( for y being set st y in Y holds ex x being set st [x,y] in R ) iff rng R = Y ) proof let X, Y be set ; ::_thesis: for R being Relation of X,Y holds ( ( for y being set st y in Y holds ex x being set st [x,y] in R ) iff rng R = Y ) let R be Relation of X,Y; ::_thesis: ( ( for y being set st y in Y holds ex x being set st [x,y] in R ) iff rng R = Y ) thus ( ( for y being set st y in Y holds ex x being set st [x,y] in R ) implies rng R = Y ) ::_thesis: ( rng R = Y implies for y being set st y in Y holds ex x being set st [x,y] in R ) proof assume A1: for y being set st y in Y holds ex x being set st [x,y] in R ; ::_thesis: rng R = Y now__::_thesis:_for_y_being_set_holds_ (_y_in_rng_R_iff_y_in_Y_) let y be set ; ::_thesis: ( y in rng R iff y in Y ) now__::_thesis:_(_y_in_Y_implies_y_in_rng_R_) assume y in Y ; ::_thesis: y in rng R then ex x being set st [x,y] in R by A1; hence y in rng R by XTUPLE_0:def_13; ::_thesis: verum end; hence ( y in rng R iff y in Y ) ; ::_thesis: verum end; hence rng R = Y by TARSKI:1; ::_thesis: verum end; thus ( rng R = Y implies for y being set st y in Y holds ex x being set st [x,y] in R ) by XTUPLE_0:def_13; ::_thesis: verum end; definition let X, Y be set ; let R be Relation of X,Y; :: original: ~ redefine funcR ~ -> Relation of Y,X; coherence R ~ is Relation of Y,X proof now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_R_~_holds_ [x,y]_in_[:Y,X:] let x, y be set ; ::_thesis: ( [x,y] in R ~ implies [x,y] in [:Y,X:] ) assume [x,y] in R ~ ; ::_thesis: [x,y] in [:Y,X:] then [y,x] in R by RELAT_1:def_7; hence [x,y] in [:Y,X:] by ZFMISC_1:88; ::_thesis: verum end; hence R ~ is Relation of Y,X by RELAT_1:def_3; ::_thesis: verum end; end; definition let X, Y1, Y2, Z be set ; let P be Relation of X,Y1; let R be Relation of Y2,Z; :: original: * redefine funcP * R -> Relation of X,Z; coherence P * R is Relation of X,Z proof now__::_thesis:_for_x,_z_being_set_st_[x,z]_in_P_*_R_holds_ [x,z]_in_[:X,Z:] let x, z be set ; ::_thesis: ( [x,z] in P * R implies [x,z] in [:X,Z:] ) assume [x,z] in P * R ; ::_thesis: [x,z] in [:X,Z:] then ex y being set st ( [x,y] in P & [y,z] in R ) by RELAT_1:def_8; then ( x in X & z in Z ) by ZFMISC_1:87; hence [x,z] in [:X,Z:] by ZFMISC_1:87; ::_thesis: verum end; hence P * R is Relation of X,Z by RELAT_1:def_3; ::_thesis: verum end; end; theorem :: RELSET_1:11 for X, Y being set for R being Relation of X,Y holds ( dom (R ~) = rng R & rng (R ~) = dom R ) proof let X, Y be set ; ::_thesis: for R being Relation of X,Y holds ( dom (R ~) = rng R & rng (R ~) = dom R ) let R be Relation of X,Y; ::_thesis: ( dom (R ~) = rng R & rng (R ~) = dom R ) now__::_thesis:_for_x_being_set_holds_ (_x_in_dom_(R_~)_iff_x_in_rng_R_) let x be set ; ::_thesis: ( x in dom (R ~) iff x in rng R ) A1: now__::_thesis:_(_x_in_rng_R_implies_x_in_dom_(R_~)_) assume x in rng R ; ::_thesis: x in dom (R ~) then consider y being set such that A2: [y,x] in R by XTUPLE_0:def_13; [x,y] in R ~ by A2, RELAT_1:def_7; hence x in dom (R ~) by XTUPLE_0:def_12; ::_thesis: verum end; now__::_thesis:_(_x_in_dom_(R_~)_implies_x_in_rng_R_) assume x in dom (R ~) ; ::_thesis: x in rng R then consider y being set such that A3: [x,y] in R ~ by XTUPLE_0:def_12; [y,x] in R by A3, RELAT_1:def_7; hence x in rng R by XTUPLE_0:def_13; ::_thesis: verum end; hence ( x in dom (R ~) iff x in rng R ) by A1; ::_thesis: verum end; hence dom (R ~) = rng R by TARSKI:1; ::_thesis: rng (R ~) = dom R now__::_thesis:_for_x_being_set_holds_ (_x_in_rng_(R_~)_iff_x_in_dom_R_) let x be set ; ::_thesis: ( x in rng (R ~) iff x in dom R ) A4: now__::_thesis:_(_x_in_dom_R_implies_x_in_rng_(R_~)_) assume x in dom R ; ::_thesis: x in rng (R ~) then consider y being set such that A5: [x,y] in R by XTUPLE_0:def_12; [y,x] in R ~ by A5, RELAT_1:def_7; hence x in rng (R ~) by XTUPLE_0:def_13; ::_thesis: verum end; now__::_thesis:_(_x_in_rng_(R_~)_implies_x_in_dom_R_) assume x in rng (R ~) ; ::_thesis: x in dom R then consider y being set such that A6: [y,x] in R ~ by XTUPLE_0:def_13; [x,y] in R by A6, RELAT_1:def_7; hence x in dom R by XTUPLE_0:def_12; ::_thesis: verum end; hence ( x in rng (R ~) iff x in dom R ) by A4; ::_thesis: verum end; hence rng (R ~) = dom R by TARSKI:1; ::_thesis: verum end; theorem :: RELSET_1:12 for X, Y being set holds {} is Relation of X,Y by XBOOLE_1:2; registration let A be empty set ; let B be set ; cluster -> empty for Element of bool [:A,B:]; coherence for b1 being Relation of A,B holds b1 is empty ; cluster -> empty for Element of bool [:B,A:]; coherence for b1 being Relation of B,A holds b1 is empty ; end; theorem Th13: :: RELSET_1:13 for X being set holds id X c= [:X,X:] proof let X be set ; ::_thesis: id X c= [:X,X:] [:X,X:] c= [:X,X:] ; then reconsider R = [:X,X:] as Relation of X,X ; for x, y being set st [x,y] in id X holds [x,y] in R proof let x, y be set ; ::_thesis: ( [x,y] in id X implies [x,y] in R ) assume [x,y] in id X ; ::_thesis: [x,y] in R then ( x in X & x = y ) by RELAT_1:def_10; hence [x,y] in R by ZFMISC_1:87; ::_thesis: verum end; hence id X c= [:X,X:] by RELAT_1:def_3; ::_thesis: verum end; theorem :: RELSET_1:14 for X being set holds id X is Relation of X,X by Th13; theorem Th15: :: RELSET_1:15 for X, Y, A being set for R being Relation of X,Y st id A c= R holds ( A c= dom R & A c= rng R ) proof let X, Y, A be set ; ::_thesis: for R being Relation of X,Y st id A c= R holds ( A c= dom R & A c= rng R ) let R be Relation of X,Y; ::_thesis: ( id A c= R implies ( A c= dom R & A c= rng R ) ) assume A1: id A c= R ; ::_thesis: ( A c= dom R & A c= rng R ) thus A c= dom R ::_thesis: A c= rng R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in dom R ) assume x in A ; ::_thesis: x in dom R then [x,x] in id A by RELAT_1:def_10; hence x in dom R by A1, XTUPLE_0:def_12; ::_thesis: verum end; thus A c= rng R ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng R ) assume x in A ; ::_thesis: x in rng R then [x,x] in id A by RELAT_1:def_10; hence x in rng R by A1, XTUPLE_0:def_13; ::_thesis: verum end; end; theorem :: RELSET_1:16 for Y, X being set for R being Relation of X,Y st id X c= R holds ( X = dom R & X c= rng R ) proof let Y, X be set ; ::_thesis: for R being Relation of X,Y st id X c= R holds ( X = dom R & X c= rng R ) let R be Relation of X,Y; ::_thesis: ( id X c= R implies ( X = dom R & X c= rng R ) ) assume A1: id X c= R ; ::_thesis: ( X = dom R & X c= rng R ) then X c= dom R by Th15; hence X = dom R by XBOOLE_0:def_10; ::_thesis: X c= rng R thus X c= rng R by A1, Th15; ::_thesis: verum end; theorem :: RELSET_1:17 for X, Y being set for R being Relation of X,Y st id Y c= R holds ( Y c= dom R & Y = rng R ) proof let X, Y be set ; ::_thesis: for R being Relation of X,Y st id Y c= R holds ( Y c= dom R & Y = rng R ) let R be Relation of X,Y; ::_thesis: ( id Y c= R implies ( Y c= dom R & Y = rng R ) ) assume A1: id Y c= R ; ::_thesis: ( Y c= dom R & Y = rng R ) hence Y c= dom R by Th15; ::_thesis: Y = rng R Y c= rng R by A1, Th15; hence Y = rng R by XBOOLE_0:def_10; ::_thesis: verum end; definition let X, Y be set ; let R be Relation of X,Y; let A be set ; :: original: | redefine funcR | A -> Relation of X,Y; coherence R | A is Relation of X,Y proof now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_R_|_A_holds_ [x,y]_in_[:X,Y:] let x, y be set ; ::_thesis: ( [x,y] in R | A implies [x,y] in [:X,Y:] ) assume [x,y] in R | A ; ::_thesis: [x,y] in [:X,Y:] then [x,y] in R by RELAT_1:def_11; hence [x,y] in [:X,Y:] ; ::_thesis: verum end; hence R | A is Relation of X,Y by RELAT_1:def_3; ::_thesis: verum end; end; definition let X, Y, B be set ; let R be Relation of X,Y; :: original: |` redefine funcB |` R -> Relation of X,Y; coherence B |` R is Relation of X,Y proof now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_B_|`_R_holds_ [x,y]_in_[:X,Y:] let x, y be set ; ::_thesis: ( [x,y] in B |` R implies [x,y] in [:X,Y:] ) assume [x,y] in B |` R ; ::_thesis: [x,y] in [:X,Y:] then [x,y] in R by RELAT_1:def_12; hence [x,y] in [:X,Y:] ; ::_thesis: verum end; hence B |` R is Relation of X,Y by RELAT_1:def_3; ::_thesis: verum end; end; theorem :: RELSET_1:18 for X, X1, Y being set for R being Relation of X,Y holds R | X1 is Relation of X1,Y proof let X, X1, Y be set ; ::_thesis: for R being Relation of X,Y holds R | X1 is Relation of X1,Y let R be Relation of X,Y; ::_thesis: R | X1 is Relation of X1,Y now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_R_|_X1_holds_ [x,y]_in_[:X1,Y:] let x, y be set ; ::_thesis: ( [x,y] in R | X1 implies [x,y] in [:X1,Y:] ) assume [x,y] in R | X1 ; ::_thesis: [x,y] in [:X1,Y:] then ( x in X1 & y in Y ) by RELAT_1:def_11, ZFMISC_1:87; hence [x,y] in [:X1,Y:] by ZFMISC_1:87; ::_thesis: verum end; hence R | X1 is Relation of X1,Y by RELAT_1:def_3; ::_thesis: verum end; theorem :: RELSET_1:19 for Y, X, X1 being set for R being Relation of X,Y st X c= X1 holds R | X1 = R proof let Y, X, X1 be set ; ::_thesis: for R being Relation of X,Y st X c= X1 holds R | X1 = R let R be Relation of X,Y; ::_thesis: ( X c= X1 implies R | X1 = R ) assume A1: X c= X1 ; ::_thesis: R | X1 = R now__::_thesis:_for_x,_y_being_set_holds_ (_[x,y]_in_R_|_X1_iff_[x,y]_in_R_) let x, y be set ; ::_thesis: ( [x,y] in R | X1 iff [x,y] in R ) now__::_thesis:_(_[x,y]_in_R_implies_[x,y]_in_R_|_X1_) assume A2: [x,y] in R ; ::_thesis: [x,y] in R | X1 then x in X by ZFMISC_1:87; hence [x,y] in R | X1 by A1, A2, RELAT_1:def_11; ::_thesis: verum end; hence ( [x,y] in R | X1 iff [x,y] in R ) by RELAT_1:def_11; ::_thesis: verum end; hence R | X1 = R by RELAT_1:def_2; ::_thesis: verum end; theorem :: RELSET_1:20 for Y, Y1, X being set for R being Relation of X,Y holds Y1 |` R is Relation of X,Y1 proof let Y, Y1, X be set ; ::_thesis: for R being Relation of X,Y holds Y1 |` R is Relation of X,Y1 let R be Relation of X,Y; ::_thesis: Y1 |` R is Relation of X,Y1 now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_Y1_|`_R_holds_ [x,y]_in_[:X,Y1:] let x, y be set ; ::_thesis: ( [x,y] in Y1 |` R implies [x,y] in [:X,Y1:] ) assume [x,y] in Y1 |` R ; ::_thesis: [x,y] in [:X,Y1:] then ( y in Y1 & x in X ) by RELAT_1:def_12, ZFMISC_1:87; hence [x,y] in [:X,Y1:] by ZFMISC_1:87; ::_thesis: verum end; hence Y1 |` R is Relation of X,Y1 by RELAT_1:def_3; ::_thesis: verum end; theorem :: RELSET_1:21 for X, Y, Y1 being set for R being Relation of X,Y st Y c= Y1 holds Y1 |` R = R proof let X, Y, Y1 be set ; ::_thesis: for R being Relation of X,Y st Y c= Y1 holds Y1 |` R = R let R be Relation of X,Y; ::_thesis: ( Y c= Y1 implies Y1 |` R = R ) assume A1: Y c= Y1 ; ::_thesis: Y1 |` R = R now__::_thesis:_for_x,_y_being_set_holds_ (_[x,y]_in_Y1_|`_R_iff_[x,y]_in_R_) let x, y be set ; ::_thesis: ( [x,y] in Y1 |` R iff [x,y] in R ) now__::_thesis:_(_[x,y]_in_R_implies_[x,y]_in_Y1_|`_R_) assume A2: [x,y] in R ; ::_thesis: [x,y] in Y1 |` R then y in Y by ZFMISC_1:87; hence [x,y] in Y1 |` R by A1, A2, RELAT_1:def_12; ::_thesis: verum end; hence ( [x,y] in Y1 |` R iff [x,y] in R ) by RELAT_1:def_12; ::_thesis: verum end; hence Y1 |` R = R by RELAT_1:def_2; ::_thesis: verum end; definition let X, Y be set ; let R be Relation of X,Y; let A be set ; :: original: .: redefine funcR .: A -> Subset of Y; coherence R .: A is Subset of Y proof R .: A c= rng R by RELAT_1:111; hence R .: A is Subset of Y by XBOOLE_1:1; ::_thesis: verum end; :: original: " redefine funcR " A -> Subset of X; coherence R " A is Subset of X proof R " A c= dom R by RELAT_1:132; hence R " A is Subset of X by XBOOLE_1:1; ::_thesis: verum end; end; theorem Th22: :: RELSET_1:22 for X, Y being set for R being Relation of X,Y holds ( R .: X = rng R & R " Y = dom R ) proof let X, Y be set ; ::_thesis: for R being Relation of X,Y holds ( R .: X = rng R & R " Y = dom R ) let R be Relation of X,Y; ::_thesis: ( R .: X = rng R & R " Y = dom R ) now__::_thesis:_for_y_being_set_holds_ (_y_in_R_.:_X_iff_y_in_rng_R_) let y be set ; ::_thesis: ( y in R .: X iff y in rng R ) A1: now__::_thesis:_(_y_in_rng_R_implies_y_in_R_.:_X_) assume y in rng R ; ::_thesis: y in R .: X then consider x being set such that A2: [x,y] in R by XTUPLE_0:def_13; x in X by A2, ZFMISC_1:87; hence y in R .: X by A2, RELAT_1:def_13; ::_thesis: verum end; now__::_thesis:_(_y_in_R_.:_X_implies_y_in_rng_R_) assume y in R .: X ; ::_thesis: y in rng R then ex x being set st ( [x,y] in R & x in X ) by RELAT_1:def_13; hence y in rng R by XTUPLE_0:def_13; ::_thesis: verum end; hence ( y in R .: X iff y in rng R ) by A1; ::_thesis: verum end; hence R .: X = rng R by TARSKI:1; ::_thesis: R " Y = dom R now__::_thesis:_for_x_being_set_holds_ (_x_in_R_"_Y_iff_x_in_dom_R_) let x be set ; ::_thesis: ( x in R " Y iff x in dom R ) A3: now__::_thesis:_(_x_in_dom_R_implies_x_in_R_"_Y_) assume x in dom R ; ::_thesis: x in R " Y then consider y being set such that A4: [x,y] in R by XTUPLE_0:def_12; y in Y by A4, ZFMISC_1:87; hence x in R " Y by A4, RELAT_1:def_14; ::_thesis: verum end; now__::_thesis:_(_x_in_R_"_Y_implies_x_in_dom_R_) assume x in R " Y ; ::_thesis: x in dom R then ex y being set st ( [x,y] in R & y in Y ) by RELAT_1:def_14; hence x in dom R by XTUPLE_0:def_12; ::_thesis: verum end; hence ( x in R " Y iff x in dom R ) by A3; ::_thesis: verum end; hence R " Y = dom R by TARSKI:1; ::_thesis: verum end; theorem :: RELSET_1:23 for Y, X being set for R being Relation of X,Y holds ( R .: (R " Y) = rng R & R " (R .: X) = dom R ) proof let Y, X be set ; ::_thesis: for R being Relation of X,Y holds ( R .: (R " Y) = rng R & R " (R .: X) = dom R ) let R be Relation of X,Y; ::_thesis: ( R .: (R " Y) = rng R & R " (R .: X) = dom R ) ( R " Y = dom R & R .: X = rng R ) by Th22; hence ( R .: (R " Y) = rng R & R " (R .: X) = dom R ) by RELAT_1:113, RELAT_1:134; ::_thesis: verum end; scheme :: RELSET_1:sch 1 RelOnSetEx{ F1() -> set , F2() -> set , P1[ set , set ] } : ex R being Relation of F1(),F2() st for x, y being set holds ( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) ) proof consider R being Relation such that A1: for x, y being set holds ( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) ) from RELAT_1:sch_1(); R c= [:F1(),F2():] proof let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in R or [x1,x2] in [:F1(),F2():] ) assume [x1,x2] in R ; ::_thesis: [x1,x2] in [:F1(),F2():] then ( x1 in F1() & x2 in F2() ) by A1; hence [x1,x2] in [:F1(),F2():] by ZFMISC_1:87; ::_thesis: verum end; then reconsider R = R as Relation of F1(),F2() ; take R ; ::_thesis: for x, y being set holds ( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) ) thus for x, y being set holds ( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) ) by A1; ::_thesis: verum end; definition let X be set ; mode Relation of X is Relation of X,X; end; registration let D be non empty set ; cluster id D -> non empty ; coherence not id D is empty proof now__::_thesis:_not_id_D_=_{} set y = the Element of D; A1: [ the Element of D, the Element of D] in id D by RELAT_1:def_10; assume id D = {} ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; hence not id D is empty ; ::_thesis: verum end; end; theorem :: RELSET_1:24 for D, E being non empty set for R being Relation of D,E for x being Element of D holds ( x in dom R iff ex y being Element of E st [x,y] in R ) proof let D, E be non empty set ; ::_thesis: for R being Relation of D,E for x being Element of D holds ( x in dom R iff ex y being Element of E st [x,y] in R ) let R be Relation of D,E; ::_thesis: for x being Element of D holds ( x in dom R iff ex y being Element of E st [x,y] in R ) let x be Element of D; ::_thesis: ( x in dom R iff ex y being Element of E st [x,y] in R ) thus ( x in dom R implies ex y being Element of E st [x,y] in R ) ::_thesis: ( ex y being Element of E st [x,y] in R implies x in dom R ) proof assume x in dom R ; ::_thesis: ex y being Element of E st [x,y] in R then consider y being set such that A1: [x,y] in R by XTUPLE_0:def_12; reconsider b = y as Element of E by A1, ZFMISC_1:87; take b ; ::_thesis: [x,b] in R thus [x,b] in R by A1; ::_thesis: verum end; given y being Element of E such that A2: [x,y] in R ; ::_thesis: x in dom R thus x in dom R by A2, XTUPLE_0:def_12; ::_thesis: verum end; theorem :: RELSET_1:25 for E, D being non empty set for R being Relation of D,E for y being set holds ( y in rng R iff ex x being Element of D st [x,y] in R ) proof let E, D be non empty set ; ::_thesis: for R being Relation of D,E for y being set holds ( y in rng R iff ex x being Element of D st [x,y] in R ) let R be Relation of D,E; ::_thesis: for y being set holds ( y in rng R iff ex x being Element of D st [x,y] in R ) let y be set ; ::_thesis: ( y in rng R iff ex x being Element of D st [x,y] in R ) thus ( y in rng R implies ex x being Element of D st [x,y] in R ) ::_thesis: ( ex x being Element of D st [x,y] in R implies y in rng R ) proof assume y in rng R ; ::_thesis: ex x being Element of D st [x,y] in R then consider x being set such that A1: [x,y] in R by XTUPLE_0:def_13; reconsider a = x as Element of D by A1, ZFMISC_1:87; take a ; ::_thesis: [a,y] in R thus [a,y] in R by A1; ::_thesis: verum end; given x being Element of D such that A2: [x,y] in R ; ::_thesis: y in rng R thus y in rng R by A2, XTUPLE_0:def_13; ::_thesis: verum end; theorem :: RELSET_1:26 for D, E being non empty set for R being Relation of D,E st dom R <> {} holds ex y being Element of E st y in rng R proof let D, E be non empty set ; ::_thesis: for R being Relation of D,E st dom R <> {} holds ex y being Element of E st y in rng R let R be Relation of D,E; ::_thesis: ( dom R <> {} implies ex y being Element of E st y in rng R ) assume dom R <> {} ; ::_thesis: ex y being Element of E st y in rng R then rng R <> {} by RELAT_1:42; then ex y being set st y in rng R by XBOOLE_0:def_1; hence ex y being Element of E st y in rng R ; ::_thesis: verum end; theorem :: RELSET_1:27 for E, D being non empty set for R being Relation of D,E st rng R <> {} holds ex x being Element of D st x in dom R proof let E, D be non empty set ; ::_thesis: for R being Relation of D,E st rng R <> {} holds ex x being Element of D st x in dom R let R be Relation of D,E; ::_thesis: ( rng R <> {} implies ex x being Element of D st x in dom R ) assume rng R <> {} ; ::_thesis: ex x being Element of D st x in dom R then dom R <> {} by RELAT_1:42; then ex x being set st x in dom R by XBOOLE_0:def_1; hence ex x being Element of D st x in dom R ; ::_thesis: verum end; theorem :: RELSET_1:28 for D, E, F being non empty set for P being Relation of D,E for R being Relation of E,F for x, z being set holds ( [x,z] in P * R iff ex y being Element of E st ( [x,y] in P & [y,z] in R ) ) proof let D, E, F be non empty set ; ::_thesis: for P being Relation of D,E for R being Relation of E,F for x, z being set holds ( [x,z] in P * R iff ex y being Element of E st ( [x,y] in P & [y,z] in R ) ) let P be Relation of D,E; ::_thesis: for R being Relation of E,F for x, z being set holds ( [x,z] in P * R iff ex y being Element of E st ( [x,y] in P & [y,z] in R ) ) let R be Relation of E,F; ::_thesis: for x, z being set holds ( [x,z] in P * R iff ex y being Element of E st ( [x,y] in P & [y,z] in R ) ) let x, z be set ; ::_thesis: ( [x,z] in P * R iff ex y being Element of E st ( [x,y] in P & [y,z] in R ) ) thus ( [x,z] in P * R implies ex y being Element of E st ( [x,y] in P & [y,z] in R ) ) ::_thesis: ( ex y being Element of E st ( [x,y] in P & [y,z] in R ) implies [x,z] in P * R ) proof assume [x,z] in P * R ; ::_thesis: ex y being Element of E st ( [x,y] in P & [y,z] in R ) then consider y being set such that A1: [x,y] in P and A2: [y,z] in R by RELAT_1:def_8; reconsider a = y as Element of E by A1, ZFMISC_1:87; take a ; ::_thesis: ( [x,a] in P & [a,z] in R ) thus ( [x,a] in P & [a,z] in R ) by A1, A2; ::_thesis: verum end; given y being Element of E such that A3: ( [x,y] in P & [y,z] in R ) ; ::_thesis: [x,z] in P * R thus [x,z] in P * R by A3, RELAT_1:def_8; ::_thesis: verum end; theorem :: RELSET_1:29 for E, D1, D being non empty set for R being Relation of D,E for y being Element of E holds ( y in R .: D1 iff ex x being Element of D st ( [x,y] in R & x in D1 ) ) proof let E, D1, D be non empty set ; ::_thesis: for R being Relation of D,E for y being Element of E holds ( y in R .: D1 iff ex x being Element of D st ( [x,y] in R & x in D1 ) ) let R be Relation of D,E; ::_thesis: for y being Element of E holds ( y in R .: D1 iff ex x being Element of D st ( [x,y] in R & x in D1 ) ) let y be Element of E; ::_thesis: ( y in R .: D1 iff ex x being Element of D st ( [x,y] in R & x in D1 ) ) thus ( y in R .: D1 implies ex x being Element of D st ( [x,y] in R & x in D1 ) ) ::_thesis: ( ex x being Element of D st ( [x,y] in R & x in D1 ) implies y in R .: D1 ) proof assume y in R .: D1 ; ::_thesis: ex x being Element of D st ( [x,y] in R & x in D1 ) then consider x being set such that A1: [x,y] in R and A2: x in D1 by RELAT_1:def_13; reconsider a = x as Element of D by A1, ZFMISC_1:87; take a ; ::_thesis: ( [a,y] in R & a in D1 ) thus ( [a,y] in R & a in D1 ) by A1, A2; ::_thesis: verum end; given x being Element of D such that A3: ( [x,y] in R & x in D1 ) ; ::_thesis: y in R .: D1 thus y in R .: D1 by A3, RELAT_1:def_13; ::_thesis: verum end; theorem :: RELSET_1:30 for D, D2, E being non empty set for R being Relation of D,E for x being Element of D holds ( x in R " D2 iff ex y being Element of E st ( [x,y] in R & y in D2 ) ) proof let D, D2, E be non empty set ; ::_thesis: for R being Relation of D,E for x being Element of D holds ( x in R " D2 iff ex y being Element of E st ( [x,y] in R & y in D2 ) ) let R be Relation of D,E; ::_thesis: for x being Element of D holds ( x in R " D2 iff ex y being Element of E st ( [x,y] in R & y in D2 ) ) let x be Element of D; ::_thesis: ( x in R " D2 iff ex y being Element of E st ( [x,y] in R & y in D2 ) ) thus ( x in R " D2 implies ex y being Element of E st ( [x,y] in R & y in D2 ) ) ::_thesis: ( ex y being Element of E st ( [x,y] in R & y in D2 ) implies x in R " D2 ) proof assume x in R " D2 ; ::_thesis: ex y being Element of E st ( [x,y] in R & y in D2 ) then consider y being set such that A1: [x,y] in R and A2: y in D2 by RELAT_1:def_14; reconsider b = y as Element of E by A1, ZFMISC_1:87; take b ; ::_thesis: ( [x,b] in R & b in D2 ) thus ( [x,b] in R & b in D2 ) by A1, A2; ::_thesis: verum end; given y being Element of E such that A3: ( [x,y] in R & y in D2 ) ; ::_thesis: x in R " D2 thus x in R " D2 by A3, RELAT_1:def_14; ::_thesis: verum end; scheme :: RELSET_1:sch 2 RelOnDomEx{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } : ex R being Relation of F1(),F2() st for x being Element of F1() for y being Element of F2() holds ( [x,y] in R iff P1[x,y] ) proof consider R being Relation of F1(),F2() such that A1: for x, y being set holds ( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) ) from RELSET_1:sch_1(); take R ; ::_thesis: for x being Element of F1() for y being Element of F2() holds ( [x,y] in R iff P1[x,y] ) thus for x being Element of F1() for y being Element of F2() holds ( [x,y] in R iff P1[x,y] ) by A1; ::_thesis: verum end; begin scheme :: RELSET_1:sch 3 Sch3{ F1() -> set , F2() -> Subset of F1(), F3( set ) -> set } : ex R being Relation of F2() st for i being Element of F1() st i in F2() holds Im (R,i) = F3(i) provided A1: for i being Element of F1() st i in F2() holds F3(i) c= F2() proof defpred S1[ set , set ] means \$2 in F3(\$1); consider R being Relation of F2() such that A2: for x, y being set holds ( [x,y] in R iff ( x in F2() & y in F2() & S1[x,y] ) ) from RELSET_1:sch_1(); take R ; ::_thesis: for i being Element of F1() st i in F2() holds Im (R,i) = F3(i) let i be Element of F1(); ::_thesis: ( i in F2() implies Im (R,i) = F3(i) ) assume A3: i in F2() ; ::_thesis: Im (R,i) = F3(i) thus Im (R,i) c= F3(i) :: according to XBOOLE_0:def_10 ::_thesis: F3(i) c= Im (R,i) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Im (R,i) or e in F3(i) ) assume e in Im (R,i) ; ::_thesis: e in F3(i) then consider u being set such that A4: [u,e] in R and A5: u in {i} by RELAT_1:def_13; u = i by A5, TARSKI:def_1; hence e in F3(i) by A2, A4; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F3(i) or e in Im (R,i) ) assume A6: e in F3(i) ; ::_thesis: e in Im (R,i) F3(i) c= F2() by A1, A3; then ( i in {i} & [i,e] in R ) by A2, A3, A6, TARSKI:def_1; hence e in Im (R,i) by RELAT_1:def_13; ::_thesis: verum end; theorem :: RELSET_1:31 for N being set for R, S being Relation of N st ( for i being set st i in N holds Im (R,i) = Im (S,i) ) holds R = S proof let N be set ; ::_thesis: for R, S being Relation of N st ( for i being set st i in N holds Im (R,i) = Im (S,i) ) holds R = S let R, S be Relation of N; ::_thesis: ( ( for i being set st i in N holds Im (R,i) = Im (S,i) ) implies R = S ) assume A1: for i being set st i in N holds Im (R,i) = Im (S,i) ; ::_thesis: R = S let a, b be Element of N; :: according to RELSET_1:def_2 ::_thesis: ( [a,b] in R iff [a,b] in S ) thus ( [a,b] in R implies [a,b] in S ) ::_thesis: ( [a,b] in S implies [a,b] in R ) proof assume A2: [a,b] in R ; ::_thesis: [a,b] in S then A3: a in dom R by XTUPLE_0:def_12; a in {a} by TARSKI:def_1; then b in Im (R,a) by A2, RELAT_1:def_13; then b in Im (S,a) by A1, A3; then ex e being set st ( [e,b] in S & e in {a} ) by RELAT_1:def_13; hence [a,b] in S by TARSKI:def_1; ::_thesis: verum end; assume A4: [a,b] in S ; ::_thesis: [a,b] in R then A5: a in dom S by XTUPLE_0:def_12; a in {a} by TARSKI:def_1; then b in Im (S,a) by A4, RELAT_1:def_13; then b in Im (R,a) by A1, A5; then ex e being set st ( [e,b] in R & e in {a} ) by RELAT_1:def_13; hence [a,b] in R by TARSKI:def_1; ::_thesis: verum end; scheme :: RELSET_1:sch 4 Sch4{ F1() -> set , F2() -> set , P1[ set , set ], F3() -> Relation of F1(),F2(), F4() -> Relation of F1(),F2() } : F3() = F4() provided A1: for p being Element of F1() for q being Element of F2() holds ( [p,q] in F3() iff P1[p,q] ) and A2: for p being Element of F1() for q being Element of F2() holds ( [p,q] in F4() iff P1[p,q] ) proof let y be Element of F1(); :: according to RELSET_1:def_2 ::_thesis: for y being Element of F2() holds ( [y,y] in F3() iff [y,y] in F4() ) let z be Element of F2(); ::_thesis: ( [y,z] in F3() iff [y,z] in F4() ) ( [y,z] in F3() iff P1[y,z] ) by A1; hence ( [y,z] in F3() iff [y,z] in F4() ) by A2; ::_thesis: verum end; registration let X, Y, Z be set ; let f be Relation of [:X,Y:],Z; cluster dom f -> Relation-like ; coherence dom f is Relation-like ; end; registration let X, Y, Z be set ; let f be Relation of X,[:Y,Z:]; cluster rng f -> Relation-like ; coherence rng f is Relation-like ; end; theorem :: RELSET_1:32 for Y, A, X being set for P being Relation of X,Y st A misses X holds P | A = {} proof let Y, A, X be set ; ::_thesis: for P being Relation of X,Y st A misses X holds P | A = {} let P be Relation of X,Y; ::_thesis: ( A misses X implies P | A = {} ) assume A misses X ; ::_thesis: P | A = {} then A misses dom P by XBOOLE_1:63; hence P | A = {} by RELAT_1:152; ::_thesis: verum end; registration let R be non empty Relation; let Y be non empty Subset of (dom R); clusterR | Y -> non empty ; coherence not R | Y is empty proof dom (R | Y) = Y by RELAT_1:62; hence not R | Y is empty ; ::_thesis: verum end; end; registration let R be non empty Relation; let Y be non empty Subset of (dom R); clusterR .: Y -> non empty ; coherence not R .: Y is empty proof R .: Y = rng (R | Y) by RELAT_1:115; hence not R .: Y is empty ; ::_thesis: verum end; end; registration let X, Y be set ; cluster empty Relation-like X -defined Y -valued for Element of bool [:X,Y:]; existence ex b1 being Relation of X,Y st b1 is empty proof {} is Relation of X,Y by XBOOLE_1:2; hence ex b1 being Relation of X,Y st b1 is empty ; ::_thesis: verum end; end;