:: RELSET_2 semantic presentation
begin
notation
let X be set ;
synonym {_{X}_} for SmallestPartition X;
end;
theorem Th1: :: RELSET_2:1
for y, X being set holds
( y in {_{X}_} iff ex x being set st
( y = {x} & x in X ) )
proof
let y, X be set ; ::_thesis: ( y in {_{X}_} iff ex x being set st
( y = {x} & x in X ) )
thus ( y in {_{X}_} implies ex x being set st
( y = {x} & x in X ) ) ::_thesis: ( ex x being set st
( y = {x} & x in X ) implies y in {_{X}_} )
proof
assume A1: y in {_{X}_} ; ::_thesis: ex x being set st
( y = {x} & x in X )
percases ( X is empty or not X is empty ) ;
supposeA2: X is empty ; ::_thesis: ex x being set st
( y = {x} & x in X )
ex x being set st
( x in X & y = Class ((id X),x) ) by A1, EQREL_1:def_3;
hence ex x being set st
( y = {x} & x in X ) by A2; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: ex x being set st
( y = {x} & x in X )
then reconsider X9 = X as non empty set ;
y in { {x} where x is Element of X9 : verum } by A1, EQREL_1:37;
then ex x being Element of X9 st y = {x} ;
hence ex x being set st
( y = {x} & x in X ) ; ::_thesis: verum
end;
end;
end;
given x being set such that A3: y = {x} and
A4: x in X ; ::_thesis: y in {_{X}_}
reconsider X9 = X as non empty set by A4;
y in { {z} where z is Element of X9 : verum } by A3, A4;
hence y in {_{X}_} by EQREL_1:37; ::_thesis: verum
end;
theorem Th2: :: RELSET_2:2
for X being set holds
( X = {} iff {_{X}_} = {} )
proof
let X be set ; ::_thesis: ( X = {} iff {_{X}_} = {} )
thus ( X = {} implies {_{X}_} = {} ) ::_thesis: ( {_{X}_} = {} implies X = {} )
proof
assume A1: X = {} ; ::_thesis: {_{X}_} = {}
assume not {_{X}_} = {} ; ::_thesis: contradiction
then consider y being set such that
A2: y in {_{X}_} by XBOOLE_0:def_1;
ex x being set st
( y = {x} & x in X ) by A2, Th1;
hence contradiction by A1; ::_thesis: verum
end;
assume A3: {_{X}_} = {} ; ::_thesis: X = {}
assume not X = {} ; ::_thesis: contradiction
then consider x being set such that
A4: x in X by XBOOLE_0:def_1;
{x} in {_{X}_} by A4, Th1;
hence contradiction by A3; ::_thesis: verum
end;
theorem Th3: :: RELSET_2:3
for X, Y being set holds {_{(X \/ Y)}_} = {_{X}_} \/ {_{Y}_}
proof
let X, Y be set ; ::_thesis: {_{(X \/ Y)}_} = {_{X}_} \/ {_{Y}_}
thus {_{(X \/ Y)}_} c= {_{X}_} \/ {_{Y}_} :: according to XBOOLE_0:def_10 ::_thesis: {_{X}_} \/ {_{Y}_} c= {_{(X \/ Y)}_}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {_{(X \/ Y)}_} or y in {_{X}_} \/ {_{Y}_} )
assume y in {_{(X \/ Y)}_} ; ::_thesis: y in {_{X}_} \/ {_{Y}_}
then consider x being set such that
A1: y = {x} and
A2: x in X \/ Y by Th1;
( x in X or x in Y ) by A2, XBOOLE_0:def_3;
then ( y in {_{X}_} or y in {_{Y}_} ) by A1, Th1;
hence y in {_{X}_} \/ {_{Y}_} by XBOOLE_0:def_3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {_{X}_} \/ {_{Y}_} or y in {_{(X \/ Y)}_} )
assume A3: y in {_{X}_} \/ {_{Y}_} ; ::_thesis: y in {_{(X \/ Y)}_}
percases ( y in {_{X}_} or y in {_{Y}_} ) by A3, XBOOLE_0:def_3;
suppose y in {_{X}_} ; ::_thesis: y in {_{(X \/ Y)}_}
then consider x being set such that
A4: y = {x} and
A5: x in X by Th1;
x in X \/ Y by A5, XBOOLE_0:def_3;
hence y in {_{(X \/ Y)}_} by A4, Th1; ::_thesis: verum
end;
suppose y in {_{Y}_} ; ::_thesis: y in {_{(X \/ Y)}_}
then consider x being set such that
A6: y = {x} and
A7: x in Y by Th1;
x in X \/ Y by A7, XBOOLE_0:def_3;
hence y in {_{(X \/ Y)}_} by A6, Th1; ::_thesis: verum
end;
end;
end;
theorem Th4: :: RELSET_2:4
for X, Y being set holds {_{(X /\ Y)}_} = {_{X}_} /\ {_{Y}_}
proof
let X, Y be set ; ::_thesis: {_{(X /\ Y)}_} = {_{X}_} /\ {_{Y}_}
thus {_{(X /\ Y)}_} c= {_{X}_} /\ {_{Y}_} :: according to XBOOLE_0:def_10 ::_thesis: {_{X}_} /\ {_{Y}_} c= {_{(X /\ Y)}_}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {_{(X /\ Y)}_} or y in {_{X}_} /\ {_{Y}_} )
assume y in {_{(X /\ Y)}_} ; ::_thesis: y in {_{X}_} /\ {_{Y}_}
then consider x being set such that
A1: y = {x} and
A2: x in X /\ Y by Th1;
A3: x in X by A2, XBOOLE_0:def_4;
A4: x in Y by A2, XBOOLE_0:def_4;
A5: y in {_{X}_} by A1, A3, Th1;
y in {_{Y}_} by A1, A4, Th1;
hence y in {_{X}_} /\ {_{Y}_} by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {_{X}_} /\ {_{Y}_} or y in {_{(X /\ Y)}_} )
assume A6: y in {_{X}_} /\ {_{Y}_} ; ::_thesis: y in {_{(X /\ Y)}_}
then A7: y in {_{X}_} by XBOOLE_0:def_4;
A8: y in {_{Y}_} by A6, XBOOLE_0:def_4;
consider x being set such that
A9: y = {x} and
A10: x in X by A7, Th1;
consider x1 being set such that
A11: y = {x1} and
A12: x1 in Y by A8, Th1;
x = x1 by A9, A11, ZFMISC_1:3;
then x in X /\ Y by A10, A12, XBOOLE_0:def_4;
hence y in {_{(X /\ Y)}_} by A9, Th1; ::_thesis: verum
end;
theorem :: RELSET_2:5
for X, Y being set holds {_{(X \ Y)}_} = {_{X}_} \ {_{Y}_}
proof
let X, Y be set ; ::_thesis: {_{(X \ Y)}_} = {_{X}_} \ {_{Y}_}
thus {_{(X \ Y)}_} c= {_{X}_} \ {_{Y}_} :: according to XBOOLE_0:def_10 ::_thesis: {_{X}_} \ {_{Y}_} c= {_{(X \ Y)}_}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {_{(X \ Y)}_} or y in {_{X}_} \ {_{Y}_} )
assume y in {_{(X \ Y)}_} ; ::_thesis: y in {_{X}_} \ {_{Y}_}
then consider x being set such that
A1: y = {x} and
A2: x in X \ Y by Th1;
A3: not x in Y by A2, XBOOLE_0:def_5;
A4: y in {_{X}_} by A1, A2, Th1;
not y in {_{Y}_}
proof
assume y in {_{Y}_} ; ::_thesis: contradiction
then ex x1 being set st
( y = {x1} & x1 in Y ) by Th1;
hence contradiction by A1, A3, ZFMISC_1:3; ::_thesis: verum
end;
hence y in {_{X}_} \ {_{Y}_} by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {_{X}_} \ {_{Y}_} or y in {_{(X \ Y)}_} )
assume A5: y in {_{X}_} \ {_{Y}_} ; ::_thesis: y in {_{(X \ Y)}_}
then A6: y in {_{X}_} by XBOOLE_0:def_5;
A7: not y in {_{Y}_} by A5, XBOOLE_0:def_5;
consider x being set such that
A8: y = {x} and
A9: x in X by A6, Th1;
not x in Y by A7, A8, Th1;
then x in X \ Y by A9, XBOOLE_0:def_5;
hence y in {_{(X \ Y)}_} by A8, Th1; ::_thesis: verum
end;
theorem Th6: :: RELSET_2:6
for X, Y being set holds
( X c= Y iff {_{X}_} c= {_{Y}_} )
proof
let X, Y be set ; ::_thesis: ( X c= Y iff {_{X}_} c= {_{Y}_} )
thus ( X c= Y implies {_{X}_} c= {_{Y}_} ) ::_thesis: ( {_{X}_} c= {_{Y}_} implies X c= Y )
proof
assume A1: X c= Y ; ::_thesis: {_{X}_} c= {_{Y}_}
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {_{X}_} or y in {_{Y}_} )
assume y in {_{X}_} ; ::_thesis: y in {_{Y}_}
then ex x being set st
( y = {x} & x in X ) by Th1;
hence y in {_{Y}_} by A1, Th1; ::_thesis: verum
end;
assume A2: {_{X}_} c= {_{Y}_} ; ::_thesis: X c= Y
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in Y )
assume y in X ; ::_thesis: y in Y
then {y} in {_{X}_} by Th1;
then ex x1 being set st
( {y} = {x1} & x1 in Y ) by A2, Th1;
hence y in Y by ZFMISC_1:3; ::_thesis: verum
end;
theorem :: RELSET_2:7
for M being set
for B1, B2 being Subset-Family of M holds (Intersect B1) /\ (Intersect B2) c= Intersect (B1 /\ B2)
proof
let M be set ; ::_thesis: for B1, B2 being Subset-Family of M holds (Intersect B1) /\ (Intersect B2) c= Intersect (B1 /\ B2)
let B1, B2 be Subset-Family of M; ::_thesis: (Intersect B1) /\ (Intersect B2) c= Intersect (B1 /\ B2)
Intersect (B1 \/ B2) c= Intersect (B1 /\ B2) by SETFAM_1:44, XBOOLE_1:29;
hence (Intersect B1) /\ (Intersect B2) c= Intersect (B1 /\ B2) by MSSUBFAM:8; ::_thesis: verum
end;
theorem :: RELSET_2:8
for P, Q, R being Relation holds (P /\ Q) * R c= (P * R) /\ (Q * R)
proof
let P, Q, R be Relation; ::_thesis: (P /\ Q) * R c= (P * R) /\ (Q * R)
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in (P /\ Q) * R or [x,y] in (P * R) /\ (Q * R) )
assume [x,y] in (P /\ Q) * R ; ::_thesis: [x,y] in (P * R) /\ (Q * R)
then consider z being set such that
A1: [x,z] in P /\ Q and
A2: [z,y] in R by RELAT_1:def_8;
A3: [x,z] in P by A1, XBOOLE_0:def_4;
A4: [x,z] in Q by A1, XBOOLE_0:def_4;
A5: [x,y] in P * R by A2, A3, RELAT_1:def_8;
[x,y] in Q * R by A2, A4, RELAT_1:def_8;
hence [x,y] in (P * R) /\ (Q * R) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
begin
theorem Th9: :: RELSET_2:9
for y, x being set
for R being Relation holds
( y in Im (R,x) iff [x,y] in R )
proof
let y, x be set ; ::_thesis: for R being Relation holds
( y in Im (R,x) iff [x,y] in R )
let R be Relation; ::_thesis: ( y in Im (R,x) iff [x,y] in R )
thus ( y in Im (R,x) implies [x,y] in R ) ::_thesis: ( [x,y] in R implies y in Im (R,x) )
proof
assume y in Im (R,x) ; ::_thesis: [x,y] in R
then ex a being set st
( [a,y] in R & a in {x} ) by RELAT_1:def_13;
hence [x,y] in R by TARSKI:def_1; ::_thesis: verum
end;
assume A1: [x,y] in R ; ::_thesis: y in Im (R,x)
x in {x} by TARSKI:def_1;
hence y in Im (R,x) by A1, RELAT_1:def_13; ::_thesis: verum
end;
theorem Th10: :: RELSET_2:10
for x being set
for R1, R2 being Relation holds Im ((R1 \/ R2),x) = (Im (R1,x)) \/ (Im (R2,x))
proof
let x be set ; ::_thesis: for R1, R2 being Relation holds Im ((R1 \/ R2),x) = (Im (R1,x)) \/ (Im (R2,x))
let R1, R2 be Relation; ::_thesis: Im ((R1 \/ R2),x) = (Im (R1,x)) \/ (Im (R2,x))
thus Im ((R1 \/ R2),x) c= (Im (R1,x)) \/ (Im (R2,x)) :: according to XBOOLE_0:def_10 ::_thesis: (Im (R1,x)) \/ (Im (R2,x)) c= Im ((R1 \/ R2),x)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Im ((R1 \/ R2),x) or y in (Im (R1,x)) \/ (Im (R2,x)) )
assume y in Im ((R1 \/ R2),x) ; ::_thesis: y in (Im (R1,x)) \/ (Im (R2,x))
then [x,y] in R1 \/ R2 by Th9;
then ( [x,y] in R1 or [x,y] in R2 ) by XBOOLE_0:def_3;
then ( y in Im (R1,x) or y in Im (R2,x) ) by Th9;
hence y in (Im (R1,x)) \/ (Im (R2,x)) by XBOOLE_0:def_3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Im (R1,x)) \/ (Im (R2,x)) or y in Im ((R1 \/ R2),x) )
assume A1: y in (Im (R1,x)) \/ (Im (R2,x)) ; ::_thesis: y in Im ((R1 \/ R2),x)
percases ( y in Im (R1,x) or y in Im (R2,x) ) by A1, XBOOLE_0:def_3;
suppose y in Im (R1,x) ; ::_thesis: y in Im ((R1 \/ R2),x)
then [x,y] in R1 by Th9;
then [x,y] in R1 \/ R2 by XBOOLE_0:def_3;
hence y in Im ((R1 \/ R2),x) by Th9; ::_thesis: verum
end;
suppose y in Im (R2,x) ; ::_thesis: y in Im ((R1 \/ R2),x)
then [x,y] in R2 by Th9;
then [x,y] in R1 \/ R2 by XBOOLE_0:def_3;
hence y in Im ((R1 \/ R2),x) by Th9; ::_thesis: verum
end;
end;
end;
theorem Th11: :: RELSET_2:11
for x being set
for R1, R2 being Relation holds Im ((R1 /\ R2),x) = (Im (R1,x)) /\ (Im (R2,x))
proof
let x be set ; ::_thesis: for R1, R2 being Relation holds Im ((R1 /\ R2),x) = (Im (R1,x)) /\ (Im (R2,x))
let R1, R2 be Relation; ::_thesis: Im ((R1 /\ R2),x) = (Im (R1,x)) /\ (Im (R2,x))
thus Im ((R1 /\ R2),x) c= (Im (R1,x)) /\ (Im (R2,x)) :: according to XBOOLE_0:def_10 ::_thesis: (Im (R1,x)) /\ (Im (R2,x)) c= Im ((R1 /\ R2),x)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Im ((R1 /\ R2),x) or y in (Im (R1,x)) /\ (Im (R2,x)) )
assume y in Im ((R1 /\ R2),x) ; ::_thesis: y in (Im (R1,x)) /\ (Im (R2,x))
then A1: [x,y] in R1 /\ R2 by Th9;
then A2: [x,y] in R1 by XBOOLE_0:def_4;
A3: [x,y] in R2 by A1, XBOOLE_0:def_4;
A4: y in Im (R1,x) by A2, Th9;
y in Im (R2,x) by A3, Th9;
hence y in (Im (R1,x)) /\ (Im (R2,x)) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Im (R1,x)) /\ (Im (R2,x)) or y in Im ((R1 /\ R2),x) )
assume A5: y in (Im (R1,x)) /\ (Im (R2,x)) ; ::_thesis: y in Im ((R1 /\ R2),x)
then A6: y in Im (R1,x) by XBOOLE_0:def_4;
A7: y in Im (R2,x) by A5, XBOOLE_0:def_4;
A8: [x,y] in R1 by A6, Th9;
[x,y] in R2 by A7, Th9;
then [x,y] in R1 /\ R2 by A8, XBOOLE_0:def_4;
hence y in Im ((R1 /\ R2),x) by Th9; ::_thesis: verum
end;
theorem :: RELSET_2:12
for x being set
for R1, R2 being Relation holds Im ((R1 \ R2),x) = (Im (R1,x)) \ (Im (R2,x))
proof
let x be set ; ::_thesis: for R1, R2 being Relation holds Im ((R1 \ R2),x) = (Im (R1,x)) \ (Im (R2,x))
let R1, R2 be Relation; ::_thesis: Im ((R1 \ R2),x) = (Im (R1,x)) \ (Im (R2,x))
thus Im ((R1 \ R2),x) c= (Im (R1,x)) \ (Im (R2,x)) :: according to XBOOLE_0:def_10 ::_thesis: (Im (R1,x)) \ (Im (R2,x)) c= Im ((R1 \ R2),x)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Im ((R1 \ R2),x) or y in (Im (R1,x)) \ (Im (R2,x)) )
assume y in Im ((R1 \ R2),x) ; ::_thesis: y in (Im (R1,x)) \ (Im (R2,x))
then A1: [x,y] in R1 \ R2 by Th9;
then A2: not [x,y] in R2 by XBOOLE_0:def_5;
A3: y in Im (R1,x) by A1, Th9;
not y in Im (R2,x) by A2, Th9;
hence y in (Im (R1,x)) \ (Im (R2,x)) by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Im (R1,x)) \ (Im (R2,x)) or y in Im ((R1 \ R2),x) )
assume A4: y in (Im (R1,x)) \ (Im (R2,x)) ; ::_thesis: y in Im ((R1 \ R2),x)
then A5: not y in Im (R2,x) by XBOOLE_0:def_5;
A6: [x,y] in R1 by A4, Th9;
not [x,y] in R2 by A5, Th9;
then [x,y] in R1 \ R2 by A6, XBOOLE_0:def_5;
hence y in Im ((R1 \ R2),x) by Th9; ::_thesis: verum
end;
theorem :: RELSET_2:13
for X being set
for R1, R2 being Relation holds (R1 /\ R2) .: {_{X}_} c= (R1 .: {_{X}_}) /\ (R2 .: {_{X}_})
proof
let X be set ; ::_thesis: for R1, R2 being Relation holds (R1 /\ R2) .: {_{X}_} c= (R1 .: {_{X}_}) /\ (R2 .: {_{X}_})
let R1, R2 be Relation; ::_thesis: (R1 /\ R2) .: {_{X}_} c= (R1 .: {_{X}_}) /\ (R2 .: {_{X}_})
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (R1 /\ R2) .: {_{X}_} or y in (R1 .: {_{X}_}) /\ (R2 .: {_{X}_}) )
assume y in (R1 /\ R2) .: {_{X}_} ; ::_thesis: y in (R1 .: {_{X}_}) /\ (R2 .: {_{X}_})
then consider x being set such that
A1: [x,y] in R1 /\ R2 and
A2: x in {_{X}_} by RELAT_1:def_13;
A3: [x,y] in R1 by A1, XBOOLE_0:def_4;
A4: [x,y] in R2 by A1, XBOOLE_0:def_4;
A5: y in R1 .: {_{X}_} by A2, A3, RELAT_1:def_13;
y in R2 .: {_{X}_} by A2, A4, RELAT_1:def_13;
hence y in (R1 .: {_{X}_}) /\ (R2 .: {_{X}_}) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
definition
let X, Y be set ;
let R be Relation of X,Y;
let x be set ;
:: original: Im
redefine func Im (R,x) -> Subset of Y;
coherence
Im (R,x) is Subset of Y
proof
Im (R,x) = R .: {x} ;
hence Im (R,x) is Subset of Y ; ::_thesis: verum
end;
:: original: Coim
redefine func Coim (R,x) -> Subset of X;
coherence
Coim (R,x) is Subset of X
proof
Coim (R,x) = R " {x} ;
hence Coim (R,x) is Subset of X ; ::_thesis: verum
end;
end;
theorem :: RELSET_2:14
for A being set
for F being Subset-Family of A
for R being Relation holds R .: (union F) = union { (R .: X) where X is Subset of A : X in F }
proof
let A be set ; ::_thesis: for F being Subset-Family of A
for R being Relation holds R .: (union F) = union { (R .: X) where X is Subset of A : X in F }
let F be Subset-Family of A; ::_thesis: for R being Relation holds R .: (union F) = union { (R .: X) where X is Subset of A : X in F }
let R be Relation; ::_thesis: R .: (union F) = union { (R .: X) where X is Subset of A : X in F }
thus R .: (union F) c= union { (R .: f) where f is Subset of A : f in F } :: according to XBOOLE_0:def_10 ::_thesis: union { (R .: X) where X is Subset of A : X in F } c= R .: (union F)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .: (union F) or y in union { (R .: f) where f is Subset of A : f in F } )
assume y in R .: (union F) ; ::_thesis: y in union { (R .: f) where f is Subset of A : f in F }
then consider x being set such that
A1: [x,y] in R and
A2: x in union F by RELAT_1:def_13;
consider Y being set such that
A3: x in Y and
A4: Y in F by A2, TARSKI:def_4;
set Z = R .: Y;
A5: y in R .: Y by A1, A3, RELAT_1:def_13;
R .: Y in { (R .: f) where f is Subset of A : f in F } by A4;
hence y in union { (R .: f) where f is Subset of A : f in F } by A5, TARSKI:def_4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union { (R .: X) where X is Subset of A : X in F } or y in R .: (union F) )
assume y in union { (R .: f) where f is Subset of A : f in F } ; ::_thesis: y in R .: (union F)
then consider Y being set such that
A6: y in Y and
A7: Y in { (R .: f) where f is Subset of A : f in F } by TARSKI:def_4;
consider f being Subset of A such that
A8: Y = R .: f and
A9: f in F by A7;
consider x being set such that
A10: [x,y] in R and
A11: x in f by A6, A8, RELAT_1:def_13;
x in union F by A9, A11, TARSKI:def_4;
hence y in R .: (union F) by A10, RELAT_1:def_13; ::_thesis: verum
end;
theorem Th15: :: RELSET_2:15
for A being non empty set
for X being Subset of A holds X = union { {x} where x is Element of A : x in X }
proof
let A be non empty set ; ::_thesis: for X being Subset of A holds X = union { {x} where x is Element of A : x in X }
let X be Subset of A; ::_thesis: X = union { {x} where x is Element of A : x in X }
thus X c= union { {x} where x is Element of A : x in X } :: according to XBOOLE_0:def_10 ::_thesis: union { {x} where x is Element of A : x in X } c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in union { {x} where x is Element of A : x in X } )
assume A1: a in X ; ::_thesis: a in union { {x} where x is Element of A : x in X }
set Y = {a};
A2: a in {a} by TARSKI:def_1;
{a} in { {x} where x is Element of A : x in X } by A1;
hence a in union { {x} where x is Element of A : x in X } by A2, TARSKI:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { {x} where x is Element of A : x in X } or a in X )
assume a in union { {x} where x is Element of A : x in X } ; ::_thesis: a in X
then consider Y being set such that
A3: a in Y and
A4: Y in { {x} where x is Element of A : x in X } by TARSKI:def_4;
ex x being Element of A st
( Y = {x} & x in X ) by A4;
hence a in X by A3, TARSKI:def_1; ::_thesis: verum
end;
theorem :: RELSET_2:16
for A being non empty set
for X being Subset of A holds { {x} where x is Element of A : x in X } is Subset-Family of A
proof
let A be non empty set ; ::_thesis: for X being Subset of A holds { {x} where x is Element of A : x in X } is Subset-Family of A
let X be Subset of A; ::_thesis: { {x} where x is Element of A : x in X } is Subset-Family of A
{ {x} where x is Element of A : x in X } c= bool A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { {x} where x is Element of A : x in X } or a in bool A )
assume a in { {x} where x is Element of A : x in X } ; ::_thesis: a in bool A
then ex x being Element of A st
( a = {x} & x in X ) ;
then a c= A by ZFMISC_1:31;
hence a in bool A ; ::_thesis: verum
end;
hence { {x} where x is Element of A : x in X } is Subset-Family of A ; ::_thesis: verum
end;
theorem :: RELSET_2:17
for A being non empty set
for B being set
for X being Subset of A
for R being Relation of A,B holds R .: X = union { (Class (R,x)) where x is Element of A : x in X }
proof
let A be non empty set ; ::_thesis: for B being set
for X being Subset of A
for R being Relation of A,B holds R .: X = union { (Class (R,x)) where x is Element of A : x in X }
let B be set ; ::_thesis: for X being Subset of A
for R being Relation of A,B holds R .: X = union { (Class (R,x)) where x is Element of A : x in X }
let X be Subset of A; ::_thesis: for R being Relation of A,B holds R .: X = union { (Class (R,x)) where x is Element of A : x in X }
let R be Relation of A,B; ::_thesis: R .: X = union { (Class (R,x)) where x is Element of A : x in X }
thus R .: X c= union { (Class (R,x)) where x is Element of A : x in X } :: according to XBOOLE_0:def_10 ::_thesis: union { (Class (R,x)) where x is Element of A : x in X } c= R .: X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .: X or y in union { (Class (R,x)) where x is Element of A : x in X } )
assume y in R .: X ; ::_thesis: y in union { (Class (R,x)) where x is Element of A : x in X }
then consider x1 being set such that
A1: [x1,y] in R and
A2: x1 in X by RELAT_1:def_13;
x1 in union { {x} where x is Element of A : x in X } by A2, Th15;
then consider S being set such that
A3: x1 in S and
A4: S in { {x} where x is Element of A : x in X } by TARSKI:def_4;
consider x being Element of A such that
A5: S = {x} and
A6: x in X by A4;
A7: y in R .: {x} by A1, A3, A5, RELAT_1:def_13;
set Y = R .: {x};
R .: {x} = Class (R,x) ;
then R .: {x} in { (Class (R,xs)) where xs is Element of A : xs in X } by A6;
hence y in union { (Class (R,x)) where x is Element of A : x in X } by A7, TARSKI:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { (Class (R,x)) where x is Element of A : x in X } or a in R .: X )
assume a in union { (Class (R,x)) where x is Element of A : x in X } ; ::_thesis: a in R .: X
then consider Y being set such that
A8: a in Y and
A9: Y in { (Class (R,x)) where x is Element of A : x in X } by TARSKI:def_4;
consider x being Element of A such that
A10: Y = Class (R,x) and
A11: x in X by A9;
Y c= R .: X
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Y or b in R .: X )
assume b in Y ; ::_thesis: b in R .: X
then consider x1 being set such that
A12: [x1,b] in R and
A13: x1 in {x} by A10, RELAT_1:def_13;
x1 = x by A13, TARSKI:def_1;
hence b in R .: X by A11, A12, RELAT_1:def_13; ::_thesis: verum
end;
hence a in R .: X by A8; ::_thesis: verum
end;
theorem :: RELSET_2:18
for A being non empty set
for B being set
for X being Subset of A
for R being Relation of A,B holds { (R .: x) where x is Element of A : x in X } is Subset-Family of B
proof
let A be non empty set ; ::_thesis: for B being set
for X being Subset of A
for R being Relation of A,B holds { (R .: x) where x is Element of A : x in X } is Subset-Family of B
let B be set ; ::_thesis: for X being Subset of A
for R being Relation of A,B holds { (R .: x) where x is Element of A : x in X } is Subset-Family of B
let X be Subset of A; ::_thesis: for R being Relation of A,B holds { (R .: x) where x is Element of A : x in X } is Subset-Family of B
let R be Relation of A,B; ::_thesis: { (R .: x) where x is Element of A : x in X } is Subset-Family of B
deffunc H1( Element of A) -> Element of bool B = R .: $1;
defpred S1[ set ] means $1 in X;
set Y = { H1(x) where x is Element of A : S1[x] } ;
thus { H1(x) where x is Element of A : S1[x] } is Subset-Family of B from DOMAIN_1:sch_8(); ::_thesis: verum
end;
definition
let A be set ;
let R be Relation;
func .: (R,A) -> Function means :Def1: :: RELSET_2:def 1
( dom it = bool A & ( for X being set st X c= A holds
it . X = R .: X ) );
existence
ex b1 being Function st
( dom b1 = bool A & ( for X being set st X c= A holds
b1 . X = R .: X ) )
proof
defpred S1[ set , set ] means for X being set st $1 = X holds
$2 = R .: X;
A1: for x being set st x in bool A holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in bool A implies ex y being set st S1[x,y] )
assume x in bool A ; ::_thesis: ex y being set st S1[x,y]
take R .: x ; ::_thesis: S1[x,R .: x]
thus S1[x,R .: x] ; ::_thesis: verum
end;
consider g being Function such that
A2: dom g = bool A and
A3: for x being set st x in bool A holds
S1[x,g . x] from CLASSES1:sch_1(A1);
take g ; ::_thesis: ( dom g = bool A & ( for X being set st X c= A holds
g . X = R .: X ) )
thus ( dom g = bool A & ( for X being set st X c= A holds
g . X = R .: X ) ) by A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = bool A & ( for X being set st X c= A holds
b1 . X = R .: X ) & dom b2 = bool A & ( for X being set st X c= A holds
b2 . X = R .: X ) holds
b1 = b2
proof
let R1, R2 be Function; ::_thesis: ( dom R1 = bool A & ( for X being set st X c= A holds
R1 . X = R .: X ) & dom R2 = bool A & ( for X being set st X c= A holds
R2 . X = R .: X ) implies R1 = R2 )
assume that
A4: dom R1 = bool A and
A5: for X being set st X c= A holds
R1 . X = R .: X and
A6: dom R2 = bool A and
A7: for X being set st X c= A holds
R2 . X = R .: X ; ::_thesis: R1 = R2
for x being set st x in bool A holds
R1 . x = R2 . x
proof
let x be set ; ::_thesis: ( x in bool A implies R1 . x = R2 . x )
assume A8: x in bool A ; ::_thesis: R1 . x = R2 . x
then R1 . x = R .: x by A5;
hence R1 . x = R2 . x by A7, A8; ::_thesis: verum
end;
hence R1 = R2 by A4, A6, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines .: RELSET_2:def_1_:_
for A being set
for R being Relation
for b3 being Function holds
( b3 = .: (R,A) iff ( dom b3 = bool A & ( for X being set st X c= A holds
b3 . X = R .: X ) ) );
notation
let B, A be set ;
let R be Subset of [:A,B:];
synonym .: R for .: (A,B);
end;
theorem Th19: :: RELSET_2:19
for X, A, B being set
for R being Subset of [:A,B:] st X in dom (.: ) holds
(.: ) . X = R .: X
proof
let X be set ; ::_thesis: for A, B being set
for R being Subset of [:A,B:] st X in dom (.: ) holds
(.: ) . X = R .: X
let A, B be set ; ::_thesis: for R being Subset of [:A,B:] st X in dom (.: ) holds
(.: ) . X = R .: X
let R be Subset of [:A,B:]; ::_thesis: ( X in dom (.: ) implies (.: ) . X = R .: X )
assume X in dom (.: ) ; ::_thesis: (.: ) . X = R .: X
then X in bool A by Def1;
hence (.: ) . X = R .: X by Def1; ::_thesis: verum
end;
theorem Th20: :: RELSET_2:20
for A, B being set
for R being Subset of [:A,B:] holds rng (.: ) c= bool (rng R)
proof
let A, B be set ; ::_thesis: for R being Subset of [:A,B:] holds rng (.: ) c= bool (rng R)
let R be Subset of [:A,B:]; ::_thesis: rng (.: ) c= bool (rng R)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (.: ) or y in bool (rng R) )
assume y in rng (.: ) ; ::_thesis: y in bool (rng R)
then consider x being set such that
A1: x in dom (.: ) and
A2: y = (.: ) . x by FUNCT_1:def_3;
y = R .: x by A1, A2, Th19;
then y c= rng R by RELAT_1:111;
hence y in bool (rng R) ; ::_thesis: verum
end;
theorem Th21: :: RELSET_2:21
for A, B being set
for R being Subset of [:A,B:] holds .: is Function of (bool A),(bool (rng R))
proof
let A, B be set ; ::_thesis: for R being Subset of [:A,B:] holds .: is Function of (bool A),(bool (rng R))
let R be Subset of [:A,B:]; ::_thesis: .: is Function of (bool A),(bool (rng R))
A1: dom (.: ) = bool A by Def1;
rng (.: ) c= bool (rng R) by Th20;
hence .: is Function of (bool A),(bool (rng R)) by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
definition
let B, A be set ;
let R be Subset of [:A,B:];
:: original: .:
redefine func .: R -> Function of (bool A),(bool B);
correctness
coherence
.: (R,A) is Function of (bool A),(bool B);
proof
A1: dom (.: ) = bool A by Def1;
.: is Function of (bool A),(bool (rng R)) by Th21;
then A2: rng (.: ) c= bool (rng R) by RELAT_1:def_19;
bool (rng R) c= bool B by ZFMISC_1:67;
then rng (.: ) c= bool B by A2, XBOOLE_1:1;
hence .: (R,A) is Function of (bool A),(bool B) by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;
theorem :: RELSET_2:22
for A, B being set
for R being Subset of [:A,B:] holds union ((.: R) .: A) c= R .: (union A)
proof
let A, B be set ; ::_thesis: for R being Subset of [:A,B:] holds union ((.: R) .: A) c= R .: (union A)
let R be Subset of [:A,B:]; ::_thesis: union ((.: R) .: A) c= R .: (union A)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union ((.: R) .: A) or y in R .: (union A) )
assume y in union ((.: R) .: A) ; ::_thesis: y in R .: (union A)
then consider Z being set such that
A1: y in Z and
A2: Z in (.: R) .: A by TARSKI:def_4;
consider X being set such that
A3: X in dom (.: R) and
A4: X in A and
A5: Z = (.: R) . X by A2, FUNCT_1:def_6;
y in R .: X by A1, A3, A5, Th19;
then consider x being set such that
A6: [x,y] in R and
A7: x in X by RELAT_1:def_13;
x in union A by A4, A7, TARSKI:def_4;
hence y in R .: (union A) by A6, RELAT_1:def_13; ::_thesis: verum
end;
begin
definition
let A, B be set ;
let X be Subset of A;
let R be Subset of [:A,B:];
funcR .:^ X -> set equals :: RELSET_2:def 2
Intersect ((.: R) .: {_{X}_});
correctness
coherence
Intersect ((.: R) .: {_{X}_}) is set ;
;
end;
:: deftheorem defines .:^ RELSET_2:def_2_:_
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds R .:^ X = Intersect ((.: R) .: {_{X}_});
definition
let A, B be set ;
let X be Subset of A;
let R be Subset of [:A,B:];
:: original: .:^
redefine funcR .:^ X -> Subset of B;
coherence
R .:^ X is Subset of B ;
end;
theorem Th23: :: RELSET_2:23
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds
( (.: R) .: {_{X}_} = {} iff X = {} )
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R being Subset of [:A,B:] holds
( (.: R) .: {_{X}_} = {} iff X = {} )
let X be Subset of A; ::_thesis: for R being Subset of [:A,B:] holds
( (.: R) .: {_{X}_} = {} iff X = {} )
let R be Subset of [:A,B:]; ::_thesis: ( (.: R) .: {_{X}_} = {} iff X = {} )
thus ( (.: R) .: {_{X}_} = {} implies X = {} ) ::_thesis: ( X = {} implies (.: R) .: {_{X}_} = {} )
proof
assume (.: R) .: {_{X}_} = {} ; ::_thesis: X = {}
then dom (.: R) misses {_{X}_} by RELAT_1:118;
then A1: bool A misses {_{X}_} by Def1;
{_{X}_} c= bool A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {_{X}_} or y in bool A )
assume y in {_{X}_} ; ::_thesis: y in bool A
then consider x being set such that
A2: y = {x} and
A3: x in X by Th1;
A4: x in A by A3;
y c= A
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in y or x1 in A )
assume x1 in y ; ::_thesis: x1 in A
hence x1 in A by A2, A4, TARSKI:def_1; ::_thesis: verum
end;
hence y in bool A ; ::_thesis: verum
end;
then A5: (bool A) /\ {_{X}_} = {_{X}_} by XBOOLE_1:28;
assume X <> {} ; ::_thesis: contradiction
then {_{X}_} <> {} by Th2;
hence contradiction by A1, A5, XBOOLE_0:def_7; ::_thesis: verum
end;
assume X = {} ; ::_thesis: (.: R) .: {_{X}_} = {}
then {_{X}_} = {} by Th2;
hence (.: R) .: {_{X}_} = {} ; ::_thesis: verum
end;
theorem Th24: :: RELSET_2:24
for A, B, y being set
for X being Subset of A
for R being Subset of [:A,B:] st y in R .:^ X holds
for x being set st x in X holds
y in Im (R,x)
proof
let A, B, y be set ; ::_thesis: for X being Subset of A
for R being Subset of [:A,B:] st y in R .:^ X holds
for x being set st x in X holds
y in Im (R,x)
let X be Subset of A; ::_thesis: for R being Subset of [:A,B:] st y in R .:^ X holds
for x being set st x in X holds
y in Im (R,x)
let R be Subset of [:A,B:]; ::_thesis: ( y in R .:^ X implies for x being set st x in X holds
y in Im (R,x) )
assume A1: y in R .:^ X ; ::_thesis: for x being set st x in X holds
y in Im (R,x)
percases ( (.: R) .: {_{X}_} = {} or (.: R) .: {_{X}_} <> {} ) ;
suppose (.: R) .: {_{X}_} = {} ; ::_thesis: for x being set st x in X holds
y in Im (R,x)
hence for x being set st x in X holds
y in Im (R,x) by Th23; ::_thesis: verum
end;
suppose (.: R) .: {_{X}_} <> {} ; ::_thesis: for x being set st x in X holds
y in Im (R,x)
then A2: y in meet ((.: R) .: {_{X}_}) by A1, SETFAM_1:def_9;
for x being set st x in X holds
y in R .: {x}
proof
let x be set ; ::_thesis: ( x in X implies y in R .: {x} )
assume A3: x in X ; ::_thesis: y in R .: {x}
then A4: {x} in {_{X}_} by Th1;
A5: {x} c= A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} or a in A )
assume a in {x} ; ::_thesis: a in A
then a = x by TARSKI:def_1;
hence a in A by A3; ::_thesis: verum
end;
then A6: (.: R) . {x} = R .: {x} by Def1;
dom (.: R) = bool A by Def1;
then [{x},(R .: {x})] in .: R by A5, A6, FUNCT_1:1;
then R .: {x} in (.: R) .: {_{X}_} by A4, RELAT_1:def_13;
hence y in R .: {x} by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence for x being set st x in X holds
y in Im (R,x) ; ::_thesis: verum
end;
end;
end;
theorem Th25: :: RELSET_2:25
for B being non empty set
for A being set
for X being Subset of A
for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
proof
let B be non empty set ; ::_thesis: for A being set
for X being Subset of A
for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
let A be set ; ::_thesis: for X being Subset of A
for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
let X be Subset of A; ::_thesis: for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
let y be Element of B; ::_thesis: for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
let R be Subset of [:A,B:]; ::_thesis: ( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
thus ( y in R .:^ X implies for x being set st x in X holds
y in Im (R,x) ) by Th24; ::_thesis: ( ( for x being set st x in X holds
y in Im (R,x) ) implies y in R .:^ X )
assume A1: for x being set st x in X holds
y in Im (R,x) ; ::_thesis: y in R .:^ X
percases ( (.: R) .: {_{X}_} = {} or (.: R) .: {_{X}_} <> {} ) ;
suppose (.: R) .: {_{X}_} = {} ; ::_thesis: y in R .:^ X
then Intersect ((.: R) .: {_{X}_}) = B by SETFAM_1:def_9;
hence y in R .:^ X ; ::_thesis: verum
end;
supposeA2: (.: R) .: {_{X}_} <> {} ; ::_thesis: y in R .:^ X
then A3: Intersect ((.: R) .: {_{X}_}) = meet ((.: R) .: {_{X}_}) by SETFAM_1:def_9;
for Y being set st Y in (.: R) .: {_{X}_} holds
y in Y
proof
let Y be set ; ::_thesis: ( Y in (.: R) .: {_{X}_} implies y in Y )
assume Y in (.: R) .: {_{X}_} ; ::_thesis: y in Y
then consider z being set such that
A4: [z,Y] in .: R and
A5: z in {_{X}_} by RELAT_1:def_13;
consider x being set such that
A6: z = {x} and
A7: x in X by A5, Th1;
A8: z in dom (.: R) by A4, FUNCT_1:1;
Y = (.: R) . z by A4, FUNCT_1:1;
then Y = Im (R,x) by A6, A8, Def1;
hence y in Y by A1, A7; ::_thesis: verum
end;
hence y in R .:^ X by A2, A3, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
theorem :: RELSET_2:26
for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] st (.: R) .: {_{X1}_} = {} holds
R .:^ (X1 \/ X2) = R .:^ X2
proof
let A, B be set ; ::_thesis: for X1, X2 being Subset of A
for R being Subset of [:A,B:] st (.: R) .: {_{X1}_} = {} holds
R .:^ (X1 \/ X2) = R .:^ X2
let X1, X2 be Subset of A; ::_thesis: for R being Subset of [:A,B:] st (.: R) .: {_{X1}_} = {} holds
R .:^ (X1 \/ X2) = R .:^ X2
let R be Subset of [:A,B:]; ::_thesis: ( (.: R) .: {_{X1}_} = {} implies R .:^ (X1 \/ X2) = R .:^ X2 )
A1: {_{(X1 \/ X2)}_} = {_{X1}_} \/ {_{X2}_} by Th3;
assume A2: (.: R) .: {_{X1}_} = {} ; ::_thesis: R .:^ (X1 \/ X2) = R .:^ X2
R .:^ (X1 \/ X2) = Intersect (((.: R) .: {_{X1}_}) \/ ((.: R) .: {_{X2}_})) by A1, RELAT_1:120
.= R .:^ X2 by A2 ;
hence R .:^ (X1 \/ X2) = R .:^ X2 ; ::_thesis: verum
end;
theorem :: RELSET_2:27
for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] holds R .:^ (X1 \/ X2) = (R .:^ X1) /\ (R .:^ X2)
proof
let A, B be set ; ::_thesis: for X1, X2 being Subset of A
for R being Subset of [:A,B:] holds R .:^ (X1 \/ X2) = (R .:^ X1) /\ (R .:^ X2)
let X1, X2 be Subset of A; ::_thesis: for R being Subset of [:A,B:] holds R .:^ (X1 \/ X2) = (R .:^ X1) /\ (R .:^ X2)
let R be Subset of [:A,B:]; ::_thesis: R .:^ (X1 \/ X2) = (R .:^ X1) /\ (R .:^ X2)
R .:^ (X1 \/ X2) = Intersect ((.: R) .: ({_{X1}_} \/ {_{X2}_})) by Th3
.= Intersect (((.: R) .: {_{X1}_}) \/ ((.: R) .: {_{X2}_})) by RELAT_1:120
.= (R .:^ X1) /\ (R .:^ X2) by MSSUBFAM:8 ;
hence R .:^ (X1 \/ X2) = (R .:^ X1) /\ (R .:^ X2) ; ::_thesis: verum
end;
theorem :: RELSET_2:28
for A being non empty set
for B being set
for F being Subset-Family of A
for R being Relation of A,B holds { (R .:^ X) where X is Subset of A : X in F } is Subset-Family of B
proof
let A be non empty set ; ::_thesis: for B being set
for F being Subset-Family of A
for R being Relation of A,B holds { (R .:^ X) where X is Subset of A : X in F } is Subset-Family of B
let B be set ; ::_thesis: for F being Subset-Family of A
for R being Relation of A,B holds { (R .:^ X) where X is Subset of A : X in F } is Subset-Family of B
let F be Subset-Family of A; ::_thesis: for R being Relation of A,B holds { (R .:^ X) where X is Subset of A : X in F } is Subset-Family of B
let R be Relation of A,B; ::_thesis: { (R .:^ X) where X is Subset of A : X in F } is Subset-Family of B
deffunc H1( Subset of A) -> Subset of B = R .:^ $1;
defpred S1[ set ] means $1 in F;
set Y = { H1(X) where X is Subset of A : S1[X] } ;
thus { H1(X) where X is Subset of A : S1[X] } is Subset-Family of B from DOMAIN_1:sch_8(); ::_thesis: verum
end;
theorem Th29: :: RELSET_2:29
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st X = {} holds
R .:^ X = B
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R being Subset of [:A,B:] st X = {} holds
R .:^ X = B
let X be Subset of A; ::_thesis: for R being Subset of [:A,B:] st X = {} holds
R .:^ X = B
let R be Subset of [:A,B:]; ::_thesis: ( X = {} implies R .:^ X = B )
assume X = {} ; ::_thesis: R .:^ X = B
then (.: R) .: {_{X}_} = {} by Th23;
hence R .:^ X = B by SETFAM_1:def_9; ::_thesis: verum
end;
theorem :: RELSET_2:30
for A being set
for B being non empty set
for R being Relation of A,B
for F being Subset-Family of A
for G being Subset-Family of B st G = { (R .:^ Y) where Y is Subset of A : Y in F } holds
R .:^ (union F) = Intersect G
proof
let A be set ; ::_thesis: for B being non empty set
for R being Relation of A,B
for F being Subset-Family of A
for G being Subset-Family of B st G = { (R .:^ Y) where Y is Subset of A : Y in F } holds
R .:^ (union F) = Intersect G
let B be non empty set ; ::_thesis: for R being Relation of A,B
for F being Subset-Family of A
for G being Subset-Family of B st G = { (R .:^ Y) where Y is Subset of A : Y in F } holds
R .:^ (union F) = Intersect G
let R be Relation of A,B; ::_thesis: for F being Subset-Family of A
for G being Subset-Family of B st G = { (R .:^ Y) where Y is Subset of A : Y in F } holds
R .:^ (union F) = Intersect G
let F be Subset-Family of A; ::_thesis: for G being Subset-Family of B st G = { (R .:^ Y) where Y is Subset of A : Y in F } holds
R .:^ (union F) = Intersect G
let G be Subset-Family of B; ::_thesis: ( G = { (R .:^ Y) where Y is Subset of A : Y in F } implies R .:^ (union F) = Intersect G )
assume A1: G = { (R .:^ Y) where Y is Subset of A : Y in F } ; ::_thesis: R .:^ (union F) = Intersect G
percases ( union F = {} or union F <> {} ) ;
supposeA2: union F = {} ; ::_thesis: R .:^ (union F) = Intersect G
then A3: R .:^ (union F) = B by Th29;
percases ( G <> {} or G = {} ) ;
supposeA4: G <> {} ; ::_thesis: R .:^ (union F) = Intersect G
G c= {B}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G or x in {B} )
assume x in G ; ::_thesis: x in {B}
then consider Y being Subset of A such that
A5: x = R .:^ Y and
A6: Y in F by A1;
Y = {} by A2, A6, ORDERS_1:6;
then (.: R) .: {_{Y}_} = {} by Th23;
then Intersect ((.: R) .: {_{Y}_}) = B by SETFAM_1:def_9;
hence x in {B} by A5, TARSKI:def_1; ::_thesis: verum
end;
then meet {B} c= meet G by A4, SETFAM_1:6;
then B c= meet G by SETFAM_1:10;
then meet G = B by XBOOLE_0:def_10;
hence R .:^ (union F) = Intersect G by A3, SETFAM_1:def_9; ::_thesis: verum
end;
suppose G = {} ; ::_thesis: R .:^ (union F) = Intersect G
hence R .:^ (union F) = Intersect G by A3, SETFAM_1:def_9; ::_thesis: verum
end;
end;
end;
suppose union F <> {} ; ::_thesis: R .:^ (union F) = Intersect G
then consider Z1 being set such that
Z1 <> {} and
A7: Z1 in F by ORDERS_1:6;
reconsider Z1 = Z1 as Subset of A by A7;
A8: G <> {}
proof
assume not G <> {} ; ::_thesis: contradiction
then not R .:^ Z1 in G ;
hence contradiction by A1, A7; ::_thesis: verum
end;
thus R .:^ (union F) c= Intersect G :: according to XBOOLE_0:def_10 ::_thesis: Intersect G c= R .:^ (union F)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in R .:^ (union F) or a in Intersect G )
assume A9: a in R .:^ (union F) ; ::_thesis: a in Intersect G
for Y being set st Y in G holds
a in Y
proof
let Z2 be set ; ::_thesis: ( Z2 in G implies a in Z2 )
assume Z2 in G ; ::_thesis: a in Z2
then consider Z3 being Subset of A such that
A10: Z2 = R .:^ Z3 and
A11: Z3 in F by A1;
reconsider a = a as Element of B by A9;
for x being set st x in Z3 holds
a in Im (R,x)
proof
let x be set ; ::_thesis: ( x in Z3 implies a in Im (R,x) )
assume x in Z3 ; ::_thesis: a in Im (R,x)
then x in union F by A11, TARSKI:def_4;
hence a in Im (R,x) by A9, Th24; ::_thesis: verum
end;
hence a in Z2 by A10, Th25; ::_thesis: verum
end;
then a in meet G by A8, SETFAM_1:def_1;
hence a in Intersect G by A8, SETFAM_1:def_9; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Intersect G or a in R .:^ (union F) )
assume A12: a in Intersect G ; ::_thesis: a in R .:^ (union F)
then A13: a in meet G by A8, SETFAM_1:def_9;
reconsider a = a as Element of B by A12;
for X being set st X in union F holds
a in Im (R,X)
proof
let X be set ; ::_thesis: ( X in union F implies a in Im (R,X) )
assume X in union F ; ::_thesis: a in Im (R,X)
then consider Z being set such that
A14: X in Z and
A15: Z in F by TARSKI:def_4;
reconsider Z = Z as Subset of A by A15;
set C = R .:^ Z;
R .:^ Z in G by A1, A15;
then a in R .:^ Z by A13, SETFAM_1:def_1;
hence a in Im (R,X) by A14, Th24; ::_thesis: verum
end;
hence a in R .:^ (union F) by Th25; ::_thesis: verum
end;
end;
end;
theorem Th31: :: RELSET_2:31
for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] st X1 c= X2 holds
R .:^ X2 c= R .:^ X1
proof
let A, B be set ; ::_thesis: for X1, X2 being Subset of A
for R being Subset of [:A,B:] st X1 c= X2 holds
R .:^ X2 c= R .:^ X1
let X1, X2 be Subset of A; ::_thesis: for R being Subset of [:A,B:] st X1 c= X2 holds
R .:^ X2 c= R .:^ X1
let R be Subset of [:A,B:]; ::_thesis: ( X1 c= X2 implies R .:^ X2 c= R .:^ X1 )
assume X1 c= X2 ; ::_thesis: R .:^ X2 c= R .:^ X1
then A1: {_{X1}_} c= {_{X2}_} by Th6;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .:^ X2 or y in R .:^ X1 )
assume A2: y in R .:^ X2 ; ::_thesis: y in R .:^ X1
percases ( (.: R) .: {_{X2}_} = {} or (.: R) .: {_{X2}_} <> {} ) ;
supposeA3: (.: R) .: {_{X2}_} = {} ; ::_thesis: y in R .:^ X1
percases ( (.: R) .: {_{X1}_} = {} or (.: R) .: {_{X1}_} <> {} ) ;
suppose (.: R) .: {_{X1}_} = {} ; ::_thesis: y in R .:^ X1
then Intersect ((.: R) .: {_{X1}_}) = B by SETFAM_1:def_9;
hence y in R .:^ X1 by A2; ::_thesis: verum
end;
supposeA4: (.: R) .: {_{X1}_} <> {} ; ::_thesis: y in R .:^ X1
for Y being set st Y in (.: R) .: {_{X1}_} holds
y in Y
proof
let Y be set ; ::_thesis: ( Y in (.: R) .: {_{X1}_} implies y in Y )
assume Y in (.: R) .: {_{X1}_} ; ::_thesis: y in Y
then ex x being set st
( [x,Y] in .: R & x in {_{X1}_} ) by RELAT_1:def_13;
hence y in Y by A1, A3, RELAT_1:def_13; ::_thesis: verum
end;
then y in meet ((.: R) .: {_{X1}_}) by A4, SETFAM_1:def_1;
hence y in R .:^ X1 by A4, SETFAM_1:def_9; ::_thesis: verum
end;
end;
end;
suppose (.: R) .: {_{X2}_} <> {} ; ::_thesis: y in R .:^ X1
then A5: y in meet ((.: R) .: {_{X2}_}) by A2, SETFAM_1:def_9;
percases ( (.: R) .: {_{X1}_} = {} or (.: R) .: {_{X1}_} <> {} ) ;
suppose (.: R) .: {_{X1}_} = {} ; ::_thesis: y in R .:^ X1
then Intersect ((.: R) .: {_{X1}_}) = B by SETFAM_1:def_9;
hence y in R .:^ X1 by A2; ::_thesis: verum
end;
supposeA6: (.: R) .: {_{X1}_} <> {} ; ::_thesis: y in R .:^ X1
(.: R) .: {_{X1}_} c= (.: R) .: {_{X2}_} by A1, RELAT_1:123;
then meet ((.: R) .: {_{X2}_}) c= meet ((.: R) .: {_{X1}_}) by A6, SETFAM_1:6;
then y in meet ((.: R) .: {_{X1}_}) by A5;
hence y in R .:^ X1 by A6, SETFAM_1:def_9; ::_thesis: verum
end;
end;
end;
end;
end;
theorem :: RELSET_2:32
for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] holds (R .:^ X1) \/ (R .:^ X2) c= R .:^ (X1 /\ X2)
proof
let A, B be set ; ::_thesis: for X1, X2 being Subset of A
for R being Subset of [:A,B:] holds (R .:^ X1) \/ (R .:^ X2) c= R .:^ (X1 /\ X2)
let X1, X2 be Subset of A; ::_thesis: for R being Subset of [:A,B:] holds (R .:^ X1) \/ (R .:^ X2) c= R .:^ (X1 /\ X2)
let R be Subset of [:A,B:]; ::_thesis: (R .:^ X1) \/ (R .:^ X2) c= R .:^ (X1 /\ X2)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (R .:^ X1) \/ (R .:^ X2) or y in R .:^ (X1 /\ X2) )
assume A1: y in (R .:^ X1) \/ (R .:^ X2) ; ::_thesis: y in R .:^ (X1 /\ X2)
A2: {_{(X1 /\ X2)}_} = {_{X1}_} /\ {_{X2}_} by Th4;
then A3: (.: R) .: {_{(X1 /\ X2)}_} c= ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) by RELAT_1:121;
percases ( y in R .:^ X1 or y in R .:^ X2 ) by A1, XBOOLE_0:def_3;
supposeA4: y in R .:^ X1 ; ::_thesis: y in R .:^ (X1 /\ X2)
y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
proof
percases ( (.: R) .: {_{(X1 /\ X2)}_} <> {} or (.: R) .: {_{(X1 /\ X2)}_} = {} ) ;
supposeA5: (.: R) .: {_{(X1 /\ X2)}_} <> {} ; ::_thesis: y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
A6: {_{(X1 /\ X2)}_} = {_{X1}_} /\ {_{X2}_} by Th4;
then A7: (.: R) .: {_{(X1 /\ X2)}_} c= ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) by RELAT_1:121;
A8: ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) <> {} by A5, A6, RELAT_1:121, XBOOLE_1:3;
(.: R) .: {_{X1}_} <> {} by A5, A7;
then A9: y in meet ((.: R) .: {_{X1}_}) by A4, SETFAM_1:def_9;
for Y being set st Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) holds
y in Y
proof
let Y be set ; ::_thesis: ( Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) implies y in Y )
assume Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) ; ::_thesis: y in Y
then Y in (.: R) .: {_{X1}_} by XBOOLE_0:def_4;
hence y in Y by A9, SETFAM_1:def_1; ::_thesis: verum
end;
then y in meet (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) by A8, SETFAM_1:def_1;
then A10: y in Intersect (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) by A8, SETFAM_1:def_9;
Intersect (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) c= Intersect ((.: R) .: ({_{X1}_} /\ {_{X2}_})) by RELAT_1:121, SETFAM_1:44;
hence y in Intersect ((.: R) .: {_{(X1 /\ X2)}_}) by A2, A10; ::_thesis: verum
end;
suppose (.: R) .: {_{(X1 /\ X2)}_} = {} ; ::_thesis: y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
then Intersect ((.: R) .: {_{(X1 /\ X2)}_}) = B by SETFAM_1:def_9;
hence y in Intersect ((.: R) .: {_{(X1 /\ X2)}_}) by A4; ::_thesis: verum
end;
end;
end;
hence y in R .:^ (X1 /\ X2) ; ::_thesis: verum
end;
supposeA11: y in R .:^ X2 ; ::_thesis: y in R .:^ (X1 /\ X2)
y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
proof
percases ( (.: R) .: {_{(X1 /\ X2)}_} <> {} or (.: R) .: {_{(X1 /\ X2)}_} = {} ) ;
supposeA12: (.: R) .: {_{(X1 /\ X2)}_} <> {} ; ::_thesis: y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
then A13: ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) <> {} by A2, RELAT_1:121, XBOOLE_1:3;
(.: R) .: {_{X2}_} <> {} by A3, A12;
then A14: y in meet ((.: R) .: {_{X2}_}) by A11, SETFAM_1:def_9;
for Y being set st Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) holds
y in Y
proof
let Y be set ; ::_thesis: ( Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) implies y in Y )
assume Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) ; ::_thesis: y in Y
then Y in (.: R) .: {_{X2}_} by XBOOLE_0:def_4;
hence y in Y by A14, SETFAM_1:def_1; ::_thesis: verum
end;
then y in meet (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) by A13, SETFAM_1:def_1;
then A15: y in Intersect (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) by A13, SETFAM_1:def_9;
A16: {_{(X1 /\ X2)}_} = {_{X1}_} /\ {_{X2}_} by Th4;
Intersect (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) c= Intersect ((.: R) .: ({_{X1}_} /\ {_{X2}_})) by RELAT_1:121, SETFAM_1:44;
hence y in Intersect ((.: R) .: {_{(X1 /\ X2)}_}) by A15, A16; ::_thesis: verum
end;
suppose (.: R) .: {_{(X1 /\ X2)}_} = {} ; ::_thesis: y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
then Intersect ((.: R) .: {_{(X1 /\ X2)}_}) = B by SETFAM_1:def_9;
hence y in Intersect ((.: R) .: {_{(X1 /\ X2)}_}) by A11; ::_thesis: verum
end;
end;
end;
hence y in R .:^ (X1 /\ X2) ; ::_thesis: verum
end;
end;
end;
theorem :: RELSET_2:33
for A, B being set
for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)
let X be Subset of A; ::_thesis: for R1, R2 being Subset of [:A,B:] holds (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)
let R1, R2 be Subset of [:A,B:]; ::_thesis: (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)
thus (R1 /\ R2) .:^ X c= (R1 .:^ X) /\ (R2 .:^ X) :: according to XBOOLE_0:def_10 ::_thesis: (R1 .:^ X) /\ (R2 .:^ X) c= (R1 /\ R2) .:^ X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (R1 /\ R2) .:^ X or y in (R1 .:^ X) /\ (R2 .:^ X) )
assume A1: y in (R1 /\ R2) .:^ X ; ::_thesis: y in (R1 .:^ X) /\ (R2 .:^ X)
then reconsider B = B as non empty set ;
reconsider y = y as Element of B by A1;
for x being set st x in X holds
y in Im (R1,x)
proof
let x be set ; ::_thesis: ( x in X implies y in Im (R1,x) )
assume x in X ; ::_thesis: y in Im (R1,x)
then y in Im ((R1 /\ R2),x) by A1, Th24;
then y in (Im (R1,x)) /\ (Im (R2,x)) by Th11;
hence y in Im (R1,x) by XBOOLE_0:def_4; ::_thesis: verum
end;
then A2: y in R1 .:^ X by Th25;
for x being set st x in X holds
y in Im (R2,x)
proof
let x be set ; ::_thesis: ( x in X implies y in Im (R2,x) )
assume x in X ; ::_thesis: y in Im (R2,x)
then y in Im ((R1 /\ R2),x) by A1, Th24;
then y in (Im (R1,x)) /\ (Im (R2,x)) by Th11;
hence y in Im (R2,x) by XBOOLE_0:def_4; ::_thesis: verum
end;
then y in R2 .:^ X by Th25;
hence y in (R1 .:^ X) /\ (R2 .:^ X) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (R1 .:^ X) /\ (R2 .:^ X) or y in (R1 /\ R2) .:^ X )
assume A3: y in (R1 .:^ X) /\ (R2 .:^ X) ; ::_thesis: y in (R1 /\ R2) .:^ X
then A4: y in R1 .:^ X by XBOOLE_0:def_4;
A5: y in R2 .:^ X by A3, XBOOLE_0:def_4;
reconsider B = B as non empty set by A3;
reconsider y = y as Element of B by A3;
for x being set st x in X holds
y in Im ((R1 /\ R2),x)
proof
let x be set ; ::_thesis: ( x in X implies y in Im ((R1 /\ R2),x) )
assume A6: x in X ; ::_thesis: y in Im ((R1 /\ R2),x)
then A7: y in Im (R1,x) by A4, Th25;
y in Im (R2,x) by A5, A6, Th25;
then y in (Im (R1,x)) /\ (Im (R2,x)) by A7, XBOOLE_0:def_4;
hence y in Im ((R1 /\ R2),x) by Th11; ::_thesis: verum
end;
hence y in (R1 /\ R2) .:^ X by Th25; ::_thesis: verum
end;
theorem :: RELSET_2:34
for A, B being set
for X being Subset of A
for FR being Subset-Family of [:A,B:] holds (union FR) .: X = union { (R .: X) where R is Subset of [:A,B:] : R in FR }
proof
let A, B be set ; ::_thesis: for X being Subset of A
for FR being Subset-Family of [:A,B:] holds (union FR) .: X = union { (R .: X) where R is Subset of [:A,B:] : R in FR }
let X be Subset of A; ::_thesis: for FR being Subset-Family of [:A,B:] holds (union FR) .: X = union { (R .: X) where R is Subset of [:A,B:] : R in FR }
let FR be Subset-Family of [:A,B:]; ::_thesis: (union FR) .: X = union { (R .: X) where R is Subset of [:A,B:] : R in FR }
thus (union FR) .: X c= union { (R .: X) where R is Subset of [:A,B:] : R in FR } :: according to XBOOLE_0:def_10 ::_thesis: union { (R .: X) where R is Subset of [:A,B:] : R in FR } c= (union FR) .: X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union FR) .: X or a in union { (R .: X) where R is Subset of [:A,B:] : R in FR } )
assume a in (union FR) .: X ; ::_thesis: a in union { (R .: X) where R is Subset of [:A,B:] : R in FR }
then consider x being set such that
A1: [x,a] in union FR and
A2: x in X by RELAT_1:def_13;
consider S being set such that
A3: [x,a] in S and
A4: S in FR by A1, TARSKI:def_4;
reconsider S = S as Subset of [:A,B:] by A4;
ex P being set st
( a in P & P in { (T .: X) where T is Subset of [:A,B:] : T in FR } )
proof
set P = S .: X;
A5: a in S .: X by A2, A3, RELAT_1:def_13;
S .: X in { (T .: X) where T is Subset of [:A,B:] : T in FR } by A4;
hence ex P being set st
( a in P & P in { (T .: X) where T is Subset of [:A,B:] : T in FR } ) by A5; ::_thesis: verum
end;
hence a in union { (R .: X) where R is Subset of [:A,B:] : R in FR } by TARSKI:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { (R .: X) where R is Subset of [:A,B:] : R in FR } or a in (union FR) .: X )
assume a in union { (R .: X) where R is Subset of [:A,B:] : R in FR } ; ::_thesis: a in (union FR) .: X
then consider P being set such that
A6: a in P and
A7: P in { (R .: X) where R is Subset of [:A,B:] : R in FR } by TARSKI:def_4;
consider R being Subset of [:A,B:] such that
A8: P = R .: X and
A9: R in FR by A7;
consider x being set such that
A10: [x,a] in R and
A11: x in X by A6, A8, RELAT_1:def_13;
ex x being set st
( x in X & [x,a] in union FR )
proof
take x ; ::_thesis: ( x in X & [x,a] in union FR )
thus ( x in X & [x,a] in union FR ) by A9, A10, A11, TARSKI:def_4; ::_thesis: verum
end;
hence a in (union FR) .: X by RELAT_1:def_13; ::_thesis: verum
end;
theorem :: RELSET_2:35
for A, B being set
for FR being Subset-Family of [:A,B:]
for A, B being set
for X being Subset of A holds { (R .:^ X) where R is Subset of [:A,B:] : R in FR } is Subset-Family of B
proof
let A, B be set ; ::_thesis: for FR being Subset-Family of [:A,B:]
for A, B being set
for X being Subset of A holds { (R .:^ X) where R is Subset of [:A,B:] : R in FR } is Subset-Family of B
let FR be Subset-Family of [:A,B:]; ::_thesis: for A, B being set
for X being Subset of A holds { (R .:^ X) where R is Subset of [:A,B:] : R in FR } is Subset-Family of B
let A, B be set ; ::_thesis: for X being Subset of A holds { (R .:^ X) where R is Subset of [:A,B:] : R in FR } is Subset-Family of B
let X be Subset of A; ::_thesis: { (R .:^ X) where R is Subset of [:A,B:] : R in FR } is Subset-Family of B
deffunc H1( Subset of [:A,B:]) -> Subset of B = $1 .:^ X;
defpred S1[ set ] means $1 in FR;
set G = { H1(R) where R is Subset of [:A,B:] : S1[R] } ;
thus { H1(R) where R is Subset of [:A,B:] : S1[R] } is Subset-Family of B from DOMAIN_1:sch_8(); ::_thesis: verum
end;
theorem Th36: :: RELSET_2:36
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st R = {} & X <> {} holds
R .:^ X = {}
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R being Subset of [:A,B:] st R = {} & X <> {} holds
R .:^ X = {}
let X be Subset of A; ::_thesis: for R being Subset of [:A,B:] st R = {} & X <> {} holds
R .:^ X = {}
let R be Subset of [:A,B:]; ::_thesis: ( R = {} & X <> {} implies R .:^ X = {} )
assume that
A1: R = {} and
A2: X <> {} ; ::_thesis: R .:^ X = {}
R .:^ X c= {}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in R .:^ X or a in {} )
assume A3: a in R .:^ X ; ::_thesis: a in {}
consider x being set such that
A4: x in X by A2, XBOOLE_0:def_1;
a in Im (R,x) by A3, A4, Th24;
hence a in {} by A1; ::_thesis: verum
end;
hence R .:^ X = {} ; ::_thesis: verum
end;
theorem Th37: :: RELSET_2:37
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st R = [:A,B:] holds
R .:^ X = B
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R being Subset of [:A,B:] st R = [:A,B:] holds
R .:^ X = B
let X be Subset of A; ::_thesis: for R being Subset of [:A,B:] st R = [:A,B:] holds
R .:^ X = B
let R be Subset of [:A,B:]; ::_thesis: ( R = [:A,B:] implies R .:^ X = B )
assume A1: R = [:A,B:] ; ::_thesis: R .:^ X = B
thus R .:^ X c= B ; :: according to XBOOLE_0:def_10 ::_thesis: B c= R .:^ X
thus B c= R .:^ X ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in R .:^ X )
assume A2: a in B ; ::_thesis: a in R .:^ X
then reconsider B = B as non empty set ;
reconsider a = a as Element of B by A2;
for x being set st x in X holds
a in Im (R,x)
proof
let x be set ; ::_thesis: ( x in X implies a in Im (R,x) )
assume x in X ; ::_thesis: a in Im (R,x)
then [x,a] in R by A1, ZFMISC_1:87;
hence a in Im (R,x) by Th9; ::_thesis: verum
end;
hence a in R .:^ X by Th25; ::_thesis: verum
end;
end;
theorem :: RELSET_2:38
for B, A being set
for X being Subset of A
for FR being Subset-Family of [:A,B:]
for G being Subset-Family of B st G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } holds
(Intersect FR) .:^ X = Intersect G
proof
let B, A be set ; ::_thesis: for X being Subset of A
for FR being Subset-Family of [:A,B:]
for G being Subset-Family of B st G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } holds
(Intersect FR) .:^ X = Intersect G
let X be Subset of A; ::_thesis: for FR being Subset-Family of [:A,B:]
for G being Subset-Family of B st G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } holds
(Intersect FR) .:^ X = Intersect G
let FR be Subset-Family of [:A,B:]; ::_thesis: for G being Subset-Family of B st G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } holds
(Intersect FR) .:^ X = Intersect G
let G be Subset-Family of B; ::_thesis: ( G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } implies (Intersect FR) .:^ X = Intersect G )
assume A1: G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } ; ::_thesis: (Intersect FR) .:^ X = Intersect G
A2: for x being set st G = {x} holds
Intersect G = x
proof
let x be set ; ::_thesis: ( G = {x} implies Intersect G = x )
assume G = {x} ; ::_thesis: Intersect G = x
then Intersect G = meet {x} by SETFAM_1:def_9;
hence Intersect G = x by SETFAM_1:10; ::_thesis: verum
end;
percases ( X = {} or X <> {} ) ;
supposeA3: X = {} ; ::_thesis: (Intersect FR) .:^ X = Intersect G
then A4: (Intersect FR) .:^ X = B by Th29;
G c= {B}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in G or a in {B} )
assume a in G ; ::_thesis: a in {B}
then ex R being Subset of [:A,B:] st
( a = R .:^ X & R in FR ) by A1;
then a = B by A3, Th29;
hence a in {B} by TARSKI:def_1; ::_thesis: verum
end;
then ( G = {} or G = {B} ) by ZFMISC_1:33;
hence (Intersect FR) .:^ X = Intersect G by A2, A4, SETFAM_1:def_9; ::_thesis: verum
end;
supposeA5: X <> {} ; ::_thesis: (Intersect FR) .:^ X = Intersect G
percases ( FR = {} or FR <> {} ) ;
supposeA6: FR = {} ; ::_thesis: (Intersect FR) .:^ X = Intersect G
then Intersect FR = [:A,B:] by SETFAM_1:def_9;
then A7: (Intersect FR) .:^ X = B by Th37;
G c= {B}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in G or a in {B} )
assume a in G ; ::_thesis: a in {B}
then ex R being Subset of [:A,B:] st
( a = R .:^ X & R in FR ) by A1;
hence a in {B} by A6; ::_thesis: verum
end;
then ( G = {} or G = {B} ) by ZFMISC_1:33;
hence (Intersect FR) .:^ X = Intersect G by A2, A7, SETFAM_1:def_9; ::_thesis: verum
end;
supposeA8: FR <> {} ; ::_thesis: (Intersect FR) .:^ X = Intersect G
percases ( B = {} or B <> {} ) ;
supposeA9: B = {} ; ::_thesis: (Intersect FR) .:^ X = Intersect G
then [:A,B:] = {} by ZFMISC_1:90;
then ( FR = {} or FR = {{}} ) by ZFMISC_1:1, ZFMISC_1:33;
then Intersect FR = meet {{}} by A8, SETFAM_1:def_9;
then (Intersect FR) .:^ X = {} by A5, Th36, SETFAM_1:10;
hence (Intersect FR) .:^ X = Intersect G by A9; ::_thesis: verum
end;
suppose B <> {} ; ::_thesis: (Intersect FR) .:^ X = Intersect G
then reconsider B = B as non empty set ;
thus (Intersect FR) .:^ X c= Intersect G :: according to XBOOLE_0:def_10 ::_thesis: Intersect G c= (Intersect FR) .:^ X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (Intersect FR) .:^ X or a in Intersect G )
assume A10: a in (Intersect FR) .:^ X ; ::_thesis: a in Intersect G
then A11: a in B ;
reconsider a = a as Element of B by A10;
( G <> {} implies a in Intersect G )
proof
assume A12: G <> {} ; ::_thesis: a in Intersect G
then A13: Intersect G = meet G by SETFAM_1:def_9;
for Y being set st Y in G holds
a in Y
proof
let Y be set ; ::_thesis: ( Y in G implies a in Y )
assume Y in G ; ::_thesis: a in Y
then consider R being Subset of [:A,B:] such that
A14: Y = R .:^ X and
A15: R in FR by A1;
for x being set st x in X holds
a in Im (R,x)
proof
let x be set ; ::_thesis: ( x in X implies a in Im (R,x) )
assume x in X ; ::_thesis: a in Im (R,x)
then a in Im ((Intersect FR),x) by A10, Th24;
then [x,a] in Intersect FR by Th9;
then [x,a] in meet FR by A8, SETFAM_1:def_9;
then [x,a] in R by A15, SETFAM_1:def_1;
hence a in Im (R,x) by Th9; ::_thesis: verum
end;
hence a in Y by A14, Th25; ::_thesis: verum
end;
hence a in Intersect G by A12, A13, SETFAM_1:def_1; ::_thesis: verum
end;
hence a in Intersect G by A11, SETFAM_1:def_9; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Intersect G or a in (Intersect FR) .:^ X )
assume A16: a in Intersect G ; ::_thesis: a in (Intersect FR) .:^ X
then reconsider a = a as Element of B ;
consider R being Subset of [:A,B:] such that
A17: R in FR by A8, SUBSET_1:4;
R .:^ X in G by A1, A17;
then A18: a in meet G by A16, SETFAM_1:def_9;
for x being set st x in X holds
a in Im ((Intersect FR),x)
proof
let x be set ; ::_thesis: ( x in X implies a in Im ((Intersect FR),x) )
assume A19: x in X ; ::_thesis: a in Im ((Intersect FR),x)
for Y being set st Y in FR holds
[x,a] in Y
proof
let P be set ; ::_thesis: ( P in FR implies [x,a] in P )
assume A20: P in FR ; ::_thesis: [x,a] in P
then reconsider P = P as Subset of [:A,B:] ;
set S = P .:^ X;
P .:^ X in G by A1, A20;
then a in P .:^ X by A18, SETFAM_1:def_1;
then a in Im (P,x) by A19, Th24;
hence [x,a] in P by Th9; ::_thesis: verum
end;
then [x,a] in meet FR by A8, SETFAM_1:def_1;
then [x,a] in Intersect FR by A8, SETFAM_1:def_9;
hence a in Im ((Intersect FR),x) by Th9; ::_thesis: verum
end;
hence a in (Intersect FR) .:^ X by Th25; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem :: RELSET_2:39
for A, B being set
for X being Subset of A
for R1, R2 being Subset of [:A,B:] st R1 c= R2 holds
R1 .:^ X c= R2 .:^ X
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R1, R2 being Subset of [:A,B:] st R1 c= R2 holds
R1 .:^ X c= R2 .:^ X
let X be Subset of A; ::_thesis: for R1, R2 being Subset of [:A,B:] st R1 c= R2 holds
R1 .:^ X c= R2 .:^ X
let R1, R2 be Subset of [:A,B:]; ::_thesis: ( R1 c= R2 implies R1 .:^ X c= R2 .:^ X )
assume A1: R1 c= R2 ; ::_thesis: R1 .:^ X c= R2 .:^ X
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R1 .:^ X or y in R2 .:^ X )
assume A2: y in R1 .:^ X ; ::_thesis: y in R2 .:^ X
then reconsider B = B as non empty set ;
reconsider y = y as Element of B by A2;
for x being set st x in X holds
y in Im (R2,x)
proof
let x be set ; ::_thesis: ( x in X implies y in Im (R2,x) )
assume x in X ; ::_thesis: y in Im (R2,x)
then y in Im (R1,x) by A2, Th25;
then [x,y] in R1 by Th9;
hence y in Im (R2,x) by A1, Th9; ::_thesis: verum
end;
hence y in R2 .:^ X by Th25; ::_thesis: verum
end;
theorem :: RELSET_2:40
for A, B being set
for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 .:^ X) \/ (R2 .:^ X) c= (R1 \/ R2) .:^ X
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 .:^ X) \/ (R2 .:^ X) c= (R1 \/ R2) .:^ X
let X be Subset of A; ::_thesis: for R1, R2 being Subset of [:A,B:] holds (R1 .:^ X) \/ (R2 .:^ X) c= (R1 \/ R2) .:^ X
let R1, R2 be Subset of [:A,B:]; ::_thesis: (R1 .:^ X) \/ (R2 .:^ X) c= (R1 \/ R2) .:^ X
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (R1 .:^ X) \/ (R2 .:^ X) or y in (R1 \/ R2) .:^ X )
assume A1: y in (R1 .:^ X) \/ (R2 .:^ X) ; ::_thesis: y in (R1 \/ R2) .:^ X
percases ( y in R1 .:^ X or y in R2 .:^ X ) by A1, XBOOLE_0:def_3;
supposeA2: y in R1 .:^ X ; ::_thesis: y in (R1 \/ R2) .:^ X
then reconsider B = B as non empty set ;
reconsider y = y as Element of B by A2;
for x being set st x in X holds
y in Im ((R1 \/ R2),x)
proof
let x be set ; ::_thesis: ( x in X implies y in Im ((R1 \/ R2),x) )
assume x in X ; ::_thesis: y in Im ((R1 \/ R2),x)
then y in Im (R1,x) by A2, Th25;
then y in (Im (R1,x)) \/ (Im (R2,x)) by XBOOLE_0:def_3;
hence y in Im ((R1 \/ R2),x) by Th10; ::_thesis: verum
end;
hence y in (R1 \/ R2) .:^ X by Th25; ::_thesis: verum
end;
supposeA3: y in R2 .:^ X ; ::_thesis: y in (R1 \/ R2) .:^ X
then reconsider B = B as non empty set ;
reconsider y = y as Element of B by A3;
for x being set st x in X holds
y in Im ((R1 \/ R2),x)
proof
let x be set ; ::_thesis: ( x in X implies y in Im ((R1 \/ R2),x) )
assume x in X ; ::_thesis: y in Im ((R1 \/ R2),x)
then y in Im (R2,x) by A3, Th25;
then y in (Im (R1,x)) \/ (Im (R2,x)) by XBOOLE_0:def_3;
hence y in Im ((R1 \/ R2),x) by Th10; ::_thesis: verum
end;
hence y in (R1 \/ R2) .:^ X by Th25; ::_thesis: verum
end;
end;
end;
theorem Th41: :: RELSET_2:41
for y, x, A, B being set
for R being Subset of [:A,B:] holds
( y in Im ((R `),x) iff ( not [x,y] in R & x in A & y in B ) )
proof
let y, x, A, B be set ; ::_thesis: for R being Subset of [:A,B:] holds
( y in Im ((R `),x) iff ( not [x,y] in R & x in A & y in B ) )
let R be Subset of [:A,B:]; ::_thesis: ( y in Im ((R `),x) iff ( not [x,y] in R & x in A & y in B ) )
thus ( y in Im ((R `),x) implies ( not [x,y] in R & x in A & y in B ) ) ::_thesis: ( not [x,y] in R & x in A & y in B implies y in Im ((R `),x) )
proof
assume y in Im ((R `),x) ; ::_thesis: ( not [x,y] in R & x in A & y in B )
then ex a being set st
( [a,y] in R ` & a in {x} ) by RELAT_1:def_13;
then [x,y] in [:A,B:] \ R by TARSKI:def_1;
hence ( not [x,y] in R & x in A & y in B ) by XBOOLE_0:def_5, ZFMISC_1:87; ::_thesis: verum
end;
assume that
A1: not [x,y] in R and
A2: x in A and
A3: y in B ; ::_thesis: y in Im ((R `),x)
A4: x in {x} by TARSKI:def_1;
[x,y] in [:A,B:] by A2, A3, ZFMISC_1:87;
then [x,y] in [:A,B:] \ R by A1, XBOOLE_0:def_5;
hence y in Im ((R `),x) by A4, RELAT_1:def_13; ::_thesis: verum
end;
theorem :: RELSET_2:42
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st X <> {} holds
R .:^ X c= R .: X
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R being Subset of [:A,B:] st X <> {} holds
R .:^ X c= R .: X
let X be Subset of A; ::_thesis: for R being Subset of [:A,B:] st X <> {} holds
R .:^ X c= R .: X
let R be Subset of [:A,B:]; ::_thesis: ( X <> {} implies R .:^ X c= R .: X )
assume A1: X <> {} ; ::_thesis: R .:^ X c= R .: X
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .:^ X or y in R .: X )
assume A2: y in R .:^ X ; ::_thesis: y in R .: X
consider x being set such that
A3: x in X by A1, XBOOLE_0:def_1;
y in Im (R,x) by A2, A3, Th24;
then [x,y] in R by Th9;
hence y in R .: X by A3, RELAT_1:def_13; ::_thesis: verum
end;
theorem Th43: :: RELSET_2:43
for A, B being set
for R being Subset of [:A,B:]
for X, Y being set holds
( X meets (R ~) .: Y iff ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) )
proof
let A, B be set ; ::_thesis: for R being Subset of [:A,B:]
for X, Y being set holds
( X meets (R ~) .: Y iff ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) )
let R be Subset of [:A,B:]; ::_thesis: for X, Y being set holds
( X meets (R ~) .: Y iff ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) )
let X, Y be set ; ::_thesis: ( X meets (R ~) .: Y iff ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) )
hereby ::_thesis: ( ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) implies X meets (R ~) .: Y )
assume X meets (R ~) .: Y ; ::_thesis: ex a, b being set st
( a in X & b in Y & a in Im ((R ~),b) )
then consider a being set such that
A1: a in X and
A2: a in (R ~) .: Y by XBOOLE_0:3;
consider b being set such that
A3: [b,a] in R ~ and
A4: b in Y by A2, RELAT_1:def_13;
A5: b in {b} by TARSKI:def_1;
take a = a; ::_thesis: ex b being set st
( a in X & b in Y & a in Im ((R ~),b) )
take b = b; ::_thesis: ( a in X & b in Y & a in Im ((R ~),b) )
thus a in X by A1; ::_thesis: ( b in Y & a in Im ((R ~),b) )
thus b in Y by A4; ::_thesis: a in Im ((R ~),b)
thus a in Im ((R ~),b) by A3, A5, RELAT_1:def_13; ::_thesis: verum
end;
given x, y being set such that A6: x in X and
A7: y in Y and
A8: x in Im ((R ~),y) ; ::_thesis: X meets (R ~) .: Y
ex a being set st
( [a,x] in R ~ & a in {y} ) by A8, RELAT_1:def_13;
then [y,x] in R ~ by TARSKI:def_1;
then x in (R ~) .: Y by A7, RELAT_1:def_13;
hence X meets (R ~) .: Y by A6, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th44: :: RELSET_2:44
for A, B being set
for R being Subset of [:A,B:]
for X, Y being set holds
( ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) iff Y meets R .: X )
proof
let A, B be set ; ::_thesis: for R being Subset of [:A,B:]
for X, Y being set holds
( ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) iff Y meets R .: X )
let R be Subset of [:A,B:]; ::_thesis: for X, Y being set holds
( ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) iff Y meets R .: X )
let X, Y be set ; ::_thesis: ( ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) iff Y meets R .: X )
thus ( ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) implies Y meets R .: X ) ::_thesis: ( Y meets R .: X implies ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) )
proof
given x, y being set such that A1: x in X and
A2: y in Y and
A3: x in Im ((R ~),y) ; ::_thesis: Y meets R .: X
consider a being set such that
A4: [a,x] in R ~ and
A5: a in {y} by A3, RELAT_1:def_13;
a = y by A5, TARSKI:def_1;
then [x,y] in R by A4, RELAT_1:def_7;
then y in R .: X by A1, RELAT_1:def_13;
hence Y meets R .: X by A2, XBOOLE_0:3; ::_thesis: verum
end;
assume Y meets R .: X ; ::_thesis: ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) )
then consider a being set such that
A6: a in Y and
A7: a in R .: X by XBOOLE_0:3;
consider b being set such that
A8: [b,a] in R and
A9: b in X by A7, RELAT_1:def_13;
A10: [a,b] in R ~ by A8, RELAT_1:def_7;
A11: a in {a} by TARSKI:def_1;
take b ; ::_thesis: ex y being set st
( b in X & y in Y & b in Im ((R ~),y) )
take a ; ::_thesis: ( b in X & a in Y & b in Im ((R ~),a) )
thus b in X by A9; ::_thesis: ( a in Y & b in Im ((R ~),a) )
thus a in Y by A6; ::_thesis: b in Im ((R ~),a)
thus b in Im ((R ~),a) by A10, A11, RELAT_1:def_13; ::_thesis: verum
end;
theorem Th45: :: RELSET_2:45
for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Subset of [:A,B:] holds
( X misses (R ~) .: Y iff Y misses R .: X )
proof
let A, B be set ; ::_thesis: for X being Subset of A
for Y being Subset of B
for R being Subset of [:A,B:] holds
( X misses (R ~) .: Y iff Y misses R .: X )
let X be Subset of A; ::_thesis: for Y being Subset of B
for R being Subset of [:A,B:] holds
( X misses (R ~) .: Y iff Y misses R .: X )
let Y be Subset of B; ::_thesis: for R being Subset of [:A,B:] holds
( X misses (R ~) .: Y iff Y misses R .: X )
let R be Subset of [:A,B:]; ::_thesis: ( X misses (R ~) .: Y iff Y misses R .: X )
( X meets (R ~) .: Y iff ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) ) by Th43;
hence ( X misses (R ~) .: Y iff Y misses R .: X ) by Th44; ::_thesis: verum
end;
theorem Th46: :: RELSET_2:46
for A, B being set
for R being Subset of [:A,B:]
for X being set holds R .: X = R .: (X /\ (proj1 R))
proof
let A, B be set ; ::_thesis: for R being Subset of [:A,B:]
for X being set holds R .: X = R .: (X /\ (proj1 R))
let R be Subset of [:A,B:]; ::_thesis: for X being set holds R .: X = R .: (X /\ (proj1 R))
let X be set ; ::_thesis: R .: X = R .: (X /\ (proj1 R))
thus R .: X c= R .: (X /\ (proj1 R)) :: according to XBOOLE_0:def_10 ::_thesis: R .: (X /\ (proj1 R)) c= R .: X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .: X or y in R .: (X /\ (proj1 R)) )
assume y in R .: X ; ::_thesis: y in R .: (X /\ (proj1 R))
then consider x being set such that
A1: [x,y] in R and
A2: x in X by RELAT_1:def_13;
x in proj1 R by A1, XTUPLE_0:def_12;
then x in X /\ (proj1 R) by A2, XBOOLE_0:def_4;
hence y in R .: (X /\ (proj1 R)) by A1, RELAT_1:def_13; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .: (X /\ (proj1 R)) or y in R .: X )
assume y in R .: (X /\ (proj1 R)) ; ::_thesis: y in R .: X
then consider x being set such that
A3: [x,y] in R and
A4: x in X /\ (proj1 R) by RELAT_1:def_13;
x in X by A4, XBOOLE_0:def_4;
hence y in R .: X by A3, RELAT_1:def_13; ::_thesis: verum
end;
theorem Th47: :: RELSET_2:47
for A, B being set
for R being Subset of [:A,B:]
for Y being set holds (R ~) .: Y = (R ~) .: (Y /\ (proj2 R))
proof
let A, B be set ; ::_thesis: for R being Subset of [:A,B:]
for Y being set holds (R ~) .: Y = (R ~) .: (Y /\ (proj2 R))
let R be Subset of [:A,B:]; ::_thesis: for Y being set holds (R ~) .: Y = (R ~) .: (Y /\ (proj2 R))
let Y be set ; ::_thesis: (R ~) .: Y = (R ~) .: (Y /\ (proj2 R))
thus (R ~) .: Y c= (R ~) .: (Y /\ (proj2 R)) :: according to XBOOLE_0:def_10 ::_thesis: (R ~) .: (Y /\ (proj2 R)) c= (R ~) .: Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (R ~) .: Y or y in (R ~) .: (Y /\ (proj2 R)) )
assume y in (R ~) .: Y ; ::_thesis: y in (R ~) .: (Y /\ (proj2 R))
then consider x being set such that
A1: [x,y] in R ~ and
A2: x in Y by RELAT_1:def_13;
[y,x] in R by A1, RELAT_1:def_7;
then x in proj2 R by XTUPLE_0:def_13;
then x in Y /\ (proj2 R) by A2, XBOOLE_0:def_4;
hence y in (R ~) .: (Y /\ (proj2 R)) by A1, RELAT_1:def_13; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (R ~) .: (Y /\ (proj2 R)) or y in (R ~) .: Y )
assume y in (R ~) .: (Y /\ (proj2 R)) ; ::_thesis: y in (R ~) .: Y
then consider x being set such that
A3: [x,y] in R ~ and
A4: x in Y /\ (proj2 R) by RELAT_1:def_13;
x in Y by A4, XBOOLE_0:def_4;
hence y in (R ~) .: Y by A3, RELAT_1:def_13; ::_thesis: verum
end;
theorem Th48: :: RELSET_2:48
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds (R .:^ X) ` = (R `) .: X
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R being Subset of [:A,B:] holds (R .:^ X) ` = (R `) .: X
let X be Subset of A; ::_thesis: for R being Subset of [:A,B:] holds (R .:^ X) ` = (R `) .: X
let R be Subset of [:A,B:]; ::_thesis: (R .:^ X) ` = (R `) .: X
thus (R .:^ X) ` c= (R `) .: X :: according to XBOOLE_0:def_10 ::_thesis: (R `) .: X c= (R .:^ X) `
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (R .:^ X) ` or a in (R `) .: X )
assume A1: a in (R .:^ X) ` ; ::_thesis: a in (R `) .: X
then not a in R .:^ X by XBOOLE_0:def_5;
then consider x being set such that
A2: x in X and
A3: not a in Im (R,x) by A1, Th25;
A4: not [x,a] in R by A3, Th9;
[x,a] in [:A,B:] by A1, A2, ZFMISC_1:87;
then [x,a] in [:A,B:] \ R by A4, XBOOLE_0:def_5;
hence a in (R `) .: X by A2, RELAT_1:def_13; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (R `) .: X or a in (R .:^ X) ` )
assume a in (R `) .: X ; ::_thesis: a in (R .:^ X) `
then consider x being set such that
A5: [x,a] in R ` and
A6: x in X by RELAT_1:def_13;
A7: not [x,a] in R by A5, XBOOLE_0:def_5;
assume not a in (R .:^ X) ` ; ::_thesis: contradiction
then A8: ( not a in B or a in R .:^ X ) by XBOOLE_0:def_5;
( a in R .:^ X implies for x being set st x in X holds
[x,a] in R )
proof
assume A9: a in R .:^ X ; ::_thesis: for x being set st x in X holds
[x,a] in R
let x be set ; ::_thesis: ( x in X implies [x,a] in R )
assume x in X ; ::_thesis: [x,a] in R
then a in Im (R,x) by A9, Th24;
hence [x,a] in R by Th9; ::_thesis: verum
end;
hence contradiction by A5, A6, A7, A8, ZFMISC_1:87; ::_thesis: verum
end;
definition
let A, B, C be set ;
let R be Subset of [:A,B:];
let S be Subset of [:B,C:];
:: original: *
redefine funcR * S -> Relation of A,C;
coherence
R * S is Relation of A,C
proof
reconsider R = R as Relation of A,B ;
reconsider S = S as Relation of B,C ;
R * S is Relation of A,C ;
hence R * S is Relation of A,C ; ::_thesis: verum
end;
end;
theorem Th49: :: RELSET_2:49
for A, B being set
for X being Subset of A
for R being Relation of A,B holds (R .: X) ` = (R `) .:^ X
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R being Relation of A,B holds (R .: X) ` = (R `) .:^ X
let X be Subset of A; ::_thesis: for R being Relation of A,B holds (R .: X) ` = (R `) .:^ X
let R be Relation of A,B; ::_thesis: (R .: X) ` = (R `) .:^ X
thus (R .: X) ` c= (R `) .:^ X :: according to XBOOLE_0:def_10 ::_thesis: (R `) .:^ X c= (R .: X) `
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (R .: X) ` or a in (R `) .:^ X )
assume A1: a in (R .: X) ` ; ::_thesis: a in (R `) .:^ X
then reconsider B = B as non empty set ;
reconsider a = a as Element of B by A1;
assume not a in (R `) .:^ X ; ::_thesis: contradiction
then consider x being set such that
A2: x in X and
A3: not a in Im ((R `),x) by Th25;
[x,a] in R by A2, A3, Th41;
then a in R .: X by A2, RELAT_1:def_13;
hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (R `) .:^ X or a in (R .: X) ` )
assume A4: a in (R `) .:^ X ; ::_thesis: a in (R .: X) `
A5: ( a in (R `) .:^ X implies for x being set st x in X holds
not [x,a] in R )
proof
assume a in (R `) .:^ X ; ::_thesis: for x being set st x in X holds
not [x,a] in R
let x be set ; ::_thesis: ( x in X implies not [x,a] in R )
assume A6: x in X ; ::_thesis: not [x,a] in R
assume A7: [x,a] in R ; ::_thesis: contradiction
a in Im ((R `),x) by A4, A6, Th24;
then ex b being set st
( [b,a] in R ` & b in {x} ) by RELAT_1:def_13;
then A8: [x,a] in R ` by TARSKI:def_1;
R ` misses R by XBOOLE_1:79;
hence contradiction by A7, A8, XBOOLE_0:3; ::_thesis: verum
end;
assume A9: not a in (R .: X) ` ; ::_thesis: contradiction
percases ( not a in B or a in R .: X ) by A9, XBOOLE_0:def_5;
suppose not a in B ; ::_thesis: contradiction
hence contradiction by A4; ::_thesis: verum
end;
suppose a in R .: X ; ::_thesis: contradiction
then ex y being set st
( [y,a] in R & y in X ) by RELAT_1:def_13;
hence contradiction by A4, A5; ::_thesis: verum
end;
end;
end;
theorem Th50: :: RELSET_2:50
for B, A being set
for R being Relation of A,B holds
( proj1 R = (R ~) .: B & proj2 R = R .: A )
proof
let B, A be set ; ::_thesis: for R being Relation of A,B holds
( proj1 R = (R ~) .: B & proj2 R = R .: A )
let R be Relation of A,B; ::_thesis: ( proj1 R = (R ~) .: B & proj2 R = R .: A )
thus proj1 R = dom R
.= rng (R ~) by RELAT_1:20
.= (R ~) .: B by RELSET_1:22 ; ::_thesis: proj2 R = R .: A
thus proj2 R = rng R
.= R .: A by RELSET_1:22 ; ::_thesis: verum
end;
theorem :: RELSET_2:51
for A, B, C being set
for R being Relation of A,B
for S being Relation of B,C holds
( proj1 (R * S) = (R ~) .: (proj1 S) & proj1 (R * S) c= proj1 R )
proof
let A, B, C be set ; ::_thesis: for R being Relation of A,B
for S being Relation of B,C holds
( proj1 (R * S) = (R ~) .: (proj1 S) & proj1 (R * S) c= proj1 R )
let R be Relation of A,B; ::_thesis: for S being Relation of B,C holds
( proj1 (R * S) = (R ~) .: (proj1 S) & proj1 (R * S) c= proj1 R )
let S be Relation of B,C; ::_thesis: ( proj1 (R * S) = (R ~) .: (proj1 S) & proj1 (R * S) c= proj1 R )
thus A1: proj1 (R * S) = ((R * S) ~) .: C by Th50
.= ((S ~) * (R ~)) .: C by RELAT_1:35
.= (R ~) .: ((S ~) .: C) by RELAT_1:126
.= (R ~) .: (proj1 S) by Th50 ; ::_thesis: proj1 (R * S) c= proj1 R
proj1 S = dom S ;
then proj1 (R * S) c= (R ~) .: B by A1, RELAT_1:123;
hence proj1 (R * S) c= proj1 R by Th50; ::_thesis: verum
end;
theorem :: RELSET_2:52
for A, B, C being set
for R being Relation of A,B
for S being Relation of B,C holds
( proj2 (R * S) = S .: (proj2 R) & proj2 (R * S) c= proj2 S )
proof
let A, B, C be set ; ::_thesis: for R being Relation of A,B
for S being Relation of B,C holds
( proj2 (R * S) = S .: (proj2 R) & proj2 (R * S) c= proj2 S )
let R be Relation of A,B; ::_thesis: for S being Relation of B,C holds
( proj2 (R * S) = S .: (proj2 R) & proj2 (R * S) c= proj2 S )
let S be Relation of B,C; ::_thesis: ( proj2 (R * S) = S .: (proj2 R) & proj2 (R * S) c= proj2 S )
thus A1: proj2 (R * S) = (R * S) .: A by Th50
.= S .: (R .: A) by RELAT_1:126
.= S .: (proj2 R) by Th50 ; ::_thesis: proj2 (R * S) c= proj2 S
proj2 R = rng R ;
then S .: (proj2 R) c= S .: B by RELAT_1:123;
hence proj2 (R * S) c= proj2 S by A1, Th50; ::_thesis: verum
end;
theorem :: RELSET_2:53
for A, B being set
for X being Subset of A
for R being Relation of A,B holds
( X c= proj1 R iff X c= (R * (R ~)) .: X )
proof
let A, B be set ; ::_thesis: for X being Subset of A
for R being Relation of A,B holds
( X c= proj1 R iff X c= (R * (R ~)) .: X )
let X be Subset of A; ::_thesis: for R being Relation of A,B holds
( X c= proj1 R iff X c= (R * (R ~)) .: X )
let R be Relation of A,B; ::_thesis: ( X c= proj1 R iff X c= (R * (R ~)) .: X )
thus ( X c= proj1 R implies X c= (R * (R ~)) .: X ) ::_thesis: ( X c= (R * (R ~)) .: X implies X c= proj1 R )
proof
assume A1: X c= proj1 R ; ::_thesis: X c= (R * (R ~)) .: X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (R * (R ~)) .: X )
assume A2: x in X ; ::_thesis: x in (R * (R ~)) .: X
then reconsider x = x as Element of A ;
consider y being set such that
A3: [x,y] in R by A1, A2, XTUPLE_0:def_12;
A4: [y,x] in R ~ by A3, RELAT_1:def_7;
y in {y} by TARSKI:def_1;
then A5: x in (R ~) .: {y} by A4, RELAT_1:def_13;
(R ~) .: {y} c= (R * (R ~)) .: X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (R ~) .: {y} or a in (R * (R ~)) .: X )
assume a in (R ~) .: {y} ; ::_thesis: a in (R * (R ~)) .: X
then ex b being set st
( [b,a] in R ~ & b in {y} ) by RELAT_1:def_13;
then [y,a] in R ~ by TARSKI:def_1;
then [x,a] in R * (R ~) by A3, RELAT_1:def_8;
hence a in (R * (R ~)) .: X by A2, RELAT_1:def_13; ::_thesis: verum
end;
hence x in (R * (R ~)) .: X by A5; ::_thesis: verum
end;
assume A6: X c= (R * (R ~)) .: X ; ::_thesis: X c= proj1 R
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in proj1 R )
assume x in X ; ::_thesis: x in proj1 R
then A7: x in (R * (R ~)) .: X by A6;
A8: (R * (R ~)) .: X = (R ~) .: (R .: X) by RELAT_1:126;
(R ~) .: (R .: X) c= (R ~) .: B by RELAT_1:123;
then (R * (R ~)) .: X c= proj1 R by A8, Th50;
hence x in proj1 R by A7; ::_thesis: verum
end;
theorem :: RELSET_2:54
for A, B being set
for Y being Subset of B
for R being Relation of A,B holds
( Y c= proj2 R iff Y c= ((R ~) * R) .: Y )
proof
let A, B be set ; ::_thesis: for Y being Subset of B
for R being Relation of A,B holds
( Y c= proj2 R iff Y c= ((R ~) * R) .: Y )
let Y be Subset of B; ::_thesis: for R being Relation of A,B holds
( Y c= proj2 R iff Y c= ((R ~) * R) .: Y )
let R be Relation of A,B; ::_thesis: ( Y c= proj2 R iff Y c= ((R ~) * R) .: Y )
thus ( Y c= proj2 R implies Y c= ((R ~) * R) .: Y ) ::_thesis: ( Y c= ((R ~) * R) .: Y implies Y c= proj2 R )
proof
assume A1: Y c= proj2 R ; ::_thesis: Y c= ((R ~) * R) .: Y
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in ((R ~) * R) .: Y )
assume A2: y in Y ; ::_thesis: y in ((R ~) * R) .: Y
then consider x being set such that
A3: [x,y] in R by A1, XTUPLE_0:def_13;
A4: [y,x] in R ~ by A3, RELAT_1:def_7;
A5: y in Im (R,x) by A3, Th9;
R .: {x} c= ((R ~) * R) .: Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in R .: {x} or a in ((R ~) * R) .: Y )
assume a in R .: {x} ; ::_thesis: a in ((R ~) * R) .: Y
then ex b being set st
( [b,a] in R & b in {x} ) by RELAT_1:def_13;
then [x,a] in R by TARSKI:def_1;
then [y,a] in (R ~) * R by A4, RELAT_1:def_8;
hence a in ((R ~) * R) .: Y by A2, RELAT_1:def_13; ::_thesis: verum
end;
hence y in ((R ~) * R) .: Y by A5; ::_thesis: verum
end;
assume A6: Y c= ((R ~) * R) .: Y ; ::_thesis: Y c= proj2 R
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in proj2 R )
assume x in Y ; ::_thesis: x in proj2 R
then A7: x in ((R ~) * R) .: Y by A6;
A8: ((R ~) * R) .: Y = R .: ((R ~) .: Y) by RELAT_1:126;
R .: ((R ~) .: Y) c= R .: A by RELAT_1:123;
then ((R ~) * R) .: Y c= proj2 R by A8, Th50;
hence x in proj2 R by A7; ::_thesis: verum
end;
theorem :: RELSET_2:55
for B, A being set
for R being Relation of A,B holds
( proj1 R = (R ~) .: B & (R ~) .: (R .: A) = (R ~) .: (proj2 R) ) by Th50;
theorem :: RELSET_2:56
for B, A being set
for R being Relation of A,B holds (R ~) .: B = (R * (R ~)) .: A
proof
let B, A be set ; ::_thesis: for R being Relation of A,B holds (R ~) .: B = (R * (R ~)) .: A
let R be Relation of A,B; ::_thesis: (R ~) .: B = (R * (R ~)) .: A
A1: (R * (R ~)) .: A = (R ~) .: (R .: A) by RELAT_1:126
.= (R ~) .: (proj2 R) by Th50 ;
thus (R ~) .: B c= (R * (R ~)) .: A :: according to XBOOLE_0:def_10 ::_thesis: (R * (R ~)) .: A c= (R ~) .: B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R ~) .: B or x in (R * (R ~)) .: A )
assume A2: x in (R ~) .: B ; ::_thesis: x in (R * (R ~)) .: A
A3: (R ~) .: B = (R ~) .: (B /\ (proj2 R)) by Th47;
(R ~) .: (B /\ (proj2 R)) c= ((R ~) .: B) /\ ((R ~) .: (proj2 R)) by RELAT_1:121;
hence x in (R * (R ~)) .: A by A1, A2, A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R * (R ~)) .: A or x in (R ~) .: B )
assume A4: x in (R * (R ~)) .: A ; ::_thesis: x in (R ~) .: B
proj2 R c= rng R ;
then (R ~) .: (proj2 R) c= (R ~) .: B by RELAT_1:123;
hence x in (R ~) .: B by A1, A4; ::_thesis: verum
end;
theorem :: RELSET_2:57
for A, B being set
for R being Relation of A,B holds R .: A = ((R ~) * R) .: B
proof
let A, B be set ; ::_thesis: for R being Relation of A,B holds R .: A = ((R ~) * R) .: B
let R be Relation of A,B; ::_thesis: R .: A = ((R ~) * R) .: B
A1: ((R ~) * R) .: B = R .: ((R ~) .: B) by RELAT_1:126
.= R .: (proj1 R) by Th50 ;
thus R .: A c= ((R ~) * R) .: B :: according to XBOOLE_0:def_10 ::_thesis: ((R ~) * R) .: B c= R .: A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R .: A or x in ((R ~) * R) .: B )
assume A2: x in R .: A ; ::_thesis: x in ((R ~) * R) .: B
A3: R .: A = R .: (A /\ (proj1 R)) by Th46;
R .: (A /\ (proj1 R)) c= (R .: A) /\ (R .: (proj1 R)) by RELAT_1:121;
hence x in ((R ~) * R) .: B by A1, A2, A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((R ~) * R) .: B or x in R .: A )
assume A4: x in ((R ~) * R) .: B ; ::_thesis: x in R .: A
proj1 R c= dom R ;
then R .: (proj1 R) c= R .: A by RELAT_1:123;
hence x in R .: A by A1, A4; ::_thesis: verum
end;
theorem :: RELSET_2:58
for A, B, C being set
for X being Subset of A
for R being Relation of A,B
for S being Relation of B,C holds S .:^ (R .: X) = ((R * (S `)) `) .:^ X
proof
let A, B, C be set ; ::_thesis: for X being Subset of A
for R being Relation of A,B
for S being Relation of B,C holds S .:^ (R .: X) = ((R * (S `)) `) .:^ X
let X be Subset of A; ::_thesis: for R being Relation of A,B
for S being Relation of B,C holds S .:^ (R .: X) = ((R * (S `)) `) .:^ X
let R be Relation of A,B; ::_thesis: for S being Relation of B,C holds S .:^ (R .: X) = ((R * (S `)) `) .:^ X
let S be Relation of B,C; ::_thesis: S .:^ (R .: X) = ((R * (S `)) `) .:^ X
(S .:^ (R .: X)) ` = (S `) .: (R .: X) by Th48
.= (R * (S `)) .: X by RELAT_1:126 ;
then S .:^ (R .: X) = ((R * (S `)) .: X) `
.= ((R * (S `)) `) .:^ X by Th49 ;
hence S .:^ (R .: X) = ((R * (S `)) `) .:^ X ; ::_thesis: verum
end;
theorem Th59: :: RELSET_2:59
for A, B being set
for R being Relation of A,B holds (R `) ~ = (R ~) `
proof
let A, B be set ; ::_thesis: for R being Relation of A,B holds (R `) ~ = (R ~) `
let R be Relation of A,B; ::_thesis: (R `) ~ = (R ~) `
(R `) ~ = ([:A,B:] ~) \ (R ~) by RELAT_1:24
.= (R ~) ` by SYSREL:5 ;
hence (R `) ~ = (R ~) ` ; ::_thesis: verum
end;
theorem Th60: :: RELSET_2:60
for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( X c= (R ~) .:^ Y iff Y c= R .:^ X )
proof
let A, B be set ; ::_thesis: for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( X c= (R ~) .:^ Y iff Y c= R .:^ X )
let X be Subset of A; ::_thesis: for Y being Subset of B
for R being Relation of A,B holds
( X c= (R ~) .:^ Y iff Y c= R .:^ X )
let Y be Subset of B; ::_thesis: for R being Relation of A,B holds
( X c= (R ~) .:^ Y iff Y c= R .:^ X )
let R be Relation of A,B; ::_thesis: ( X c= (R ~) .:^ Y iff Y c= R .:^ X )
( X c= (R ~) .:^ Y iff X misses ((R ~) .:^ Y) ` ) by SUBSET_1:24;
then ( X c= (R ~) .:^ Y iff X misses ((R ~) `) .: Y ) by Th48;
then A1: ( X c= (R ~) .:^ Y iff X /\ (((R ~) `) .: Y) = {} ) by XBOOLE_0:def_7;
reconsider S = R ` as Relation of A,B ;
( X misses (S ~) .: Y iff Y misses S .: X ) by Th45;
then ( X /\ ((S ~) .: Y) = {} iff Y /\ (S .: X) = {} ) by XBOOLE_0:def_7;
then ( X c= (R ~) .:^ Y iff ((R .:^ X) `) /\ Y = {} ) by A1, Th48, Th59;
then ( X c= (R ~) .:^ Y iff (R .:^ X) ` misses Y ) by XBOOLE_0:def_7;
hence ( X c= (R ~) .:^ Y iff Y c= R .:^ X ) by SUBSET_1:24; ::_thesis: verum
end;
theorem :: RELSET_2:61
for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( R .: (X `) c= Y ` iff (R ~) .: Y c= X )
proof
let A, B be set ; ::_thesis: for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( R .: (X `) c= Y ` iff (R ~) .: Y c= X )
let X be Subset of A; ::_thesis: for Y being Subset of B
for R being Relation of A,B holds
( R .: (X `) c= Y ` iff (R ~) .: Y c= X )
let Y be Subset of B; ::_thesis: for R being Relation of A,B holds
( R .: (X `) c= Y ` iff (R ~) .: Y c= X )
let R be Relation of A,B; ::_thesis: ( R .: (X `) c= Y ` iff (R ~) .: Y c= X )
( X ` misses (R ~) .: Y iff Y misses R .: (X `) ) by Th45;
hence ( R .: (X `) c= Y ` iff (R ~) .: Y c= X ) by SUBSET_1:23, SUBSET_1:24; ::_thesis: verum
end;
theorem :: RELSET_2:62
for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( X c= (R ~) .:^ (R .:^ X) & Y c= R .:^ ((R ~) .:^ Y) ) by Th60;
theorem :: RELSET_2:63
for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
proof
let A, B be set ; ::_thesis: for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
let X be Subset of A; ::_thesis: for Y being Subset of B
for R being Relation of A,B holds
( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
let Y be Subset of B; ::_thesis: for R being Relation of A,B holds
( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
let R be Relation of A,B; ::_thesis: ( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
A1: R .:^ X c= R .:^ ((R ~) .:^ (R .:^ X)) by Th60;
X c= (R ~) .:^ (R .:^ X) by Th60;
then R .:^ ((R ~) .:^ (R .:^ X)) c= R .:^ X by Th31;
hence R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) by A1, XBOOLE_0:def_10; ::_thesis: (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y))
thus (R ~) .:^ Y c= (R ~) .:^ (R .:^ ((R ~) .:^ Y)) by Th60; :: according to XBOOLE_0:def_10 ::_thesis: (R ~) .:^ (R .:^ ((R ~) .:^ Y)) c= (R ~) .:^ Y
Y c= R .:^ ((R ~) .:^ Y) by Th60;
hence (R ~) .:^ (R .:^ ((R ~) .:^ Y)) c= (R ~) .:^ Y by Th31; ::_thesis: verum
end;
theorem :: RELSET_2:64
for A, B being set
for R being Relation of A,B holds (id A) * R = R * (id B)
proof
let A, B be set ; ::_thesis: for R being Relation of A,B holds (id A) * R = R * (id B)
let R be Relation of A,B; ::_thesis: (id A) * R = R * (id B)
(id A) * R = R by FUNCT_2:17
.= R * (id B) by FUNCT_2:17 ;
hence (id A) * R = R * (id B) ; ::_thesis: verum
end;