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