:: PARTIT_2 semantic presentation begin definition let Y be non empty set ; let G be non empty Subset of (PARTITIONS Y); :: original: Element redefine mode Element of G -> a_partition of Y; coherence for b1 being Element of G holds b1 is a_partition of Y proof let p be Element of G; ::_thesis: p is a_partition of Y thus p is a_partition of Y by PARTIT1:def_3; ::_thesis: verum end; end; theorem Th1: :: PARTIT_2:1 for Y being non empty set holds '/\' ({} (PARTITIONS Y)) = %O Y proof let Y be non empty set ; ::_thesis: '/\' ({} (PARTITIONS Y)) = %O Y for x being set holds ( x in %O Y iff ex h being Function ex F being Subset-Family of Y st ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds h . d in d ) & x = Intersect F & x <> {} ) ) proof let x be set ; ::_thesis: ( x in %O Y iff ex h being Function ex F being Subset-Family of Y st ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds h . d in d ) & x = Intersect F & x <> {} ) ) hereby ::_thesis: ( ex h being Function ex F being Subset-Family of Y st ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds h . d in d ) & x = Intersect F & x <> {} ) implies x in %O Y ) reconsider h = {} as Function ; assume x in %O Y ; ::_thesis: ex h being Function ex F being Element of bool (bool Y) st ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds h . d in d ) & x = Intersect F & x <> {} ) then A1: x in {Y} by PARTIT1:def_8; take h = h; ::_thesis: ex F being Element of bool (bool Y) st ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds h . d in d ) & x = Intersect F & x <> {} ) take F = {} (bool Y); ::_thesis: ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds h . d in d ) & x = Intersect F & x <> {} ) thus dom h = {} (PARTITIONS Y) ; ::_thesis: ( rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds h . d in d ) & x = Intersect F & x <> {} ) thus rng h = F ; ::_thesis: ( ( for d being set st d in {} (PARTITIONS Y) holds h . d in d ) & x = Intersect F & x <> {} ) thus for d being set st d in {} (PARTITIONS Y) holds h . d in d ; ::_thesis: ( x = Intersect F & x <> {} ) x = Y by A1, TARSKI:def_1; hence x = Intersect F by SETFAM_1:def_9; ::_thesis: x <> {} thus x <> {} by A1, TARSKI:def_1; ::_thesis: verum end; given h being Function, F being Subset-Family of Y such that A2: ( dom h = {} (PARTITIONS Y) & rng h = F ) and for d being set st d in {} (PARTITIONS Y) holds h . d in d and A3: x = Intersect F and x <> {} ; ::_thesis: x in %O Y F = {} by A2, RELAT_1:42; then x = Y by A3, SETFAM_1:def_9; then x in {Y} by TARSKI:def_1; hence x in %O Y by PARTIT1:def_8; ::_thesis: verum end; hence '/\' ({} (PARTITIONS Y)) = %O Y by BVFUNC_2:def_1; ::_thesis: verum end; theorem Th2: :: PARTIT_2:2 for Y being non empty set for R, S being Equivalence_Relation of Y holds R \/ S c= R * S proof let Y be non empty set ; ::_thesis: for R, S being Equivalence_Relation of Y holds R \/ S c= R * S let R, S be Equivalence_Relation of Y; ::_thesis: R \/ S c= R * S let x, y be Element of Y; :: according to RELSET_1:def_1 ::_thesis: ( not [x,y] in R \/ S or [x,y] in R * S ) assume A1: [x,y] in R \/ S ; ::_thesis: [x,y] in R * S percases ( [x,y] in R or [x,y] in S ) by A1, XBOOLE_0:def_3; supposeA2: [x,y] in R ; ::_thesis: [x,y] in R * S [y,y] in S by EQREL_1:5; hence [x,y] in R * S by A2, RELAT_1:def_8; ::_thesis: verum end; supposeA3: [x,y] in S ; ::_thesis: [x,y] in R * S [x,x] in R by EQREL_1:5; hence [x,y] in R * S by A3, RELAT_1:def_8; ::_thesis: verum end; end; end; theorem :: PARTIT_2:3 for Y being non empty set for R being Relation of Y holds R c= nabla Y ; theorem Th4: :: PARTIT_2:4 for Y being non empty set for R being Equivalence_Relation of Y holds ( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y ) proof let Y be non empty set ; ::_thesis: for R being Equivalence_Relation of Y holds ( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y ) let R be Equivalence_Relation of Y; ::_thesis: ( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y ) (nabla Y) \/ R c= (nabla Y) * R by Th2; then nabla Y c= (nabla Y) * R by EQREL_1:1; hence (nabla Y) * R = nabla Y by XBOOLE_0:def_10; ::_thesis: R * (nabla Y) = nabla Y (nabla Y) \/ R c= R * (nabla Y) by Th2; then nabla Y c= R * (nabla Y) by EQREL_1:1; hence R * (nabla Y) = nabla Y by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th5: :: PARTIT_2:5 for Y being non empty set for P being a_partition of Y for x, y being Element of Y holds ( [x,y] in ERl P iff x in EqClass (y,P) ) proof let Y be non empty set ; ::_thesis: for P being a_partition of Y for x, y being Element of Y holds ( [x,y] in ERl P iff x in EqClass (y,P) ) let P be a_partition of Y; ::_thesis: for x, y being Element of Y holds ( [x,y] in ERl P iff x in EqClass (y,P) ) let x, y be Element of Y; ::_thesis: ( [x,y] in ERl P iff x in EqClass (y,P) ) hereby ::_thesis: ( x in EqClass (y,P) implies [x,y] in ERl P ) assume [x,y] in ERl P ; ::_thesis: x in EqClass (y,P) then ex A being Subset of Y st ( A in P & x in A & y in A ) by PARTIT1:def_6; hence x in EqClass (y,P) by EQREL_1:def_6; ::_thesis: verum end; y in EqClass (y,P) by EQREL_1:def_6; hence ( x in EqClass (y,P) implies [x,y] in ERl P ) by PARTIT1:def_6; ::_thesis: verum end; theorem :: PARTIT_2:6 for Y being non empty set for P, Q, R being a_partition of Y st ERl R = (ERl P) * (ERl Q) holds for x, y being Element of Y holds ( x in EqClass (y,R) iff ex z being Element of Y st ( x in EqClass (z,P) & z in EqClass (y,Q) ) ) proof let Y be non empty set ; ::_thesis: for P, Q, R being a_partition of Y st ERl R = (ERl P) * (ERl Q) holds for x, y being Element of Y holds ( x in EqClass (y,R) iff ex z being Element of Y st ( x in EqClass (z,P) & z in EqClass (y,Q) ) ) let P, Q, R be a_partition of Y; ::_thesis: ( ERl R = (ERl P) * (ERl Q) implies for x, y being Element of Y holds ( x in EqClass (y,R) iff ex z being Element of Y st ( x in EqClass (z,P) & z in EqClass (y,Q) ) ) ) assume A1: ERl R = (ERl P) * (ERl Q) ; ::_thesis: for x, y being Element of Y holds ( x in EqClass (y,R) iff ex z being Element of Y st ( x in EqClass (z,P) & z in EqClass (y,Q) ) ) let x, y be Element of Y; ::_thesis: ( x in EqClass (y,R) iff ex z being Element of Y st ( x in EqClass (z,P) & z in EqClass (y,Q) ) ) hereby ::_thesis: ( ex z being Element of Y st ( x in EqClass (z,P) & z in EqClass (y,Q) ) implies x in EqClass (y,R) ) assume x in EqClass (y,R) ; ::_thesis: ex z being Element of Y st ( x in EqClass (z,P) & z in EqClass (y,Q) ) then [x,y] in ERl R by Th5; then consider z being Element of Y such that A2: [x,z] in ERl P and A3: [z,y] in ERl Q by A1, RELSET_1:28; take z = z; ::_thesis: ( x in EqClass (z,P) & z in EqClass (y,Q) ) thus x in EqClass (z,P) by A2, Th5; ::_thesis: z in EqClass (y,Q) thus z in EqClass (y,Q) by A3, Th5; ::_thesis: verum end; given z being Element of Y such that A4: ( x in EqClass (z,P) & z in EqClass (y,Q) ) ; ::_thesis: x in EqClass (y,R) ( [x,z] in ERl P & [z,y] in ERl Q ) by A4, Th5; then [x,y] in ERl R by A1, RELAT_1:def_8; hence x in EqClass (y,R) by Th5; ::_thesis: verum end; theorem Th7: :: PARTIT_2:7 for R, S being Relation for Y being set st R is_reflexive_in Y & S is_reflexive_in Y holds R * S is_reflexive_in Y proof let R, S be Relation; ::_thesis: for Y being set st R is_reflexive_in Y & S is_reflexive_in Y holds R * S is_reflexive_in Y let Y be set ; ::_thesis: ( R is_reflexive_in Y & S is_reflexive_in Y implies R * S is_reflexive_in Y ) assume A1: ( R is_reflexive_in Y & S is_reflexive_in Y ) ; ::_thesis: R * S is_reflexive_in Y let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in Y or [x,x] in R * S ) assume x in Y ; ::_thesis: [x,x] in R * S then ( [x,x] in R & [x,x] in S ) by A1, RELAT_2:def_1; hence [x,x] in R * S by RELAT_1:def_8; ::_thesis: verum end; theorem Th8: :: PARTIT_2:8 for R being Relation for Y being set st R is_reflexive_in Y holds Y c= field R proof let R be Relation; ::_thesis: for Y being set st R is_reflexive_in Y holds Y c= field R let Y be set ; ::_thesis: ( R is_reflexive_in Y implies Y c= field R ) assume A1: R is_reflexive_in Y ; ::_thesis: Y c= field R let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in field R ) assume x in Y ; ::_thesis: x in field R then [x,x] in R by A1, RELAT_2:def_1; hence x in field R by RELAT_1:15; ::_thesis: verum end; theorem Th9: :: PARTIT_2:9 for Y being set for R being Relation of Y st R is_reflexive_in Y holds Y = field R proof let Y be set ; ::_thesis: for R being Relation of Y st R is_reflexive_in Y holds Y = field R let R be Relation of Y; ::_thesis: ( R is_reflexive_in Y implies Y = field R ) assume R is_reflexive_in Y ; ::_thesis: Y = field R hence Y c= field R by Th8; :: according to XBOOLE_0:def_10 ::_thesis: field R c= Y field R c= Y \/ Y by RELSET_1:8; hence field R c= Y ; ::_thesis: verum end; theorem :: PARTIT_2:10 for Y being non empty set for R, S being Equivalence_Relation of Y st R * S = S * R holds R * S is Equivalence_Relation of Y proof let Y be non empty set ; ::_thesis: for R, S being Equivalence_Relation of Y st R * S = S * R holds R * S is Equivalence_Relation of Y let R, S be Equivalence_Relation of Y; ::_thesis: ( R * S = S * R implies R * S is Equivalence_Relation of Y ) assume A1: R * S = S * R ; ::_thesis: R * S is Equivalence_Relation of Y A2: field S = Y by ORDERS_1:12; then A3: S is_reflexive_in Y by RELAT_2:def_9; A4: field R = Y by ORDERS_1:12; then R is_reflexive_in Y by RELAT_2:def_9; then R * S is_reflexive_in Y by A3, Th7; then A5: ( field (R * S) = Y & dom (R * S) = Y ) by ORDERS_1:13; A6: R * S is_symmetric_in Y proof A7: S is_symmetric_in Y by A2, RELAT_2:def_11; let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in Y or not y in Y or not [x,y] in R * S or [y,x] in R * S ) assume that A8: x in Y and A9: y in Y ; ::_thesis: ( not [x,y] in R * S or [y,x] in R * S ) assume [x,y] in R * S ; ::_thesis: [y,x] in R * S then consider z being set such that A10: [x,z] in R and A11: [z,y] in S by RELAT_1:def_8; z in field S by A11, RELAT_1:15; then A12: [y,z] in S by A2, A7, A9, A11, RELAT_2:def_3; A13: R is_symmetric_in Y by A4, RELAT_2:def_11; z in field R by A10, RELAT_1:15; then [z,x] in R by A4, A13, A8, A10, RELAT_2:def_3; hence [y,x] in R * S by A1, A12, RELAT_1:def_8; ::_thesis: verum end; A14: ( R * R c= R & S * S c= S ) by RELAT_2:27; (R * S) * (R * S) = ((R * S) * R) * S by RELAT_1:36 .= (R * (R * S)) * S by A1, RELAT_1:36 .= ((R * R) * S) * S by RELAT_1:36 .= (R * R) * (S * S) by RELAT_1:36 ; then (R * S) * (R * S) c= R * S by A14, RELAT_1:31; hence R * S is Equivalence_Relation of Y by A5, A6, PARTFUN1:def_2, RELAT_2:27, RELAT_2:def_11; ::_thesis: verum end; begin theorem Th11: :: PARTIT_2:11 for Y being non empty set for a, b being Function of Y,BOOLEAN st a '<' b holds 'not' b '<' 'not' a proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st a '<' b holds 'not' b '<' 'not' a let a, b be Function of Y,BOOLEAN; ::_thesis: ( a '<' b implies 'not' b '<' 'not' a ) assume A1: a '<' b ; ::_thesis: 'not' b '<' 'not' a let x be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ('not' b) . x = TRUE or ('not' a) . x = TRUE ) assume A2: ('not' b) . x = TRUE ; ::_thesis: ('not' a) . x = TRUE b . x = ('not' ('not' b)) . x .= 'not' TRUE by A2, MARGREL1:def_19 .= FALSE ; then a . x <> TRUE by A1, BVFUNC_1:def_12; then a . x = FALSE by XBOOLEAN:def_3; hence ('not' a) . x = 'not' FALSE by MARGREL1:def_19 .= TRUE ; ::_thesis: verum end; theorem Th12: :: PARTIT_2:12 for Y being non empty set for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for P being a_partition of Y st a '<' b holds All (a,P,G) '<' All (b,P,G) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for P being a_partition of Y st a '<' b holds All (a,P,G) '<' All (b,P,G) let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for P being a_partition of Y st a '<' b holds All (a,P,G) '<' All (b,P,G) let G be Subset of (PARTITIONS Y); ::_thesis: for P being a_partition of Y st a '<' b holds All (a,P,G) '<' All (b,P,G) let P be a_partition of Y; ::_thesis: ( a '<' b implies All (a,P,G) '<' All (b,P,G) ) assume A1: a '<' b ; ::_thesis: All (a,P,G) '<' All (b,P,G) let x be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All (a,P,G)) . x = TRUE or (All (b,P,G)) . x = TRUE ) assume A2: (All (a,P,G)) . x = TRUE ; ::_thesis: (All (b,P,G)) . x = TRUE A3: All (a,P,G) = B_INF (a,(CompF (P,G))) by BVFUNC_2:def_9; A4: for y being Element of Y st y in EqClass (x,(CompF (P,G))) holds b . y = TRUE proof let y be Element of Y; ::_thesis: ( y in EqClass (x,(CompF (P,G))) implies b . y = TRUE ) assume y in EqClass (x,(CompF (P,G))) ; ::_thesis: b . y = TRUE then a . y = TRUE by A3, A2, BVFUNC_1:def_16; hence b . y = TRUE by A1, BVFUNC_1:def_12; ::_thesis: verum end; All (b,P,G) = B_INF (b,(CompF (P,G))) by BVFUNC_2:def_9; hence (All (b,P,G)) . x = TRUE by A4, BVFUNC_1:def_16; ::_thesis: verum end; theorem :: PARTIT_2:13 for Y being non empty set for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for P being a_partition of Y st a '<' b holds Ex (a,P,G) '<' Ex (b,P,G) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for P being a_partition of Y st a '<' b holds Ex (a,P,G) '<' Ex (b,P,G) let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for P being a_partition of Y st a '<' b holds Ex (a,P,G) '<' Ex (b,P,G) let G be Subset of (PARTITIONS Y); ::_thesis: for P being a_partition of Y st a '<' b holds Ex (a,P,G) '<' Ex (b,P,G) let P be a_partition of Y; ::_thesis: ( a '<' b implies Ex (a,P,G) '<' Ex (b,P,G) ) A1: Ex (b,P,G) = Ex (('not' ('not' b)),P,G) .= 'not' (All (('not' b),P,G)) by BVFUNC_2:18 ; assume a '<' b ; ::_thesis: Ex (a,P,G) '<' Ex (b,P,G) then 'not' b '<' 'not' a by Th11; then A2: All (('not' b),P,G) '<' All (('not' a),P,G) by Th12; Ex (a,P,G) = Ex (('not' ('not' a)),P,G) .= 'not' (All (('not' a),P,G)) by BVFUNC_2:18 ; hence Ex (a,P,G) '<' Ex (b,P,G) by A1, A2, Th11; ::_thesis: verum end; begin Lm1: for Y being non empty set for G being Subset of (PARTITIONS Y) st G is independent holds for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) st G is independent holds for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) let G be Subset of (PARTITIONS Y); ::_thesis: ( G is independent implies for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ) assume A1: G is independent ; ::_thesis: for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) let P, Q be Subset of (PARTITIONS Y); ::_thesis: ( P c= G & Q c= G implies (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ) assume that A2: P c= G and A3: Q c= G ; ::_thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) percases ( P = {} or Q = {} or ( P <> {} & Q <> {} ) ) ; suppose P = {} ; ::_thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) then P = {} (PARTITIONS Y) ; then (ERl ('/\' Q)) * (ERl ('/\' P)) = (ERl ('/\' Q)) * (ERl (%O Y)) by Th1 .= (ERl ('/\' Q)) * (nabla Y) by PARTIT1:33 .= nabla Y by Th4 ; hence (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; ::_thesis: verum end; suppose Q = {} ; ::_thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) then Q = {} (PARTITIONS Y) ; then (ERl ('/\' Q)) * (ERl ('/\' P)) = (ERl (%O Y)) * (ERl ('/\' P)) by Th1 .= (nabla Y) * (ERl ('/\' P)) by PARTIT1:33 .= nabla Y by Th4 ; hence (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; ::_thesis: verum end; supposeA4: ( P <> {} & Q <> {} ) ; ::_thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) then reconsider G9 = G as non empty Subset of (PARTITIONS Y) by A2; let x, y be Element of Y; :: according to RELSET_1:def_1 ::_thesis: ( not [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) or [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) ) assume [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) ; ::_thesis: [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) then consider z being Element of Y such that A5: [x,z] in ERl ('/\' P) and A6: [z,y] in ERl ('/\' Q) by RELSET_1:28; consider A being Subset of Y such that A7: A in '/\' P and A8: x in A and A9: z in A by A5, PARTIT1:def_6; consider B being Subset of Y such that A10: B in '/\' Q and A11: z in B and A12: y in B by A6, PARTIT1:def_6; consider hQ being Function, FQ being Subset-Family of Y such that A13: ( dom hQ = Q & rng hQ = FQ ) and A14: for d being set st d in Q holds hQ . d in d and A15: B = Intersect FQ and B <> {} by A10, BVFUNC_2:def_1; consider hP being Function, FP being Subset-Family of Y such that A16: ( dom hP = P & rng hP = FP ) and A17: for d being set st d in P holds hP . d in d and A18: A = Intersect FP and A <> {} by A7, BVFUNC_2:def_1; reconsider P = P, Q = Q as non empty Subset of (PARTITIONS Y) by A4; deffunc H1( Element of P) -> Element of \$1 = EqClass (y,\$1); consider hP9 being Function of P,(bool Y) such that A19: for p being Element of P holds hP9 . p = H1(p) from FUNCT_2:sch_4(); deffunc H2( Element of Q) -> Element of \$1 = EqClass (x,\$1); consider hQ9 being Function of Q,(bool Y) such that A20: for p being Element of Q holds hQ9 . p = H2(p) from FUNCT_2:sch_4(); deffunc H3( set ) -> set = \$1; A21: for d being Element of G9 holds bool Y meets H3(d) proof let d be Element of G9; ::_thesis: bool Y meets H3(d) d meets d ; hence bool Y meets d by XBOOLE_1:63; ::_thesis: verum end; consider h9 being Function of G9,(bool Y) such that A22: for d being Element of G9 holds h9 . d in H3(d) from FUNCT_2:sch_10(A21); set h = (h9 +* hP9) +* hQ9; A23: dom hQ9 = Q by FUNCT_2:def_1; A24: dom hP9 = P by FUNCT_2:def_1; A25: for d being set st d in P holds ((h9 +* hP9) +* hQ9) . d = hP9 . d proof let d be set ; ::_thesis: ( d in P implies ((h9 +* hP9) +* hQ9) . d = hP9 . d ) assume A26: d in P ; ::_thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d then reconsider d9 = d as Element of P ; percases ( d in Q or not d in Q ) ; supposeA27: d in Q ; ::_thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d then A28: hQ . d in FQ by A13, FUNCT_1:def_3; then A29: y in hQ . d by A12, A15, SETFAM_1:43; A30: z in hQ . d by A11, A15, A28, SETFAM_1:43; A31: hQ . d in d by A14, A27; A32: hP . d in FP by A16, A26, FUNCT_1:def_3; then A33: x in hP . d by A8, A18, SETFAM_1:43; A34: z in hP . d by A9, A18, A32, SETFAM_1:43; A35: hP . d in d by A17, A26; thus ((h9 +* hP9) +* hQ9) . d = hQ9 . d by A23, A27, FUNCT_4:13 .= EqClass (x,d9) by A20, A27 .= hP . d by A35, A33, EQREL_1:def_6 .= EqClass (z,d9) by A35, A34, EQREL_1:def_6 .= hQ . d by A31, A30, EQREL_1:def_6 .= EqClass (y,d9) by A31, A29, EQREL_1:def_6 .= hP9 . d by A19 ; ::_thesis: verum end; suppose not d in Q ; ::_thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d hence ((h9 +* hP9) +* hQ9) . d = (h9 +* hP9) . d by A23, FUNCT_4:11 .= hP9 . d by A24, A26, FUNCT_4:13 ; ::_thesis: verum end; end; end; reconsider FP9 = rng hP9, FQ9 = rng hQ9 as Subset-Family of Y ; set A9 = Intersect FP9; set B9 = Intersect FQ9; for a being set st a in FP9 holds y in a proof let a be set ; ::_thesis: ( a in FP9 implies y in a ) assume a in FP9 ; ::_thesis: y in a then consider b being set such that A36: b in dom hP9 and A37: hP9 . b = a by FUNCT_1:def_3; reconsider b = b as Element of P by A36; a = EqClass (y,b) by A19, A37; hence y in a by EQREL_1:def_6; ::_thesis: verum end; then A38: y in Intersect FP9 by SETFAM_1:43; for a being set st a in FQ9 holds x in a proof let a be set ; ::_thesis: ( a in FQ9 implies x in a ) assume a in FQ9 ; ::_thesis: x in a then consider b being set such that A39: b in dom hQ9 and A40: hQ9 . b = a by FUNCT_1:def_3; reconsider b = b as Element of Q by A39; a = EqClass (x,b) by A20, A40; hence x in a by EQREL_1:def_6; ::_thesis: verum end; then A41: x in Intersect FQ9 by SETFAM_1:43; A42: for d being set st d in Q holds hQ9 . d in d proof let d be set ; ::_thesis: ( d in Q implies hQ9 . d in d ) assume d in Q ; ::_thesis: hQ9 . d in d then reconsider d = d as Element of Q ; hQ9 . d = EqClass (x,d) by A20; hence hQ9 . d in d ; ::_thesis: verum end; rng (h9 +* hP9) c= (rng h9) \/ (rng hP9) by FUNCT_4:17; then rng (h9 +* hP9) c= bool Y by XBOOLE_1:1; then ( rng ((h9 +* hP9) +* hQ9) c= (rng (h9 +* hP9)) \/ (rng hQ9) & (rng (h9 +* hP9)) \/ (rng hQ9) c= bool Y ) by FUNCT_4:17, XBOOLE_1:8; then reconsider F = rng ((h9 +* hP9) +* hQ9) as Subset-Family of Y by XBOOLE_1:1; A43: dom ((h9 +* hP9) +* hQ9) = (dom (h9 +* hP9)) \/ Q by A23, FUNCT_4:def_1 .= ((dom h9) \/ P) \/ Q by A24, FUNCT_4:def_1 .= (G \/ P) \/ Q by FUNCT_2:def_1 .= G \/ Q by A2, XBOOLE_1:12 .= G by A3, XBOOLE_1:12 ; A44: for d being set st d in P holds hP9 . d in d proof let d be set ; ::_thesis: ( d in P implies hP9 . d in d ) assume d in P ; ::_thesis: hP9 . d in d then reconsider d = d as Element of P ; hP9 . d = EqClass (y,d) by A19; hence hP9 . d in d ; ::_thesis: verum end; for d being set st d in G holds ((h9 +* hP9) +* hQ9) . d in d proof let d be set ; ::_thesis: ( d in G implies ((h9 +* hP9) +* hQ9) . d in d ) assume A45: d in G ; ::_thesis: ((h9 +* hP9) +* hQ9) . d in d G = (P \/ Q) \/ G by A2, A3, XBOOLE_1:8, XBOOLE_1:12 .= (G \ (P \/ Q)) \/ (P \/ Q) by XBOOLE_1:39 ; then A46: ( d in G \ (P \/ Q) or d in P \/ Q ) by A45, XBOOLE_0:def_3; percases ( d in Q or d in P or d in G \ (P \/ Q) ) by A46, XBOOLE_0:def_3; supposeA47: d in Q ; ::_thesis: ((h9 +* hP9) +* hQ9) . d in d then ((h9 +* hP9) +* hQ9) . d = hQ9 . d by A23, FUNCT_4:13; hence ((h9 +* hP9) +* hQ9) . d in d by A42, A47; ::_thesis: verum end; supposeA48: d in P ; ::_thesis: ((h9 +* hP9) +* hQ9) . d in d then ((h9 +* hP9) +* hQ9) . d = hP9 . d by A25; hence ((h9 +* hP9) +* hQ9) . d in d by A44, A48; ::_thesis: verum end; supposeA49: d in G \ (P \/ Q) ; ::_thesis: ((h9 +* hP9) +* hQ9) . d in d then not d in P \/ Q by XBOOLE_0:def_5; then ( (h9 +* hP9) +* hQ9 = h9 +* (hP9 +* hQ9) & not d in dom (hP9 +* hQ9) ) by A24, A23, FUNCT_4:14, FUNCT_4:def_1; then A50: ((h9 +* hP9) +* hQ9) . d = h9 . d by FUNCT_4:11; d in G by A49, XBOOLE_0:def_5; hence ((h9 +* hP9) +* hQ9) . d in d by A22, A50; ::_thesis: verum end; end; end; then Intersect F <> {} by A1, A43, BVFUNC_2:def_5; then consider t being Element of Y such that A51: t in Intersect F by SUBSET_1:4; for a being set st a in FP9 holds t in a proof let a be set ; ::_thesis: ( a in FP9 implies t in a ) assume a in FP9 ; ::_thesis: t in a then consider b being set such that A52: b in dom hP9 and A53: hP9 . b = a by FUNCT_1:def_3; hP9 . b = ((h9 +* hP9) +* hQ9) . b by A25, A52; then a in F by A2, A24, A43, A52, A53, FUNCT_1:def_3; hence t in a by A51, SETFAM_1:43; ::_thesis: verum end; then A54: t in Intersect FP9 by SETFAM_1:43; then Intersect FP9 in '/\' P by A44, A24, BVFUNC_2:def_1; then A55: [t,y] in ERl ('/\' P) by A38, A54, PARTIT1:def_6; for a being set st a in FQ9 holds t in a proof let a be set ; ::_thesis: ( a in FQ9 implies t in a ) assume a in FQ9 ; ::_thesis: t in a then consider b being set such that A56: b in dom hQ9 and A57: hQ9 . b = a by FUNCT_1:def_3; reconsider b = b as Element of Q by A56; hQ9 . b = ((h9 +* hP9) +* hQ9) . b by A56, FUNCT_4:13; then a in F by A3, A23, A43, A56, A57, FUNCT_1:def_3; hence t in a by A51, SETFAM_1:43; ::_thesis: verum end; then A58: t in Intersect FQ9 by SETFAM_1:43; then Intersect FQ9 in '/\' Q by A42, A23, BVFUNC_2:def_1; then [x,t] in ERl ('/\' Q) by A41, A58, PARTIT1:def_6; hence [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) by A55, RELSET_1:28; ::_thesis: verum end; end; end; theorem Th14: :: PARTIT_2:14 for Y being non empty set for G being Subset of (PARTITIONS Y) st G is independent holds for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) st G is independent holds for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) let G be Subset of (PARTITIONS Y); ::_thesis: ( G is independent implies for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) ) assume A1: G is independent ; ::_thesis: for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) let P, Q be Subset of (PARTITIONS Y); ::_thesis: ( P c= G & Q c= G implies (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) ) assume ( P c= G & Q c= G ) ; ::_thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) then ( (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) & (ERl ('/\' Q)) * (ERl ('/\' P)) c= (ERl ('/\' P)) * (ERl ('/\' Q)) ) by A1, Lm1; hence (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th15: :: PARTIT_2:15 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for P, Q being a_partition of Y st G is independent holds All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for P, Q being a_partition of Y st G is independent holds All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for P, Q being a_partition of Y st G is independent holds All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G) let G be Subset of (PARTITIONS Y); ::_thesis: for P, Q being a_partition of Y st G is independent holds All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G) let P, Q be a_partition of Y; ::_thesis: ( G is independent implies All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G) ) set A = G \ {P}; set B = G \ {Q}; A1: CompF (P,G) = '/\' (G \ {P}) by BVFUNC_2:def_7; A2: ( G \ {P} c= G & G \ {Q} c= G ) by XBOOLE_1:36; A3: CompF (Q,G) = '/\' (G \ {Q}) by BVFUNC_2:def_7; assume G is independent ; ::_thesis: All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G) then A4: (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) = (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P}))) by A2, Th14; A5: for y being Element of Y holds ( ( ( for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE ) & ( ex x being Element of Y st ( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE ) ) proof let y be Element of Y; ::_thesis: ( ( ( for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE ) & ( ex x being Element of Y st ( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE ) ) hereby ::_thesis: ( ex x being Element of Y st ( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE ) assume A6: for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds (B_INF (a,(CompF (P,G)))) . x = TRUE ; ::_thesis: (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE for x being Element of Y st x in EqClass (y,(CompF (P,G))) holds (B_INF (a,(CompF (Q,G)))) . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (y,(CompF (P,G))) implies (B_INF (a,(CompF (Q,G)))) . x = TRUE ) assume x in EqClass (y,(CompF (P,G))) ; ::_thesis: (B_INF (a,(CompF (Q,G)))) . x = TRUE then A7: [x,y] in ERl ('/\' (G \ {P})) by A1, Th5; for z being Element of Y st z in EqClass (x,(CompF (Q,G))) holds a . z = TRUE proof let z be Element of Y; ::_thesis: ( z in EqClass (x,(CompF (Q,G))) implies a . z = TRUE ) assume z in EqClass (x,(CompF (Q,G))) ; ::_thesis: a . z = TRUE then [z,x] in ERl ('/\' (G \ {Q})) by A3, Th5; then [z,y] in (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) by A4, A7, RELAT_1:def_8; then consider u being set such that A8: [z,u] in ERl ('/\' (G \ {P})) and A9: [u,y] in ERl ('/\' (G \ {Q})) by RELAT_1:def_8; u in field (ERl ('/\' (G \ {Q}))) by A9, RELAT_1:15; then reconsider u = u as Element of Y by ORDERS_1:12; u in EqClass (y,(CompF (Q,G))) by A3, A9, Th5; then A10: (B_INF (a,(CompF (P,G)))) . u <> FALSE by A6; z in EqClass (u,(CompF (P,G))) by A1, A8, Th5; hence a . z = TRUE by A10, BVFUNC_1:def_16; ::_thesis: verum end; hence (B_INF (a,(CompF (Q,G)))) . x = TRUE by BVFUNC_1:def_16; ::_thesis: verum end; hence (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE by BVFUNC_1:def_16; ::_thesis: verum end; given x being Element of Y such that A11: x in EqClass (y,(CompF (Q,G))) and A12: (B_INF (a,(CompF (P,G)))) . x <> TRUE ; ::_thesis: (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE consider z being Element of Y such that A13: z in EqClass (x,(CompF (P,G))) and A14: a . z <> TRUE by A12, BVFUNC_1:def_16; A15: [x,y] in ERl ('/\' (G \ {Q})) by A3, A11, Th5; [z,x] in ERl ('/\' (G \ {P})) by A1, A13, Th5; then [z,y] in (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P}))) by A4, A15, RELAT_1:def_8; then consider u being set such that A16: [z,u] in ERl ('/\' (G \ {Q})) and A17: [u,y] in ERl ('/\' (G \ {P})) by RELAT_1:def_8; u in field (ERl ('/\' (G \ {Q}))) by A16, RELAT_1:15; then reconsider u = u as Element of Y by ORDERS_1:12; z in EqClass (u,(CompF (Q,G))) by A3, A16, Th5; then A18: (B_INF (a,(CompF (Q,G)))) . u = FALSE by A14, BVFUNC_1:def_16; u in EqClass (y,(CompF (P,G))) by A1, A17, Th5; hence (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE by A18, BVFUNC_1:def_16; ::_thesis: verum end; thus All ((All (a,P,G)),Q,G) = B_INF ((All (a,P,G)),(CompF (Q,G))) by BVFUNC_2:def_9 .= B_INF ((B_INF (a,(CompF (P,G)))),(CompF (Q,G))) by BVFUNC_2:def_9 .= B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G))) by A5, BVFUNC_1:def_16 .= B_INF ((All (a,Q,G)),(CompF (P,G))) by BVFUNC_2:def_9 .= All ((All (a,Q,G)),P,G) by BVFUNC_2:def_9 ; ::_thesis: verum end; theorem :: PARTIT_2:16 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for P, Q being a_partition of Y st G is independent holds Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for P, Q being a_partition of Y st G is independent holds Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for P, Q being a_partition of Y st G is independent holds Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G) let G be Subset of (PARTITIONS Y); ::_thesis: for P, Q being a_partition of Y st G is independent holds Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G) let P, Q be a_partition of Y; ::_thesis: ( G is independent implies Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G) ) assume A1: G is independent ; ::_thesis: Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G) thus Ex ((Ex (a,P,G)),Q,G) = 'not' ('not' (Ex ((Ex (a,P,G)),Q,G))) .= 'not' (All (('not' (Ex (a,P,G))),Q,G)) by BVFUNC_2:19 .= 'not' (All ((All (('not' a),P,G)),Q,G)) by BVFUNC_2:19 .= 'not' (All ((All (('not' a),Q,G)),P,G)) by A1, Th15 .= 'not' (All (('not' (Ex (a,Q,G))),P,G)) by BVFUNC_2:19 .= 'not' ('not' (Ex ((Ex (a,Q,G)),P,G))) by BVFUNC_2:19 .= Ex ((Ex (a,Q,G)),P,G) ; ::_thesis: verum end; theorem :: PARTIT_2:17 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for P, Q being a_partition of Y st G is independent holds Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for P, Q being a_partition of Y st G is independent holds Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for P, Q being a_partition of Y st G is independent holds Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G) let G be Subset of (PARTITIONS Y); ::_thesis: for P, Q being a_partition of Y st G is independent holds Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G) let P, Q be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G) ) assume A1: G is independent ; ::_thesis: Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G) set A = G \ {P}; set B = G \ {Q}; ( G \ {P} c= G & G \ {Q} c= G ) by XBOOLE_1:36; then A2: (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) = (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P}))) by A1, Th14; A3: CompF (P,G) = '/\' (G \ {P}) by BVFUNC_2:def_7; A4: Ex ((All (a,P,G)),Q,G) = B_SUP ((All (a,P,G)),(CompF (Q,G))) by BVFUNC_2:def_10; A5: CompF (Q,G) = '/\' (G \ {Q}) by BVFUNC_2:def_7; let x be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((All (a,P,G)),Q,G)) . x = TRUE or (All ((Ex (a,Q,G)),P,G)) . x = TRUE ) assume A6: (Ex ((All (a,P,G)),Q,G)) . x = TRUE ; ::_thesis: (All ((Ex (a,Q,G)),P,G)) . x = TRUE A7: for z being Element of Y st z in EqClass (x,(CompF (P,G))) holds (Ex (a,Q,G)) . z = TRUE proof let z be Element of Y; ::_thesis: ( z in EqClass (x,(CompF (P,G))) implies (Ex (a,Q,G)) . z = TRUE ) consider y being Element of Y such that A8: y in EqClass (x,(CompF (Q,G))) and A9: (All (a,P,G)) . y = TRUE by A6, A4, BVFUNC_1:def_17; assume z in EqClass (x,(CompF (P,G))) ; ::_thesis: (Ex (a,Q,G)) . z = TRUE then [z,x] in ERl ('/\' (G \ {P})) by A3, Th5; then A10: [x,z] in ERl ('/\' (G \ {P})) by EQREL_1:6; [y,x] in ERl ('/\' (G \ {Q})) by A5, A8, Th5; then [y,z] in (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) by A2, A10, RELAT_1:def_8; then consider u being set such that A11: [y,u] in ERl ('/\' (G \ {P})) and A12: [u,z] in ERl ('/\' (G \ {Q})) by RELAT_1:def_8; u in field (ERl ('/\' (G \ {Q}))) by A12, RELAT_1:15; then reconsider u = u as Element of Y by ORDERS_1:12; [u,y] in ERl ('/\' (G \ {P})) by A11, EQREL_1:6; then ( All (a,P,G) = B_INF (a,(CompF (P,G))) & u in EqClass (y,(CompF (P,G))) ) by A3, Th5, BVFUNC_2:def_9; then A13: a . u = TRUE by A9, BVFUNC_1:def_16; ( Ex (a,Q,G) = B_SUP (a,(CompF (Q,G))) & u in EqClass (z,(CompF (Q,G))) ) by A5, A12, Th5, BVFUNC_2:def_10; hence (Ex (a,Q,G)) . z = TRUE by A13, BVFUNC_1:def_17; ::_thesis: verum end; All ((Ex (a,Q,G)),P,G) = B_INF ((Ex (a,Q,G)),(CompF (P,G))) by BVFUNC_2:def_9; hence (All ((Ex (a,Q,G)),P,G)) . x = TRUE by A7, BVFUNC_1:def_16; ::_thesis: verum end; begin notation let A, B be set ; synonym [#] (A,B) for [:A,B:]; end; definition let A, B be set ; func {} (A,B) -> Relation of A,B equals :: PARTIT_2:def 1 {} ; correctness coherence {} is Relation of A,B; by RELSET_1:12; :: original: [#] redefine func [#] (A,B) -> Relation of A,B; correctness coherence [#] (A,B) is Relation of A,B; proof [#] (A,B) c= [:A,B:] ; hence [#] (A,B) is Relation of A,B ; ::_thesis: verum end; end; :: deftheorem defines {} PARTIT_2:def_1_:_ for A, B being set holds {} (A,B) = {} ; registration let A, B be set ; cluster {} (A,B) -> empty ; coherence {} (A,B) is empty ; end; theorem :: PARTIT_2:18 for X being non empty set holds field (id X) = X proof let X be non empty set ; ::_thesis: field (id X) = X ( dom (id X) = X & rng (id X) = X ) ; then field (id X) = X \/ X by RELAT_1:def_6; hence field (id X) = X ; ::_thesis: verum end; theorem :: PARTIT_2:19 op1 = {[{},{}]} proof {{}} = dom op1 by CARD_1:49, FUNCT_2:def_1; then {} in dom op1 by TARSKI:def_1; then [{},(op1 . {})] in op1 by FUNCT_1:def_2; then A1: {[{},(op1 . {})]} c= op1 by ZFMISC_1:31; rng op1 = {(op1 . {})} by CARD_1:49, FUNCT_2:48; then A2: op1 . {} = {} by CARD_1:49, ZFMISC_1:18; op1 c= [:{{}},{{}}:] by CARD_1:49; then op1 c= {[{},{}]} by ZFMISC_1:29; hence op1 = {[{},{}]} by A2, A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: PARTIT_2:20 for A, B being set holds field ({} (A,B)) = {} by RELAT_1:40; theorem :: PARTIT_2:21 for X being non empty set for R being Relation of X st R is_reflexive_in X holds ( R is reflexive & field R = X ) proof let X be non empty set ; ::_thesis: for R being Relation of X st R is_reflexive_in X holds ( R is reflexive & field R = X ) let R be Relation of X; ::_thesis: ( R is_reflexive_in X implies ( R is reflexive & field R = X ) ) assume A1: R is_reflexive_in X ; ::_thesis: ( R is reflexive & field R = X ) then X = field R by Th9; hence ( R is reflexive & field R = X ) by A1, RELAT_2:def_9; ::_thesis: verum end; theorem :: PARTIT_2:22 for X being non empty set for R being Relation of X st R is_symmetric_in X holds R is symmetric proof let X be non empty set ; ::_thesis: for R being Relation of X st R is_symmetric_in X holds R is symmetric let R be Relation of X; ::_thesis: ( R is_symmetric_in X implies R is symmetric ) assume A1: R is_symmetric_in X ; ::_thesis: R is symmetric let x, y be set ; :: according to RELAT_2:def_3,RELAT_2:def_11 ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R ) field R c= X \/ X by RELSET_1:8; hence ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R ) by A1, RELAT_2:def_3; ::_thesis: verum end; theorem :: PARTIT_2:23 for X, S being non empty set for R being Relation of X st R is symmetric holds R is_symmetric_in S proof let X, S be non empty set ; ::_thesis: for R being Relation of X st R is symmetric holds R is_symmetric_in S let R be Relation of X; ::_thesis: ( R is symmetric implies R is_symmetric_in S ) assume R is symmetric ; ::_thesis: R is_symmetric_in S then A1: R is_symmetric_in field R by RELAT_2:def_11; let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in S or not y in S or not [x,y] in R or [y,x] in R ) assume ( x in S & y in S ) ; ::_thesis: ( not [x,y] in R or [y,x] in R ) assume A2: [x,y] in R ; ::_thesis: [y,x] in R then ( x in field R & y in field R ) by RELAT_1:15; hence [y,x] in R by A1, A2, RELAT_2:def_3; ::_thesis: verum end; theorem :: PARTIT_2:24 for X, S being non empty set for R being Relation of X st R is antisymmetric holds R is_antisymmetric_in S proof let X, S be non empty set ; ::_thesis: for R being Relation of X st R is antisymmetric holds R is_antisymmetric_in S let R be Relation of X; ::_thesis: ( R is antisymmetric implies R is_antisymmetric_in S ) assume R is antisymmetric ; ::_thesis: R is_antisymmetric_in S then A1: R is_antisymmetric_in field R by RELAT_2:def_12; let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in S or not y in S or not [x,y] in R or not [y,x] in R or x = y ) assume ( x in S & y in S ) ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y ) assume A2: [x,y] in R ; ::_thesis: ( not [y,x] in R or x = y ) then ( x in field R & y in field R ) by RELAT_1:15; hence ( not [y,x] in R or x = y ) by A1, A2, RELAT_2:def_4; ::_thesis: verum end; theorem :: PARTIT_2:25 for X being non empty set for R being Relation of X st R is_antisymmetric_in X holds R is antisymmetric proof let X be non empty set ; ::_thesis: for R being Relation of X st R is_antisymmetric_in X holds R is antisymmetric let R be Relation of X; ::_thesis: ( R is_antisymmetric_in X implies R is antisymmetric ) assume A1: R is_antisymmetric_in X ; ::_thesis: R is antisymmetric let x, y be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R or x = y ) field R c= X \/ X by RELSET_1:8; hence ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R or x = y ) by A1, RELAT_2:def_4; ::_thesis: verum end; theorem :: PARTIT_2:26 for X, S being non empty set for R being Relation of X st R is transitive holds R is_transitive_in S proof let X, S be non empty set ; ::_thesis: for R being Relation of X st R is transitive holds R is_transitive_in S let R be Relation of X; ::_thesis: ( R is transitive implies R is_transitive_in S ) assume R is transitive ; ::_thesis: R is_transitive_in S then A1: R is_transitive_in field R by RELAT_2:def_16; let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in S or not y in S or not z in S or not [x,y] in R or not [y,z] in R or [x,z] in R ) assume ( x in S & y in S & z in S ) ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R ) assume A2: [x,y] in R ; ::_thesis: ( not [y,z] in R or [x,z] in R ) then A3: x in field R by RELAT_1:15; assume A4: [y,z] in R ; ::_thesis: [x,z] in R then ( y in field R & z in field R ) by RELAT_1:15; hence [x,z] in R by A1, A2, A4, A3, RELAT_2:def_8; ::_thesis: verum end; theorem :: PARTIT_2:27 for X being non empty set for R being Relation of X st R is_transitive_in X holds R is transitive proof let X be non empty set ; ::_thesis: for R being Relation of X st R is_transitive_in X holds R is transitive let R be Relation of X; ::_thesis: ( R is_transitive_in X implies R is transitive ) assume A1: R is_transitive_in X ; ::_thesis: R is transitive let x, y, z be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R ) field R c= X \/ X by RELSET_1:8; hence ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R ) by A1, RELAT_2:def_8; ::_thesis: verum end; theorem :: PARTIT_2:28 for X, S being non empty set for R being Relation of X st R is asymmetric holds R is_asymmetric_in S proof let X, S be non empty set ; ::_thesis: for R being Relation of X st R is asymmetric holds R is_asymmetric_in S let R be Relation of X; ::_thesis: ( R is asymmetric implies R is_asymmetric_in S ) assume R is asymmetric ; ::_thesis: R is_asymmetric_in S then A1: R is_asymmetric_in field R by RELAT_2:def_13; let x, y be set ; :: according to RELAT_2:def_5 ::_thesis: ( not x in S or not y in S or not [x,y] in R or not [y,x] in R ) assume ( x in S & y in S ) ; ::_thesis: ( not [x,y] in R or not [y,x] in R ) assume A2: [x,y] in R ; ::_thesis: not [y,x] in R then ( x in field R & y in field R ) by RELAT_1:15; hence not [y,x] in R by A1, A2, RELAT_2:def_5; ::_thesis: verum end; theorem :: PARTIT_2:29 for X being non empty set for R being Relation of X st R is_asymmetric_in X holds R is asymmetric proof let X be non empty set ; ::_thesis: for R being Relation of X st R is_asymmetric_in X holds R is asymmetric let R be Relation of X; ::_thesis: ( R is_asymmetric_in X implies R is asymmetric ) assume A1: R is_asymmetric_in X ; ::_thesis: R is asymmetric let x, y be set ; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R ) field R c= X \/ X by RELSET_1:8; hence ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R ) by A1, RELAT_2:def_5; ::_thesis: verum end; theorem :: PARTIT_2:30 for X, S being non empty set for R being Relation of X st R is irreflexive & field R c= S holds R is_irreflexive_in S proof let X, S be non empty set ; ::_thesis: for R being Relation of X st R is irreflexive & field R c= S holds R is_irreflexive_in S let R be Relation of X; ::_thesis: ( R is irreflexive & field R c= S implies R is_irreflexive_in S ) assume that A1: R is irreflexive and A2: field R c= S ; ::_thesis: R is_irreflexive_in S let x be set ; :: according to RELAT_2:def_2 ::_thesis: ( not x in S or not [x,x] in R ) S = (field R) \/ (S \ (field R)) by A2, XBOOLE_1:45; then A3: ( not x in S or x in field R or x in S \ (field R) ) by XBOOLE_0:def_3; A4: ( x in S \ (field R) implies not [x,x] in R ) proof assume x in S \ (field R) ; ::_thesis: not [x,x] in R then x in S \ ((dom R) \/ (rng R)) by RELAT_1:def_6; then x in (S \ (dom R)) /\ (S \ (rng R)) by XBOOLE_1:53; then x in S \ (rng R) by XBOOLE_0:def_4; then not x in rng R by XBOOLE_0:def_5; hence not [x,x] in R by XTUPLE_0:def_13; ::_thesis: verum end; R is_irreflexive_in field R by A1, RELAT_2:def_10; hence ( not x in S or not [x,x] in R ) by A3, A4, RELAT_2:def_2; ::_thesis: verum end; theorem :: PARTIT_2:31 for X being non empty set for R being Relation of X st R is_irreflexive_in X holds R is irreflexive proof let X be non empty set ; ::_thesis: for R being Relation of X st R is_irreflexive_in X holds R is irreflexive let R be Relation of X; ::_thesis: ( R is_irreflexive_in X implies R is irreflexive ) A1: field R c= X \/ X by RELSET_1:8; assume R is_irreflexive_in X ; ::_thesis: R is irreflexive then for x being set st x in field R holds not [x,x] in R by A1, RELAT_2:def_2; then R is_irreflexive_in field R by RELAT_2:def_2; hence R is irreflexive by RELAT_2:def_10; ::_thesis: verum end; registration cluster empty Relation-like -> irreflexive asymmetric transitive for set ; coherence for b1 being Relation st b1 is empty holds ( b1 is irreflexive & b1 is asymmetric & b1 is transitive ) proof let R be Relation; ::_thesis: ( R is empty implies ( R is irreflexive & R is asymmetric & R is transitive ) ) assume A1: R is empty ; ::_thesis: ( R is irreflexive & R is asymmetric & R is transitive ) hence for x being set st x in field R holds not [x,x] in R ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( R is asymmetric & R is transitive ) thus for x, y being set st x in field R & y in field R & [x,y] in R holds not [y,x] in R by A1; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: R is transitive thus for x, y, z being set st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds [x,z] in R by A1; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: verum end; end; definition let f be Function; attrf is involutive means :Def2: :: PARTIT_2:def 2 for x being set st x in dom f holds f . (f . x) = x; end; :: deftheorem Def2 defines involutive PARTIT_2:def_2_:_ for f being Function holds ( f is involutive iff for x being set st x in dom f holds f . (f . x) = x ); definition let X be non empty set ; let f be UnOp of X; :: original: involutive redefine attrf is involutive means :: PARTIT_2:def 3 for x being Element of X holds f . (f . x) = x; compatibility ( f is involutive iff for x being Element of X holds f . (f . x) = x ) proof dom f = X by PARTFUN1:def_2; hence ( f is involutive implies for x being Element of X holds f . (f . x) = x ) by Def2; ::_thesis: ( ( for x being Element of X holds f . (f . x) = x ) implies f is involutive ) assume A1: for x being Element of X holds f . (f . x) = x ; ::_thesis: f is involutive let x be set ; :: according to PARTIT_2:def_2 ::_thesis: ( x in dom f implies f . (f . x) = x ) assume x in dom f ; ::_thesis: f . (f . x) = x hence f . (f . x) = x by A1; ::_thesis: verum end; end; :: deftheorem defines involutive PARTIT_2:def_3_:_ for X being non empty set for f being UnOp of X holds ( f is involutive iff for x being Element of X holds f . (f . x) = x ); registration cluster op1 -> involutive for Function; coherence for b1 being Function st b1 = op1 holds b1 is involutive proof op1 is () proof let a be Element of 1; :: according to PARTIT_2:def_3 ::_thesis: op1 . (op1 . a) = a a = {} by CARD_1:49, TARSKI:def_1; hence op1 . (op1 . a) = a by CARD_1:49, FUNCT_2:50; ::_thesis: verum end; hence for b1 being Function st b1 = op1 holds b1 is involutive ; ::_thesis: verum end; end; registration let X be set ; cluster id X -> involutive ; coherence id X is involutive proof set f = id X; let a be set ; :: according to PARTIT_2:def_2 ::_thesis: ( a in dom (id X) implies (id X) . ((id X) . a) = a ) assume a in dom (id X) ; ::_thesis: (id X) . ((id X) . a) = a then a in X ; then (id X) . a = a by FUNCT_1:17; hence (id X) . ((id X) . a) = a ; ::_thesis: verum end; end;