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