:: SYSREL semantic presentation
begin
Lm1: for X, Y being set st X <> {} & Y <> {} holds
( dom [:X,Y:] = X & rng [:X,Y:] = Y )
by RELAT_1:160;
theorem Th1: :: SYSREL:1
for X, Y being set
for R being Relation holds
( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
proof
let X, Y be set ; ::_thesis: for R being Relation holds
( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
let R be Relation; ::_thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
percases ( X = {} or Y = {} or ( X <> {} & Y <> {} ) ) ;
suppose ( X = {} or Y = {} ) ; ::_thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
then R /\ [:X,Y:] = R /\ {} by ZFMISC_1:90
.= {} ;
hence ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y ) by RELAT_1:38, XBOOLE_1:2; ::_thesis: verum
end;
supposeA1: ( X <> {} & Y <> {} ) ; ::_thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
rng (R /\ [:X,Y:]) c= (rng R) /\ (rng [:X,Y:]) by RELAT_1:13;
then A2: rng (R /\ [:X,Y:]) c= (rng R) /\ Y by A1, Lm1;
dom (R /\ [:X,Y:]) c= (dom R) /\ (dom [:X,Y:]) by RELAT_1:2;
then A3: dom (R /\ [:X,Y:]) c= (dom R) /\ X by A1, Lm1;
(dom R) /\ X c= X by XBOOLE_1:17;
hence dom (R /\ [:X,Y:]) c= X by A3, XBOOLE_1:1; ::_thesis: rng (R /\ [:X,Y:]) c= Y
(rng R) /\ Y c= Y by XBOOLE_1:17;
hence rng (R /\ [:X,Y:]) c= Y by A2, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
theorem :: SYSREL:2
for X, Y being set
for R being Relation st X misses Y holds
dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:])
proof
let X, Y be set ; ::_thesis: for R being Relation st X misses Y holds
dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:])
let R be Relation; ::_thesis: ( X misses Y implies dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:]) )
assume A1: X /\ Y = {} ; :: according to XBOOLE_0:def_7 ::_thesis: dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:])
dom (R /\ [:X,Y:]) c= X by Th1;
then A2: (dom (R /\ [:X,Y:])) /\ (rng (R /\ [:X,Y:])) c= X /\ (rng (R /\ [:X,Y:])) by XBOOLE_1:26;
X /\ (rng (R /\ [:X,Y:])) c= X /\ Y by Th1, XBOOLE_1:26;
hence (dom (R /\ [:X,Y:])) /\ (rng (R /\ [:X,Y:])) = {} by A1, A2, XBOOLE_1:1, XBOOLE_1:3; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
theorem Th3: :: SYSREL:3
for X, Y being set
for R being Relation st R c= [:X,Y:] holds
( dom R c= X & rng R c= Y )
proof
let X, Y be set ; ::_thesis: for R being Relation st R c= [:X,Y:] holds
( dom R c= X & rng R c= Y )
let R be Relation; ::_thesis: ( R c= [:X,Y:] implies ( dom R c= X & rng R c= Y ) )
assume R c= [:X,Y:] ; ::_thesis: ( dom R c= X & rng R c= Y )
then R /\ [:X,Y:] = R by XBOOLE_1:28;
hence ( dom R c= X & rng R c= Y ) by Th1; ::_thesis: verum
end;
theorem :: SYSREL:4
for X, Y being set
for R being Relation st R c= [:X,Y:] holds
R ~ c= [:Y,X:]
proof
let X, Y be set ; ::_thesis: for R being Relation st R c= [:X,Y:] holds
R ~ c= [:Y,X:]
let R be Relation; ::_thesis: ( R c= [:X,Y:] implies R ~ c= [:Y,X:] )
assume A1: R c= [:X,Y:] ; ::_thesis: R ~ c= [:Y,X:]
let z be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [z,b1] in R ~ or [z,b1] in [:Y,X:] )
let t be set ; ::_thesis: ( not [z,t] in R ~ or [z,t] in [:Y,X:] )
assume [z,t] in R ~ ; ::_thesis: [z,t] in [:Y,X:]
then [t,z] in R by RELAT_1:def_7;
then ( t in X & z in Y ) by A1, ZFMISC_1:87;
hence [z,t] in [:Y,X:] by ZFMISC_1:87; ::_thesis: verum
end;
theorem :: SYSREL:5
for X, Y being set holds [:X,Y:] ~ = [:Y,X:]
proof
let X, Y be set ; ::_thesis: [:X,Y:] ~ = [:Y,X:]
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in [:X,Y:] ~ or [x,b1] in [:Y,X:] ) & ( not [x,b1] in [:Y,X:] or [x,b1] in [:X,Y:] ~ ) )
let y be set ; ::_thesis: ( ( not [x,y] in [:X,Y:] ~ or [x,y] in [:Y,X:] ) & ( not [x,y] in [:Y,X:] or [x,y] in [:X,Y:] ~ ) )
thus ( [x,y] in [:X,Y:] ~ implies [x,y] in [:Y,X:] ) ::_thesis: ( not [x,y] in [:Y,X:] or [x,y] in [:X,Y:] ~ )
proof
assume [x,y] in [:X,Y:] ~ ; ::_thesis: [x,y] in [:Y,X:]
then [y,x] in [:X,Y:] by RELAT_1:def_7;
then ( y in X & x in Y ) by ZFMISC_1:87;
hence [x,y] in [:Y,X:] by ZFMISC_1:87; ::_thesis: verum
end;
assume [x,y] in [:Y,X:] ; ::_thesis: [x,y] in [:X,Y:] ~
then ( y in X & x in Y ) by ZFMISC_1:87;
then [y,x] in [:X,Y:] by ZFMISC_1:87;
hence [x,y] in [:X,Y:] ~ by RELAT_1:def_7; ::_thesis: verum
end;
theorem Th6: :: SYSREL:6
for R, S, T being Relation holds (R \/ S) * T = (R * T) \/ (S * T)
proof
let R, S, T be Relation; ::_thesis: (R \/ S) * T = (R * T) \/ (S * T)
thus (R \/ S) * T = (R * T) \/ (S * T) ::_thesis: verum
proof
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in (R \/ S) * T or [x,b1] in (R * T) \/ (S * T) ) & ( not [x,b1] in (R * T) \/ (S * T) or [x,b1] in (R \/ S) * T ) )
let y be set ; ::_thesis: ( ( not [x,y] in (R \/ S) * T or [x,y] in (R * T) \/ (S * T) ) & ( not [x,y] in (R * T) \/ (S * T) or [x,y] in (R \/ S) * T ) )
thus ( [x,y] in (R \/ S) * T implies [x,y] in (R * T) \/ (S * T) ) ::_thesis: ( not [x,y] in (R * T) \/ (S * T) or [x,y] in (R \/ S) * T )
proof
assume [x,y] in (R \/ S) * T ; ::_thesis: [x,y] in (R * T) \/ (S * T)
then consider z being set such that
A1: ( [x,z] in R \/ S & [z,y] in T ) by RELAT_1:def_8;
( ( [x,z] in R & [z,y] in T ) or ( [x,z] in S & [z,y] in T ) ) by A1, XBOOLE_0:def_3;
then ( [x,y] in R * T or [x,y] in S * T ) by RELAT_1:def_8;
hence [x,y] in (R * T) \/ (S * T) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume A2: [x,y] in (R * T) \/ (S * T) ; ::_thesis: [x,y] in (R \/ S) * T
percases ( [x,y] in S * T or [x,y] in R * T ) by A2, XBOOLE_0:def_3;
suppose [x,y] in S * T ; ::_thesis: [x,y] in (R \/ S) * T
then consider z being set such that
A3: [x,z] in S and
A4: [z,y] in T by RELAT_1:def_8;
[x,z] in R \/ S by A3, XBOOLE_0:def_3;
hence [x,y] in (R \/ S) * T by A4, RELAT_1:def_8; ::_thesis: verum
end;
suppose [x,y] in R * T ; ::_thesis: [x,y] in (R \/ S) * T
then consider z being set such that
A5: [x,z] in R and
A6: [z,y] in T by RELAT_1:def_8;
[x,z] in R \/ S by A5, XBOOLE_0:def_3;
hence [x,y] in (R \/ S) * T by A6, RELAT_1:def_8; ::_thesis: verum
end;
end;
end;
end;
theorem :: SYSREL:7
for X, Y, x, y being set
for R being Relation holds
( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
proof
let X, Y, x, y be set ; ::_thesis: for R being Relation holds
( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
let R be Relation; ::_thesis: ( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
thus ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) ::_thesis: ( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
proof
assume that
A1: X misses Y and
A2: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A3: x in X ; ::_thesis: ( not x in Y & not y in X & y in Y )
A4: not [x,y] in [:Y,X:]
proof
assume A5: [x,y] in [:Y,X:] ; ::_thesis: contradiction
not x in Y by A1, A3, XBOOLE_0:3;
hence contradiction by A5, ZFMISC_1:87; ::_thesis: verum
end;
A6: ( [x,y] in [:X,Y:] implies ( not x in Y & not y in X & y in Y ) )
proof
assume [x,y] in [:X,Y:] ; ::_thesis: ( not x in Y & not y in X & y in Y )
then ( x in X & y in Y ) by ZFMISC_1:87;
hence ( not x in Y & not y in X & y in Y ) by A1, XBOOLE_0:3; ::_thesis: verum
end;
[:X,Y:] misses [:Y,X:] by A1, ZFMISC_1:104;
hence ( not x in Y & not y in X & y in Y ) by A2, A6, A4, XBOOLE_0:5; ::_thesis: verum
end;
thus ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) ::_thesis: ( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
proof
assume that
A7: X misses Y and
A8: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A9: y in Y ; ::_thesis: ( not y in X & not x in Y & x in X )
A10: not [x,y] in [:Y,X:]
proof
assume A11: [x,y] in [:Y,X:] ; ::_thesis: contradiction
not y in X by A7, A9, XBOOLE_0:3;
hence contradiction by A11, ZFMISC_1:87; ::_thesis: verum
end;
( [x,y] in [:X,Y:] implies ( not y in X & not x in Y & x in X ) )
proof
assume [x,y] in [:X,Y:] ; ::_thesis: ( not y in X & not x in Y & x in X )
then ( x in X & y in Y ) by ZFMISC_1:87;
hence ( not y in X & not x in Y & x in X ) by A7, XBOOLE_0:3; ::_thesis: verum
end;
hence ( not y in X & not x in Y & x in X ) by A8, A10, XBOOLE_0:def_3; ::_thesis: verum
end;
thus ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) ::_thesis: ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) )
proof
assume that
A12: X misses Y and
A13: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A14: x in Y ; ::_thesis: ( not x in X & not y in Y & y in X )
A15: not [x,y] in [:X,Y:]
proof
assume A16: [x,y] in [:X,Y:] ; ::_thesis: contradiction
not x in X by A12, A14, XBOOLE_0:3;
hence contradiction by A16, ZFMISC_1:87; ::_thesis: verum
end;
( [x,y] in [:Y,X:] & not [x,y] in [:X,Y:] implies ( not x in X & not y in Y & y in X ) )
proof
assume ( [x,y] in [:Y,X:] & not [x,y] in [:X,Y:] ) ; ::_thesis: ( not x in X & not y in Y & y in X )
then ( ( x in Y & y in X & not x in X ) or ( x in Y & y in X & not y in Y ) ) by ZFMISC_1:87;
hence ( not x in X & not y in Y & y in X ) by A12, XBOOLE_0:3; ::_thesis: verum
end;
hence ( not x in X & not y in Y & y in X ) by A13, A15, XBOOLE_0:def_3; ::_thesis: verum
end;
assume that
A17: X misses Y and
A18: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A19: y in X ; ::_thesis: ( not x in X & not y in Y & x in Y )
A20: not [x,y] in [:X,Y:]
proof
assume A21: [x,y] in [:X,Y:] ; ::_thesis: contradiction
not y in Y by A17, A19, XBOOLE_0:3;
hence contradiction by A21, ZFMISC_1:87; ::_thesis: verum
end;
( [x,y] in [:Y,X:] implies ( not x in X & not y in Y & x in Y ) )
proof
assume [x,y] in [:Y,X:] ; ::_thesis: ( not x in X & not y in Y & x in Y )
then ( x in Y & y in X ) by ZFMISC_1:87;
hence ( not x in X & not y in Y & x in Y ) by A17, XBOOLE_0:3; ::_thesis: verum
end;
hence ( not x in X & not y in Y & x in Y ) by A18, A20, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th8: :: SYSREL:8
for X, Y, Z being set
for R being Relation st R c= [:X,Y:] holds
( R | Z = R /\ [:Z,Y:] & Z |` R = R /\ [:X,Z:] )
proof
let X, Y, Z be set ; ::_thesis: for R being Relation st R c= [:X,Y:] holds
( R | Z = R /\ [:Z,Y:] & Z |` R = R /\ [:X,Z:] )
let R be Relation; ::_thesis: ( R c= [:X,Y:] implies ( R | Z = R /\ [:Z,Y:] & Z |` R = R /\ [:X,Z:] ) )
assume A1: R c= [:X,Y:] ; ::_thesis: ( R | Z = R /\ [:Z,Y:] & Z |` R = R /\ [:X,Z:] )
thus R | Z = R /\ [:Z,Y:] ::_thesis: Z |` R = R /\ [:X,Z:]
proof
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in R | Z or [x,b1] in R /\ [:Z,Y:] ) & ( not [x,b1] in R /\ [:Z,Y:] or [x,b1] in R | Z ) )
let y be set ; ::_thesis: ( ( not [x,y] in R | Z or [x,y] in R /\ [:Z,Y:] ) & ( not [x,y] in R /\ [:Z,Y:] or [x,y] in R | Z ) )
thus ( [x,y] in R | Z implies [x,y] in R /\ [:Z,Y:] ) ::_thesis: ( not [x,y] in R /\ [:Z,Y:] or [x,y] in R | Z )
proof
assume A2: [x,y] in R | Z ; ::_thesis: [x,y] in R /\ [:Z,Y:]
then A3: x in Z by RELAT_1:def_11;
A4: [x,y] in R by A2, RELAT_1:def_11;
then y in Y by A1, ZFMISC_1:87;
then [x,y] in [:Z,Y:] by A3, ZFMISC_1:87;
hence [x,y] in R /\ [:Z,Y:] by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
thus ( [x,y] in R /\ [:Z,Y:] implies [x,y] in R | Z ) ::_thesis: verum
proof
assume A5: [x,y] in R /\ [:Z,Y:] ; ::_thesis: [x,y] in R | Z
then [x,y] in [:Z,Y:] by XBOOLE_0:def_4;
then A6: x in Z by ZFMISC_1:87;
[x,y] in R by A5, XBOOLE_0:def_4;
hence [x,y] in R | Z by A6, RELAT_1:def_11; ::_thesis: verum
end;
end;
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in Z |` R or [x,b1] in R /\ [:X,Z:] ) & ( not [x,b1] in R /\ [:X,Z:] or [x,b1] in Z |` R ) )
let y be set ; ::_thesis: ( ( not [x,y] in Z |` R or [x,y] in R /\ [:X,Z:] ) & ( not [x,y] in R /\ [:X,Z:] or [x,y] in Z |` R ) )
thus ( [x,y] in Z |` R implies [x,y] in R /\ [:X,Z:] ) ::_thesis: ( not [x,y] in R /\ [:X,Z:] or [x,y] in Z |` R )
proof
assume A7: [x,y] in Z |` R ; ::_thesis: [x,y] in R /\ [:X,Z:]
then A8: y in Z by RELAT_1:def_12;
A9: [x,y] in R by A7, RELAT_1:def_12;
then x in X by A1, ZFMISC_1:87;
then [x,y] in [:X,Z:] by A8, ZFMISC_1:87;
hence [x,y] in R /\ [:X,Z:] by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A10: [x,y] in R /\ [:X,Z:] ; ::_thesis: [x,y] in Z |` R
then [x,y] in [:X,Z:] by XBOOLE_0:def_4;
then A11: y in Z by ZFMISC_1:87;
[x,y] in R by A10, XBOOLE_0:def_4;
hence [x,y] in Z |` R by A11, RELAT_1:def_12; ::_thesis: verum
end;
theorem :: SYSREL:9
for X, Y, Z, W being set
for R being Relation st R c= [:X,Y:] & X = Z \/ W holds
R = (R | Z) \/ (R | W)
proof
let X, Y, Z, W be set ; ::_thesis: for R being Relation st R c= [:X,Y:] & X = Z \/ W holds
R = (R | Z) \/ (R | W)
let R be Relation; ::_thesis: ( R c= [:X,Y:] & X = Z \/ W implies R = (R | Z) \/ (R | W) )
assume that
A1: R c= [:X,Y:] and
A2: X = Z \/ W ; ::_thesis: R = (R | Z) \/ (R | W)
thus R = R /\ [:X,Y:] by A1, XBOOLE_1:28
.= R /\ ([:Z,Y:] \/ [:W,Y:]) by A2, ZFMISC_1:97
.= (R /\ [:Z,Y:]) \/ (R /\ [:W,Y:]) by XBOOLE_1:23
.= (R | Z) \/ (R /\ [:W,Y:]) by A1, Th8
.= (R | Z) \/ (R | W) by A1, Th8 ; ::_thesis: verum
end;
theorem :: SYSREL:10
for X, Y being set
for R being Relation st X misses Y & R c= [:X,Y:] \/ [:Y,X:] holds
R | X c= [:X,Y:]
proof
let X, Y be set ; ::_thesis: for R being Relation st X misses Y & R c= [:X,Y:] \/ [:Y,X:] holds
R | X c= [:X,Y:]
let R be Relation; ::_thesis: ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] implies R | X c= [:X,Y:] )
assume that
A1: X /\ Y = {} and
A2: R c= [:X,Y:] \/ [:Y,X:] ; :: according to XBOOLE_0:def_7 ::_thesis: R | X c= [:X,Y:]
R | X = R /\ [:X,(rng R):] by RELAT_1:67;
then R | X c= ([:X,Y:] \/ [:Y,X:]) /\ [:X,(rng R):] by A2, XBOOLE_1:26;
then A3: R | X c= ([:X,Y:] /\ [:X,(rng R):]) \/ ([:Y,X:] /\ [:X,(rng R):]) by XBOOLE_1:23;
[:Y,X:] /\ [:X,(rng R):] = [:(X /\ Y),(X /\ (rng R)):] by ZFMISC_1:100
.= {} by A1, ZFMISC_1:90 ;
hence R | X c= [:X,Y:] by A3, XBOOLE_1:18; ::_thesis: verum
end;
theorem :: SYSREL:11
for R, S being Relation st R c= S holds
R ~ c= S ~
proof
let R, S be Relation; ::_thesis: ( R c= S implies R ~ c= S ~ )
assume R c= S ; ::_thesis: R ~ c= S ~
then R \/ S = S by XBOOLE_1:12;
then (R ~) \/ (S ~) = S ~ by RELAT_1:23;
hence R ~ c= S ~ by XBOOLE_1:7; ::_thesis: verum
end;
Lm2: for X being set holds id X c= [:X,X:]
proof
let X be set ; ::_thesis: id X c= [:X,X:]
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in id X or [x,b1] in [:X,X:] )
let y be set ; ::_thesis: ( not [x,y] in id X or [x,y] in [:X,X:] )
assume [x,y] in id X ; ::_thesis: [x,y] in [:X,X:]
then ( x in X & x = y ) by RELAT_1:def_10;
hence [x,y] in [:X,X:] by ZFMISC_1:87; ::_thesis: verum
end;
theorem Th12: :: SYSREL:12
for X being set holds (id X) * (id X) = id X
proof
let X be set ; ::_thesis: (id X) * (id X) = id X
dom (id X) = X ;
hence (id X) * (id X) = id X by RELAT_1:51; ::_thesis: verum
end;
theorem :: SYSREL:13
for x being set holds id {x} = {[x,x]}
proof
let x be set ; ::_thesis: id {x} = {[x,x]}
x in {x} by TARSKI:def_1;
then [x,x] in id {x} by RELAT_1:def_10;
then A1: {[x,x]} c= id {x} by ZFMISC_1:31;
[:{x},{x}:] = {[x,x]} by ZFMISC_1:29;
then id {x} c= {[x,x]} by Lm2;
hence id {x} = {[x,x]} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th14: :: SYSREL:14
for X, Y being set holds
( id (X \/ Y) = (id X) \/ (id Y) & id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )
proof
let X, Y be set ; ::_thesis: ( id (X \/ Y) = (id X) \/ (id Y) & id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )
thus id (X \/ Y) = (id X) \/ (id Y) ::_thesis: ( id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )
proof
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in id (X \/ Y) or [x,b1] in (id X) \/ (id Y) ) & ( not [x,b1] in (id X) \/ (id Y) or [x,b1] in id (X \/ Y) ) )
let y be set ; ::_thesis: ( ( not [x,y] in id (X \/ Y) or [x,y] in (id X) \/ (id Y) ) & ( not [x,y] in (id X) \/ (id Y) or [x,y] in id (X \/ Y) ) )
thus ( [x,y] in id (X \/ Y) implies [x,y] in (id X) \/ (id Y) ) ::_thesis: ( not [x,y] in (id X) \/ (id Y) or [x,y] in id (X \/ Y) )
proof
assume A1: [x,y] in id (X \/ Y) ; ::_thesis: [x,y] in (id X) \/ (id Y)
then x in X \/ Y by RELAT_1:def_10;
then A2: ( x in X or x in Y ) by XBOOLE_0:def_3;
x = y by A1, RELAT_1:def_10;
then ( [x,y] in id X or [x,y] in id Y ) by A2, RELAT_1:def_10;
hence [x,y] in (id X) \/ (id Y) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume [x,y] in (id X) \/ (id Y) ; ::_thesis: [x,y] in id (X \/ Y)
then A3: ( [x,y] in id X or [x,y] in id Y ) by XBOOLE_0:def_3;
then ( x in X or x in Y ) by RELAT_1:def_10;
then A4: x in X \/ Y by XBOOLE_0:def_3;
x = y by A3, RELAT_1:def_10;
hence [x,y] in id (X \/ Y) by A4, RELAT_1:def_10; ::_thesis: verum
end;
thus id (X /\ Y) = (id X) /\ (id Y) ::_thesis: id (X \ Y) = (id X) \ (id Y)
proof
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in id (X /\ Y) or [x,b1] in (id X) /\ (id Y) ) & ( not [x,b1] in (id X) /\ (id Y) or [x,b1] in id (X /\ Y) ) )
let y be set ; ::_thesis: ( ( not [x,y] in id (X /\ Y) or [x,y] in (id X) /\ (id Y) ) & ( not [x,y] in (id X) /\ (id Y) or [x,y] in id (X /\ Y) ) )
thus ( [x,y] in id (X /\ Y) implies [x,y] in (id X) /\ (id Y) ) ::_thesis: ( not [x,y] in (id X) /\ (id Y) or [x,y] in id (X /\ Y) )
proof
assume A5: [x,y] in id (X /\ Y) ; ::_thesis: [x,y] in (id X) /\ (id Y)
then A6: x in X /\ Y by RELAT_1:def_10;
A7: x = y by A5, RELAT_1:def_10;
x in Y by A6, XBOOLE_0:def_4;
then A8: [x,y] in id Y by A7, RELAT_1:def_10;
x in X by A6, XBOOLE_0:def_4;
then [x,y] in id X by A7, RELAT_1:def_10;
hence [x,y] in (id X) /\ (id Y) by A8, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A9: [x,y] in (id X) /\ (id Y) ; ::_thesis: [x,y] in id (X /\ Y)
then A10: [x,y] in id X by XBOOLE_0:def_4;
then A11: x = y by RELAT_1:def_10;
[x,y] in id Y by A9, XBOOLE_0:def_4;
then A12: x in Y by RELAT_1:def_10;
x in X by A10, RELAT_1:def_10;
then x in X /\ Y by A12, XBOOLE_0:def_4;
hence [x,y] in id (X /\ Y) by A11, RELAT_1:def_10; ::_thesis: verum
end;
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in id (X \ Y) or [x,b1] in (id X) \ (id Y) ) & ( not [x,b1] in (id X) \ (id Y) or [x,b1] in id (X \ Y) ) )
let y be set ; ::_thesis: ( ( not [x,y] in id (X \ Y) or [x,y] in (id X) \ (id Y) ) & ( not [x,y] in (id X) \ (id Y) or [x,y] in id (X \ Y) ) )
thus ( [x,y] in id (X \ Y) implies [x,y] in (id X) \ (id Y) ) ::_thesis: ( not [x,y] in (id X) \ (id Y) or [x,y] in id (X \ Y) )
proof
assume A13: [x,y] in id (X \ Y) ; ::_thesis: [x,y] in (id X) \ (id Y)
then A14: x in X \ Y by RELAT_1:def_10;
then not x in Y by XBOOLE_0:def_5;
then A15: not [x,y] in id Y by RELAT_1:def_10;
x = y by A13, RELAT_1:def_10;
then [x,y] in id X by A14, RELAT_1:def_10;
hence [x,y] in (id X) \ (id Y) by A15, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A16: [x,y] in (id X) \ (id Y) ; ::_thesis: [x,y] in id (X \ Y)
then A17: x = y by RELAT_1:def_10;
not [x,y] in id Y by A16, XBOOLE_0:def_5;
then A18: ( not x in Y or not x = y ) by RELAT_1:def_10;
x in X by A16, RELAT_1:def_10;
then x in X \ Y by A16, A18, RELAT_1:def_10, XBOOLE_0:def_5;
hence [x,y] in id (X \ Y) by A17, RELAT_1:def_10; ::_thesis: verum
end;
theorem Th15: :: SYSREL:15
for X, Y being set st X c= Y holds
id X c= id Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies id X c= id Y )
assume X c= Y ; ::_thesis: id X c= id Y
then X \/ Y = Y by XBOOLE_1:12;
then (id X) \/ (id Y) = id Y by Th14;
hence id X c= id Y by XBOOLE_1:7; ::_thesis: verum
end;
theorem :: SYSREL:16
for X, Y being set holds (id (X \ Y)) \ (id X) = {}
proof
let X, Y be set ; ::_thesis: (id (X \ Y)) \ (id X) = {}
id (X \ Y) c= id X by Th15;
hence (id (X \ Y)) \ (id X) = {} by XBOOLE_1:37; ::_thesis: verum
end;
theorem :: SYSREL:17
for R being Relation st R c= id (dom R) holds
R = id (dom R)
proof
let R be Relation; ::_thesis: ( R c= id (dom R) implies R = id (dom R) )
assume A1: R c= id (dom R) ; ::_thesis: R = id (dom R)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in R or [x,b1] in id (dom R) ) & ( not [x,b1] in id (dom R) or [x,b1] in R ) )
let y be set ; ::_thesis: ( ( not [x,y] in R or [x,y] in id (dom R) ) & ( not [x,y] in id (dom R) or [x,y] in R ) )
thus ( [x,y] in R implies [x,y] in id (dom R) ) by A1; ::_thesis: ( not [x,y] in id (dom R) or [x,y] in R )
assume A2: [x,y] in id (dom R) ; ::_thesis: [x,y] in R
then x in dom R by RELAT_1:def_10;
then A3: ex z being set st [x,z] in R by XTUPLE_0:def_12;
x = y by A2, RELAT_1:def_10;
hence [x,y] in R by A1, A3, RELAT_1:def_10; ::_thesis: verum
end;
theorem :: SYSREL:18
for X being set
for R being Relation st id X c= R \/ (R ~) holds
( id X c= R & id X c= R ~ )
proof
let X be set ; ::_thesis: for R being Relation st id X c= R \/ (R ~) holds
( id X c= R & id X c= R ~ )
let R be Relation; ::_thesis: ( id X c= R \/ (R ~) implies ( id X c= R & id X c= R ~ ) )
assume A1: id X c= R \/ (R ~) ; ::_thesis: ( id X c= R & id X c= R ~ )
for x being set st x in X holds
( [x,x] in R & [x,x] in R ~ )
proof
let x be set ; ::_thesis: ( x in X implies ( [x,x] in R & [x,x] in R ~ ) )
assume x in X ; ::_thesis: ( [x,x] in R & [x,x] in R ~ )
then [x,x] in id X by RELAT_1:def_10;
then A2: ( [x,x] in R or [x,x] in R ~ ) by A1, XBOOLE_0:def_3;
hence [x,x] in R by RELAT_1:def_7; ::_thesis: [x,x] in R ~
thus [x,x] in R ~ by A2, RELAT_1:def_7; ::_thesis: verum
end;
then ( ( for x being set st x in X holds
[x,x] in R ) & ( for x being set st x in X holds
[x,x] in R ~ ) ) ;
hence ( id X c= R & id X c= R ~ ) by RELAT_1:47; ::_thesis: verum
end;
theorem :: SYSREL:19
for X being set
for R being Relation st id X c= R holds
id X c= R ~
proof
let X be set ; ::_thesis: for R being Relation st id X c= R holds
id X c= R ~
let R be Relation; ::_thesis: ( id X c= R implies id X c= R ~ )
assume A1: id X c= R ; ::_thesis: id X c= R ~
for x being set st x in X holds
[x,x] in R ~
proof
let x be set ; ::_thesis: ( x in X implies [x,x] in R ~ )
assume x in X ; ::_thesis: [x,x] in R ~
then [x,x] in id X by RELAT_1:def_10;
hence [x,x] in R ~ by A1, RELAT_1:def_7; ::_thesis: verum
end;
hence id X c= R ~ by RELAT_1:47; ::_thesis: verum
end;
theorem :: SYSREL:20
for X being set
for R being Relation st R c= [:X,X:] holds
( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) )
proof
let X be set ; ::_thesis: for R being Relation st R c= [:X,X:] holds
( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) )
let R be Relation; ::_thesis: ( R c= [:X,X:] implies ( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) ) )
A1: R \ (id (dom R)) c= R \ (id X)
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in R \ (id (dom R)) or [x,b1] in R \ (id X) )
let y be set ; ::_thesis: ( not [x,y] in R \ (id (dom R)) or [x,y] in R \ (id X) )
assume A2: [x,y] in R \ (id (dom R)) ; ::_thesis: [x,y] in R \ (id X)
then A3: not [x,y] in id (dom R) by XBOOLE_0:def_5;
not [x,y] in id X
proof
assume [x,y] in id X ; ::_thesis: contradiction
then A4: x = y by RELAT_1:def_10;
x in dom R by A2, XTUPLE_0:def_12;
hence contradiction by A3, A4, RELAT_1:def_10; ::_thesis: verum
end;
hence [x,y] in R \ (id X) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
A5: R \ (id (rng R)) c= R \ (id X)
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in R \ (id (rng R)) or [x,b1] in R \ (id X) )
let y be set ; ::_thesis: ( not [x,y] in R \ (id (rng R)) or [x,y] in R \ (id X) )
assume A6: [x,y] in R \ (id (rng R)) ; ::_thesis: [x,y] in R \ (id X)
then A7: not [x,y] in id (rng R) by XBOOLE_0:def_5;
not [x,y] in id X
proof
assume [x,y] in id X ; ::_thesis: contradiction
then A8: x = y by RELAT_1:def_10;
y in rng R by A6, XTUPLE_0:def_13;
hence contradiction by A7, A8, RELAT_1:def_10; ::_thesis: verum
end;
hence [x,y] in R \ (id X) by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A9: R c= [:X,X:] ; ::_thesis: ( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) )
then id (dom R) c= id X by Th3, Th15;
then R \ (id X) c= R \ (id (dom R)) by XBOOLE_1:34;
hence R \ (id (dom R)) = R \ (id X) by A1, XBOOLE_0:def_10; ::_thesis: R \ (id (rng R)) = R \ (id X)
id (rng R) c= id X by A9, Th3, Th15;
then R \ (id X) c= R \ (id (rng R)) by XBOOLE_1:34;
hence R \ (id (rng R)) = R \ (id X) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: SYSREL:21
for X being set
for R being Relation holds
( ( (id X) * (R \ (id X)) = {} implies dom (R \ (id X)) = (dom R) \ X ) & ( (R \ (id X)) * (id X) = {} implies rng (R \ (id X)) = (rng R) \ X ) )
proof
let X be set ; ::_thesis: for R being Relation holds
( ( (id X) * (R \ (id X)) = {} implies dom (R \ (id X)) = (dom R) \ X ) & ( (R \ (id X)) * (id X) = {} implies rng (R \ (id X)) = (rng R) \ X ) )
let R be Relation; ::_thesis: ( ( (id X) * (R \ (id X)) = {} implies dom (R \ (id X)) = (dom R) \ X ) & ( (R \ (id X)) * (id X) = {} implies rng (R \ (id X)) = (rng R) \ X ) )
thus ( (id X) * (R \ (id X)) = {} implies dom (R \ (id X)) = (dom R) \ X ) ::_thesis: ( (R \ (id X)) * (id X) = {} implies rng (R \ (id X)) = (rng R) \ X )
proof
assume A1: (id X) * (R \ (id X)) = {} ; ::_thesis: dom (R \ (id X)) = (dom R) \ X
A2: dom (R \ (id X)) c= (dom R) \ X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (R \ (id X)) or x in (dom R) \ X )
A3: ( x in dom R & not x in X & x in dom (R \ (id X)) implies x in (dom R) \ X ) by XBOOLE_0:def_5;
assume x in dom (R \ (id X)) ; ::_thesis: x in (dom R) \ X
then A6: ex y being set st [x,y] in R \ (id X) by XTUPLE_0:def_12;
not x in X
proof
assume x in X ; ::_thesis: contradiction
then [x,x] in id X by RELAT_1:def_10;
hence contradiction by A1, A6, RELAT_1:def_8; ::_thesis: verum
end;
hence x in (dom R) \ X by A6, A3, XTUPLE_0:def_12; ::_thesis: verum
end;
(dom R) \ (dom (id X)) c= dom (R \ (id X)) by RELAT_1:3;
then (dom R) \ X c= dom (R \ (id X)) ;
hence dom (R \ (id X)) = (dom R) \ X by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus ( (R \ (id X)) * (id X) = {} implies rng (R \ (id X)) = (rng R) \ X ) ::_thesis: verum
proof
assume A7: (R \ (id X)) * (id X) = {} ; ::_thesis: rng (R \ (id X)) = (rng R) \ X
A8: rng (R \ (id X)) c= (rng R) \ X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (R \ (id X)) or y in (rng R) \ X )
A9: ( y in rng R & not y in X & y in rng (R \ (id X)) implies y in (rng R) \ X ) by XBOOLE_0:def_5;
assume y in rng (R \ (id X)) ; ::_thesis: y in (rng R) \ X
then A12: ex x being set st [x,y] in R \ (id X) by XTUPLE_0:def_13;
not y in X
proof
assume y in X ; ::_thesis: contradiction
then [y,y] in id X by RELAT_1:def_10;
hence contradiction by A7, A12, RELAT_1:def_8; ::_thesis: verum
end;
hence y in (rng R) \ X by A12, A9, XTUPLE_0:def_13; ::_thesis: verum
end;
(rng R) \ (rng (id X)) c= rng (R \ (id X)) by RELAT_1:14;
then (rng R) \ X c= rng (R \ (id X)) ;
hence rng (R \ (id X)) = (rng R) \ X by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
theorem Th22: :: SYSREL:22
for R being Relation holds
( ( R c= R * R & R * (R \ (id (rng R))) = {} implies id (rng R) c= R ) & ( R c= R * R & (R \ (id (dom R))) * R = {} implies id (dom R) c= R ) )
proof
let R be Relation; ::_thesis: ( ( R c= R * R & R * (R \ (id (rng R))) = {} implies id (rng R) c= R ) & ( R c= R * R & (R \ (id (dom R))) * R = {} implies id (dom R) c= R ) )
thus ( R c= R * R & R * (R \ (id (rng R))) = {} implies id (rng R) c= R ) ::_thesis: ( R c= R * R & (R \ (id (dom R))) * R = {} implies id (dom R) c= R )
proof
assume that
A1: R c= R * R and
A2: R * (R \ (id (rng R))) = {} ; ::_thesis: id (rng R) c= R
for y being set st y in rng R holds
[y,y] in R
proof
let y be set ; ::_thesis: ( y in rng R implies [y,y] in R )
assume y in rng R ; ::_thesis: [y,y] in R
then consider x being set such that
A3: [x,y] in R by XTUPLE_0:def_13;
consider z being set such that
A4: [x,z] in R and
A5: [z,y] in R by A1, A3, RELAT_1:def_8;
z = y
proof
assume z <> y ; ::_thesis: contradiction
then not [z,y] in id (rng R) by RELAT_1:def_10;
then [z,y] in R \ (id (rng R)) by A5, XBOOLE_0:def_5;
hence contradiction by A2, A4, RELAT_1:def_8; ::_thesis: verum
end;
hence [y,y] in R by A5; ::_thesis: verum
end;
hence id (rng R) c= R by RELAT_1:47; ::_thesis: verum
end;
assume that
A6: R c= R * R and
A7: (R \ (id (dom R))) * R = {} ; ::_thesis: id (dom R) c= R
for x being set st x in dom R holds
[x,x] in R
proof
let x be set ; ::_thesis: ( x in dom R implies [x,x] in R )
assume x in dom R ; ::_thesis: [x,x] in R
then consider y being set such that
A8: [x,y] in R by XTUPLE_0:def_12;
consider z being set such that
A9: [x,z] in R and
A10: [z,y] in R by A6, A8, RELAT_1:def_8;
z = x
proof
assume z <> x ; ::_thesis: contradiction
then not [x,z] in id (dom R) by RELAT_1:def_10;
then [x,z] in R \ (id (dom R)) by A9, XBOOLE_0:def_5;
hence contradiction by A7, A10, RELAT_1:def_8; ::_thesis: verum
end;
hence [x,x] in R by A9; ::_thesis: verum
end;
hence id (dom R) c= R by RELAT_1:47; ::_thesis: verum
end;
theorem :: SYSREL:23
for R being Relation holds
( ( R c= R * R & R * (R \ (id (rng R))) = {} implies R /\ (id (rng R)) = id (rng R) ) & ( R c= R * R & (R \ (id (dom R))) * R = {} implies R /\ (id (dom R)) = id (dom R) ) ) by Th22, XBOOLE_1:28;
theorem :: SYSREL:24
for X being set
for R being Relation holds
( ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} ) )
proof
let X be set ; ::_thesis: for R being Relation holds
( ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} ) )
let R be Relation; ::_thesis: ( ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} ) )
thus ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) ::_thesis: ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} )
proof
assume that
A1: R * (R \ (id X)) = {} and
A2: R * (R \ (id (rng R))) <> {} ; ::_thesis: contradiction
consider x, y being set such that
A3: [x,y] in R * (R \ (id (rng R))) by A2, RELAT_1:37;
consider z being set such that
A4: [x,z] in R and
A5: [z,y] in R \ (id (rng R)) by A3, RELAT_1:def_8;
( z in rng R & not [z,y] in id (rng R) ) by A4, A5, XBOOLE_0:def_5, XTUPLE_0:def_13;
then z <> y by RELAT_1:def_10;
then not [z,y] in id X by RELAT_1:def_10;
then [z,y] in R \ (id X) by A5, XBOOLE_0:def_5;
hence contradiction by A1, A4, RELAT_1:def_8; ::_thesis: verum
end;
assume that
A6: (R \ (id X)) * R = {} and
A7: (R \ (id (dom R))) * R <> {} ; ::_thesis: contradiction
consider x, y being set such that
A8: [x,y] in (R \ (id (dom R))) * R by A7, RELAT_1:37;
consider z being set such that
A9: [x,z] in R \ (id (dom R)) and
A10: [z,y] in R by A8, RELAT_1:def_8;
not [x,z] in id (dom R) by A9, XBOOLE_0:def_5;
then ( not z in dom R or x <> z ) by RELAT_1:def_10;
then not [x,z] in id X by A10, RELAT_1:def_10, XTUPLE_0:def_12;
then [x,z] in R \ (id X) by A9, XBOOLE_0:def_5;
hence contradiction by A6, A10, RELAT_1:def_8; ::_thesis: verum
end;
definition
let R be Relation;
func CL R -> Relation equals :: SYSREL:def 1
R /\ (id (dom R));
correctness
coherence
R /\ (id (dom R)) is Relation;
;
end;
:: deftheorem defines CL SYSREL:def_1_:_
for R being Relation holds CL R = R /\ (id (dom R));
theorem Th25: :: SYSREL:25
for x, y being set
for R being Relation st [x,y] in CL R holds
( x in dom (CL R) & x = y )
proof
let x, y be set ; ::_thesis: for R being Relation st [x,y] in CL R holds
( x in dom (CL R) & x = y )
let R be Relation; ::_thesis: ( [x,y] in CL R implies ( x in dom (CL R) & x = y ) )
assume A1: [x,y] in CL R ; ::_thesis: ( x in dom (CL R) & x = y )
then [x,y] in id (dom R) by XBOOLE_0:def_4;
hence ( x in dom (CL R) & x = y ) by A1, RELAT_1:def_10, XTUPLE_0:def_12; ::_thesis: verum
end;
theorem Th26: :: SYSREL:26
for R being Relation holds dom (CL R) = rng (CL R)
proof
let R be Relation; ::_thesis: dom (CL R) = rng (CL R)
thus dom (CL R) c= rng (CL R) :: according to XBOOLE_0:def_10 ::_thesis: rng (CL R) c= dom (CL R)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (CL R) or x in rng (CL R) )
assume x in dom (CL R) ; ::_thesis: x in rng (CL R)
then consider y being set such that
A1: [x,y] in CL R by XTUPLE_0:def_12;
[x,y] in id (dom R) by A1, XBOOLE_0:def_4;
then [x,x] in CL R by A1, RELAT_1:def_10;
hence x in rng (CL R) by XTUPLE_0:def_13; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (CL R) or x in dom (CL R) )
assume x in rng (CL R) ; ::_thesis: x in dom (CL R)
then consider y being set such that
A2: [y,x] in CL R by XTUPLE_0:def_13;
[y,x] in id (dom R) by A2, XBOOLE_0:def_4;
then [x,x] in CL R by A2, RELAT_1:def_10;
hence x in dom (CL R) by XTUPLE_0:def_12; ::_thesis: verum
end;
theorem Th27: :: SYSREL:27
for x being set
for R being Relation holds
( ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in dom (CL R) ) & ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
proof
let x be set ; ::_thesis: for R being Relation holds
( ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in dom (CL R) ) & ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
let R be Relation; ::_thesis: ( ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in dom (CL R) ) & ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
A1: ( x in dom R & [x,x] in R implies x in dom (CL R) )
proof
assume that
A2: x in dom R and
A3: [x,x] in R ; ::_thesis: x in dom (CL R)
[x,x] in id (dom R) by A2, RELAT_1:def_10;
then [x,x] in R /\ (id (dom R)) by A3, XBOOLE_0:def_4;
hence x in dom (CL R) by XTUPLE_0:def_12; ::_thesis: verum
end;
A4: ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) )
proof
assume x in dom (CL R) ; ::_thesis: ( x in dom R & [x,x] in R )
then consider y being set such that
A5: [x,y] in CL R by XTUPLE_0:def_12;
( [x,y] in R & [x,y] in id (dom R) ) by A5, XBOOLE_0:def_4;
hence ( x in dom R & [x,x] in R ) by RELAT_1:def_10; ::_thesis: verum
end;
hence ( x in dom (CL R) iff ( x in dom R & [x,x] in R ) ) by A1; ::_thesis: ( ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
thus ( x in rng (CL R) iff ( x in dom R & [x,x] in R ) ) by A4, A1, Th26; ::_thesis: ( ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
thus ( x in rng (CL R) iff ( x in rng R & [x,x] in R ) ) by A4, A1, Th26, XTUPLE_0:def_12, XTUPLE_0:def_13; ::_thesis: ( x in dom (CL R) iff ( x in rng R & [x,x] in R ) )
thus ( x in dom (CL R) iff ( x in rng R & [x,x] in R ) ) by A4, A1, XTUPLE_0:def_12, XTUPLE_0:def_13; ::_thesis: verum
end;
theorem Th28: :: SYSREL:28
for R being Relation holds CL R = id (dom (CL R))
proof
let R be Relation; ::_thesis: CL R = id (dom (CL R))
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in CL R or [x,b1] in id (dom (CL R)) ) & ( not [x,b1] in id (dom (CL R)) or [x,b1] in CL R ) )
let y be set ; ::_thesis: ( ( not [x,y] in CL R or [x,y] in id (dom (CL R)) ) & ( not [x,y] in id (dom (CL R)) or [x,y] in CL R ) )
thus ( [x,y] in CL R implies [x,y] in id (dom (CL R)) ) ::_thesis: ( not [x,y] in id (dom (CL R)) or [x,y] in CL R )
proof
assume A1: [x,y] in CL R ; ::_thesis: [x,y] in id (dom (CL R))
then [x,y] in id (dom R) by XBOOLE_0:def_4;
then A2: x = y by RELAT_1:def_10;
x in dom (CL R) by A1, XTUPLE_0:def_12;
hence [x,y] in id (dom (CL R)) by A2, RELAT_1:def_10; ::_thesis: verum
end;
assume A3: [x,y] in id (dom (CL R)) ; ::_thesis: [x,y] in CL R
then x in dom (CL R) by RELAT_1:def_10;
then A4: ex z being set st [x,z] in CL R by XTUPLE_0:def_12;
x = y by A3, RELAT_1:def_10;
hence [x,y] in CL R by A4, Th25; ::_thesis: verum
end;
theorem Th29: :: SYSREL:29
for x, y being set
for R being Relation holds
( ( R * R = R & R * (R \ (CL R)) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
proof
let x, y be set ; ::_thesis: for R being Relation holds
( ( R * R = R & R * (R \ (CL R)) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
let R be Relation; ::_thesis: ( ( R * R = R & R * (R \ (CL R)) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
thus ( R * R = R & R * (R \ (CL R)) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) ::_thesis: ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) )
proof
assume that
A1: R * R = R and
A2: R * (R \ (CL R)) = {} and
A3: [x,y] in R and
A4: x <> y ; ::_thesis: ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) )
A5: y in rng R by A3, XTUPLE_0:def_13;
consider z being set such that
A6: [x,z] in R and
A7: [z,y] in R by A1, A3, RELAT_1:def_8;
A8: z = y
proof
assume z <> y ; ::_thesis: contradiction
then not [z,y] in id (dom R) by RELAT_1:def_10;
then not [z,y] in R /\ (id (dom R)) by XBOOLE_0:def_4;
then [z,y] in R \ (CL R) by A7, XBOOLE_0:def_5;
hence contradiction by A2, A6, RELAT_1:def_8; ::_thesis: verum
end;
not [x,y] in id (dom R) by A4, RELAT_1:def_10;
then not [x,y] in R /\ (id (dom R)) by XBOOLE_0:def_4;
then A9: [x,y] in R \ (CL R) by A3, XBOOLE_0:def_5;
A10: not x in dom (CL R)
proof
assume x in dom (CL R) ; ::_thesis: contradiction
then [x,x] in R by Th27;
hence contradiction by A2, A9, RELAT_1:def_8; ::_thesis: verum
end;
x in dom R by A6, XTUPLE_0:def_12;
hence ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) by A7, A8, A5, A10, Th27, XBOOLE_0:def_5; ::_thesis: verum
end;
thus ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) ::_thesis: verum
proof
assume that
A11: R * R = R and
A12: (R \ (CL R)) * R = {} and
A13: [x,y] in R and
A14: x <> y ; ::_thesis: ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) )
A15: x in dom R by A13, XTUPLE_0:def_12;
consider z being set such that
A16: [x,z] in R and
A17: [z,y] in R by A11, A13, RELAT_1:def_8;
A18: z = x
proof
assume z <> x ; ::_thesis: contradiction
then not [x,z] in id (dom R) by RELAT_1:def_10;
then not [x,z] in R /\ (id (dom R)) by XBOOLE_0:def_4;
then [x,z] in R \ (CL R) by A16, XBOOLE_0:def_5;
hence contradiction by A12, A17, RELAT_1:def_8; ::_thesis: verum
end;
not [x,y] in id (dom R) by A14, RELAT_1:def_10;
then not [x,y] in R /\ (id (dom R)) by XBOOLE_0:def_4;
then A19: [x,y] in R \ (CL R) by A13, XBOOLE_0:def_5;
A20: not y in dom (CL R)
proof
assume y in dom (CL R) ; ::_thesis: contradiction
then [y,y] in R by Th27;
hence contradiction by A12, A19, RELAT_1:def_8; ::_thesis: verum
end;
y in rng R by A17, XTUPLE_0:def_13;
hence ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) by A16, A18, A15, A20, Th27, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
theorem :: SYSREL:30
for x, y being set
for R being Relation holds
( ( R * R = R & R * (R \ (id (dom R))) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
proof
let x, y be set ; ::_thesis: for R being Relation holds
( ( R * R = R & R * (R \ (id (dom R))) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
let R be Relation; ::_thesis: ( ( R * R = R & R * (R \ (id (dom R))) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
R \ (CL R) = R \ (id (dom R)) by XBOOLE_1:47;
hence ( ( R * R = R & R * (R \ (id (dom R))) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) ) by Th29; ::_thesis: verum
end;
theorem :: SYSREL:31
for R being Relation holds
( ( R * R = R & R * (R \ (id (dom R))) = {} implies ( dom (CL R) = rng R & rng (CL R) = rng R ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} implies ( dom (CL R) = dom R & rng (CL R) = dom R ) ) )
proof
let R be Relation; ::_thesis: ( ( R * R = R & R * (R \ (id (dom R))) = {} implies ( dom (CL R) = rng R & rng (CL R) = rng R ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} implies ( dom (CL R) = dom R & rng (CL R) = dom R ) ) )
thus ( R * R = R & R * (R \ (id (dom R))) = {} implies ( dom (CL R) = rng R & rng (CL R) = rng R ) ) ::_thesis: ( R * R = R & (R \ (id (dom R))) * R = {} implies ( dom (CL R) = dom R & rng (CL R) = dom R ) )
proof
assume that
A1: R * R = R and
A2: R * (R \ (id (dom R))) = {} ; ::_thesis: ( dom (CL R) = rng R & rng (CL R) = rng R )
for y being set st y in rng R holds
y in dom (CL R)
proof
let y be set ; ::_thesis: ( y in rng R implies y in dom (CL R) )
assume y in rng R ; ::_thesis: y in dom (CL R)
then consider x being set such that
A3: [x,y] in R by XTUPLE_0:def_13;
consider z being set such that
A4: [x,z] in R and
A5: [z,y] in R by A1, A3, RELAT_1:def_8;
A6: z = y
proof
assume z <> y ; ::_thesis: contradiction
then not [z,y] in id (dom R) by RELAT_1:def_10;
then [z,y] in R \ (id (dom R)) by A5, XBOOLE_0:def_5;
hence contradiction by A2, A4, RELAT_1:def_8; ::_thesis: verum
end;
z in dom R by A5, XTUPLE_0:def_12;
then [z,y] in id (dom R) by A6, RELAT_1:def_10;
then [z,y] in R /\ (id (dom R)) by A5, XBOOLE_0:def_4;
hence y in dom (CL R) by A6, XTUPLE_0:def_12; ::_thesis: verum
end;
then A7: rng R c= dom (CL R) by TARSKI:def_3;
CL R c= R by XBOOLE_1:17;
then rng (CL R) c= rng R by RELAT_1:11;
then dom (CL R) c= rng R by Th26;
then dom (CL R) = rng R by A7, XBOOLE_0:def_10;
hence ( dom (CL R) = rng R & rng (CL R) = rng R ) by Th26; ::_thesis: verum
end;
thus ( R * R = R & (R \ (id (dom R))) * R = {} implies ( dom (CL R) = dom R & rng (CL R) = dom R ) ) ::_thesis: verum
proof
assume that
A8: R * R = R and
A9: (R \ (id (dom R))) * R = {} ; ::_thesis: ( dom (CL R) = dom R & rng (CL R) = dom R )
for x being set st x in dom R holds
x in dom (CL R)
proof
let x be set ; ::_thesis: ( x in dom R implies x in dom (CL R) )
assume A10: x in dom R ; ::_thesis: x in dom (CL R)
then consider y being set such that
A11: [x,y] in R by XTUPLE_0:def_12;
consider z being set such that
A12: [x,z] in R and
A13: [z,y] in R by A8, A11, RELAT_1:def_8;
A14: z = x
proof
assume z <> x ; ::_thesis: contradiction
then not [x,z] in id (dom R) by RELAT_1:def_10;
then [x,z] in R \ (id (dom R)) by A12, XBOOLE_0:def_5;
hence contradiction by A9, A13, RELAT_1:def_8; ::_thesis: verum
end;
then [x,z] in id (dom R) by A10, RELAT_1:def_10;
then [x,z] in R /\ (id (dom R)) by A12, XBOOLE_0:def_4;
then z in rng (CL R) by XTUPLE_0:def_13;
hence x in dom (CL R) by A14, Th26; ::_thesis: verum
end;
then A15: dom R c= dom (CL R) by TARSKI:def_3;
CL R c= R by XBOOLE_1:17;
then dom (CL R) c= dom R by RELAT_1:11;
then dom (CL R) = dom R by A15, XBOOLE_0:def_10;
hence ( dom (CL R) = dom R & rng (CL R) = dom R ) by Th26; ::_thesis: verum
end;
end;
theorem Th32: :: SYSREL:32
for R being Relation holds
( dom (CL R) c= dom R & rng (CL R) c= rng R & rng (CL R) c= dom R & dom (CL R) c= rng R )
proof
let R be Relation; ::_thesis: ( dom (CL R) c= dom R & rng (CL R) c= rng R & rng (CL R) c= dom R & dom (CL R) c= rng R )
CL R c= R by XBOOLE_1:17;
hence ( dom (CL R) c= dom R & rng (CL R) c= rng R ) by RELAT_1:11; ::_thesis: ( rng (CL R) c= dom R & dom (CL R) c= rng R )
hence ( rng (CL R) c= dom R & dom (CL R) c= rng R ) by Th26; ::_thesis: verum
end;
theorem :: SYSREL:33
for R being Relation holds
( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) )
proof
let R be Relation; ::_thesis: ( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) )
dom (CL R) c= dom R by Th32;
then id (dom (CL R)) c= id (dom R) by Th15;
hence ( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) ) by Th26; ::_thesis: verum
end;
theorem Th34: :: SYSREL:34
for R being Relation holds
( id (dom (CL R)) c= R & id (rng (CL R)) c= R )
proof
let R be Relation; ::_thesis: ( id (dom (CL R)) c= R & id (rng (CL R)) c= R )
thus id (dom (CL R)) c= R ::_thesis: id (rng (CL R)) c= R
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in id (dom (CL R)) or [x,b1] in R )
let y be set ; ::_thesis: ( not [x,y] in id (dom (CL R)) or [x,y] in R )
assume [x,y] in id (dom (CL R)) ; ::_thesis: [x,y] in R
then ( x in dom (CL R) & x = y ) by RELAT_1:def_10;
hence [x,y] in R by Th27; ::_thesis: verum
end;
hence id (rng (CL R)) c= R by Th26; ::_thesis: verum
end;
theorem Th35: :: SYSREL:35
for X being set
for R being Relation holds
( ( id X c= R & (id X) * (R \ (id X)) = {} implies R | X = id X ) & ( id X c= R & (R \ (id X)) * (id X) = {} implies X |` R = id X ) )
proof
let X be set ; ::_thesis: for R being Relation holds
( ( id X c= R & (id X) * (R \ (id X)) = {} implies R | X = id X ) & ( id X c= R & (R \ (id X)) * (id X) = {} implies X |` R = id X ) )
let R be Relation; ::_thesis: ( ( id X c= R & (id X) * (R \ (id X)) = {} implies R | X = id X ) & ( id X c= R & (R \ (id X)) * (id X) = {} implies X |` R = id X ) )
thus ( id X c= R & (id X) * (R \ (id X)) = {} implies R | X = id X ) ::_thesis: ( id X c= R & (R \ (id X)) * (id X) = {} implies X |` R = id X )
proof
assume that
A1: id X c= R and
A2: (id X) * (R \ (id X)) = {} ; ::_thesis: R | X = id X
R | X = (id X) * R by RELAT_1:65
.= (id X) * (R \/ (id X)) by A1, XBOOLE_1:12
.= (id X) * ((R \ (id X)) \/ (id X)) by XBOOLE_1:39
.= {} \/ ((id X) * (id X)) by A2, RELAT_1:32
.= id X by Th12 ;
hence R | X = id X ; ::_thesis: verum
end;
assume that
A3: id X c= R and
A4: (R \ (id X)) * (id X) = {} ; ::_thesis: X |` R = id X
X |` R = R * (id X) by RELAT_1:92
.= (R \/ (id X)) * (id X) by A3, XBOOLE_1:12
.= ((R \ (id X)) \/ (id X)) * (id X) by XBOOLE_1:39
.= {} \/ ((id X) * (id X)) by A4, Th6
.= id X by Th12 ;
hence X |` R = id X ; ::_thesis: verum
end;
theorem :: SYSREL:36
for R being Relation holds
( ( (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} implies ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) ) & ( (R \ (id (rng (CL R)))) * (id (rng (CL R))) = {} implies ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) ) ) )
proof
let R be Relation; ::_thesis: ( ( (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} implies ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) ) & ( (R \ (id (rng (CL R)))) * (id (rng (CL R))) = {} implies ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) ) ) )
thus ( (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} implies ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) ) ::_thesis: ( (R \ (id (rng (CL R)))) * (id (rng (CL R))) = {} implies ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) ) )
proof
assume A1: (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} ; ::_thesis: ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) )
id (dom (CL R)) c= R by Th34;
then R | (dom (CL R)) = id (dom (CL R)) by A1, Th35;
hence ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) by Th26; ::_thesis: verum
end;
assume A2: (R \ (id (rng (CL R)))) * (id (rng (CL R))) = {} ; ::_thesis: ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) )
id (rng (CL R)) c= R by Th34;
then (rng (CL R)) |` R = id (rng (CL R)) by A2, Th35;
then (dom (CL R)) |` R = id (rng (CL R)) by Th26;
hence ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) ) by Th26; ::_thesis: verum
end;
theorem :: SYSREL:37
for R being Relation holds
( ( R * (R \ (id (dom R))) = {} implies (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} ) & ( (R \ (id (dom R))) * R = {} implies (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} ) )
proof
let R be Relation; ::_thesis: ( ( R * (R \ (id (dom R))) = {} implies (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} ) & ( (R \ (id (dom R))) * R = {} implies (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} ) )
thus ( R * (R \ (id (dom R))) = {} implies (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} ) ::_thesis: ( (R \ (id (dom R))) * R = {} implies (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} )
proof
A1: id (dom (CL R)) c= R by Th34;
assume A2: R * (R \ (id (dom R))) = {} ; ::_thesis: (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {}
R \ (id (dom R)) = R \ (CL R) by XBOOLE_1:47
.= R \ (id (dom (CL R))) by Th28 ;
hence (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} by A2, A1, RELAT_1:30, XBOOLE_1:3; ::_thesis: verum
end;
A3: id (dom (CL R)) c= R by Th34;
assume A4: (R \ (id (dom R))) * R = {} ; ::_thesis: (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {}
R \ (id (dom R)) = R \ (CL R) by XBOOLE_1:47
.= R \ (id (dom (CL R))) by Th28 ;
hence (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} by A4, A3, RELAT_1:29, XBOOLE_1:3; ::_thesis: verum
end;
theorem Th38: :: SYSREL:38
for S, R being Relation holds
( ( S * R = S & R * (R \ (id (dom R))) = {} implies S * (R \ (id (dom R))) = {} ) & ( R * S = S & (R \ (id (dom R))) * R = {} implies (R \ (id (dom R))) * S = {} ) )
proof
let S, R be Relation; ::_thesis: ( ( S * R = S & R * (R \ (id (dom R))) = {} implies S * (R \ (id (dom R))) = {} ) & ( R * S = S & (R \ (id (dom R))) * R = {} implies (R \ (id (dom R))) * S = {} ) )
thus ( S * R = S & R * (R \ (id (dom R))) = {} implies S * (R \ (id (dom R))) = {} ) ::_thesis: ( R * S = S & (R \ (id (dom R))) * R = {} implies (R \ (id (dom R))) * S = {} )
proof
assume ( S * R = S & R * (R \ (id (dom R))) = {} ) ; ::_thesis: S * (R \ (id (dom R))) = {}
then S * (R \ (id (dom R))) = S * {} by RELAT_1:36
.= {} ;
hence S * (R \ (id (dom R))) = {} ; ::_thesis: verum
end;
assume ( R * S = S & (R \ (id (dom R))) * R = {} ) ; ::_thesis: (R \ (id (dom R))) * S = {}
then (R \ (id (dom R))) * S = {} * S by RELAT_1:36
.= {} ;
hence (R \ (id (dom R))) * S = {} ; ::_thesis: verum
end;
theorem Th39: :: SYSREL:39
for S, R being Relation holds
( ( S * R = S & R * (R \ (id (dom R))) = {} implies CL S c= CL R ) & ( R * S = S & (R \ (id (dom R))) * R = {} implies CL S c= CL R ) )
proof
let S, R be Relation; ::_thesis: ( ( S * R = S & R * (R \ (id (dom R))) = {} implies CL S c= CL R ) & ( R * S = S & (R \ (id (dom R))) * R = {} implies CL S c= CL R ) )
thus ( S * R = S & R * (R \ (id (dom R))) = {} implies CL S c= CL R ) ::_thesis: ( R * S = S & (R \ (id (dom R))) * R = {} implies CL S c= CL R )
proof
assume that
A1: S * R = S and
A2: R * (R \ (id (dom R))) = {} ; ::_thesis: CL S c= CL R
A3: S * (R \ (id (dom R))) = {} by A1, A2, Th38;
for x, y being set st [x,y] in CL S holds
[x,y] in CL R
proof
let x, y be set ; ::_thesis: ( [x,y] in CL S implies [x,y] in CL R )
assume A4: [x,y] in CL S ; ::_thesis: [x,y] in CL R
then A5: [x,y] in id (dom S) by XBOOLE_0:def_4;
[x,y] in S by A4, XBOOLE_0:def_4;
then consider z being set such that
A6: [x,z] in S and
A7: [z,y] in R by A1, RELAT_1:def_8;
A8: z = y
proof
assume z <> y ; ::_thesis: contradiction
then not [z,y] in id (dom R) by RELAT_1:def_10;
then [z,y] in R \ (id (dom R)) by A7, XBOOLE_0:def_5;
hence contradiction by A3, A6, RELAT_1:def_8; ::_thesis: verum
end;
A9: x = y by A5, RELAT_1:def_10;
then x in dom R by A7, A8, XTUPLE_0:def_12;
then A10: [x,y] in id (dom R) by A9, RELAT_1:def_10;
[x,y] in R by A5, A7, A8, RELAT_1:def_10;
hence [x,y] in CL R by A10, XBOOLE_0:def_4; ::_thesis: verum
end;
hence CL S c= CL R by RELAT_1:def_3; ::_thesis: verum
end;
assume that
A11: R * S = S and
A12: (R \ (id (dom R))) * R = {} ; ::_thesis: CL S c= CL R
A13: (R \ (id (dom R))) * S = {} by A11, A12, Th38;
for x, y being set st [x,y] in CL S holds
[x,y] in CL R
proof
let x, y be set ; ::_thesis: ( [x,y] in CL S implies [x,y] in CL R )
assume A14: [x,y] in CL S ; ::_thesis: [x,y] in CL R
then A15: [x,y] in id (dom S) by XBOOLE_0:def_4;
then A16: x = y by RELAT_1:def_10;
[x,y] in S by A14, XBOOLE_0:def_4;
then consider z being set such that
A17: [x,z] in R and
A18: [z,y] in S by A11, RELAT_1:def_8;
x in dom R by A17, XTUPLE_0:def_12;
then A19: [x,y] in id (dom R) by A16, RELAT_1:def_10;
z = x
proof
assume z <> x ; ::_thesis: contradiction
then not [x,z] in id (dom R) by RELAT_1:def_10;
then [x,z] in R \ (id (dom R)) by A17, XBOOLE_0:def_5;
hence contradiction by A13, A18, RELAT_1:def_8; ::_thesis: verum
end;
then [x,y] in R by A15, A17, RELAT_1:def_10;
hence [x,y] in CL R by A19, XBOOLE_0:def_4; ::_thesis: verum
end;
hence CL S c= CL R by RELAT_1:def_3; ::_thesis: verum
end;
theorem :: SYSREL:40
for S, R being Relation holds
( ( S * R = S & R * (R \ (id (dom R))) = {} & R * S = R & S * (S \ (id (dom S))) = {} implies CL S = CL R ) & ( R * S = S & (R \ (id (dom R))) * R = {} & S * R = R & (S \ (id (dom S))) * S = {} implies CL S = CL R ) )
proof
let S, R be Relation; ::_thesis: ( ( S * R = S & R * (R \ (id (dom R))) = {} & R * S = R & S * (S \ (id (dom S))) = {} implies CL S = CL R ) & ( R * S = S & (R \ (id (dom R))) * R = {} & S * R = R & (S \ (id (dom S))) * S = {} implies CL S = CL R ) )
thus ( S * R = S & R * (R \ (id (dom R))) = {} & R * S = R & S * (S \ (id (dom S))) = {} implies CL S = CL R ) ::_thesis: ( R * S = S & (R \ (id (dom R))) * R = {} & S * R = R & (S \ (id (dom S))) * S = {} implies CL S = CL R )
proof
assume ( S * R = S & R * (R \ (id (dom R))) = {} & R * S = R & S * (S \ (id (dom S))) = {} ) ; ::_thesis: CL S = CL R
then ( CL S c= CL R & CL R c= CL S ) by Th39;
hence CL S = CL R by XBOOLE_0:def_10; ::_thesis: verum
end;
assume ( R * S = S & (R \ (id (dom R))) * R = {} & S * R = R & (S \ (id (dom S))) * S = {} ) ; ::_thesis: CL S = CL R
then ( CL S c= CL R & CL R c= CL S ) by Th39;
hence CL S = CL R by XBOOLE_0:def_10; ::_thesis: verum
end;