:: BVFUNC_2 semantic presentation begin definition let X be set ; :: original: PARTITIONS redefine func PARTITIONS X -> Part-Family of X; coherence PARTITIONS X is Part-Family of X proof A1: PARTITIONS X c= bool (bool X) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PARTITIONS X or x in bool (bool X) ) assume x in PARTITIONS X ; ::_thesis: x in bool (bool X) then x is a_partition of X by PARTIT1:def_3; hence x in bool (bool X) ; ::_thesis: verum end; for S being set st S in PARTITIONS X holds S is a_partition of X by PARTIT1:def_3; hence PARTITIONS X is Part-Family of X by A1, EQREL_1:def_7; ::_thesis: verum end; end; definition let X be set ; let F be non empty Part-Family of X; :: original: Element redefine mode Element of F -> a_partition of X; coherence for b1 being Element of F holds b1 is a_partition of X by EQREL_1:def_7; end; theorem Th1: :: BVFUNC_2:1 for Y being non empty set for G being Subset of (PARTITIONS Y) for y being Element of Y ex X being Subset of Y st ( y in X & ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & X = Intersect F & X <> {} ) ) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for y being Element of Y ex X being Subset of Y st ( y in X & ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & X = Intersect F & X <> {} ) ) let G be Subset of (PARTITIONS Y); ::_thesis: for y being Element of Y ex X being Subset of Y st ( y in X & ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & X = Intersect F & X <> {} ) ) let y be Element of Y; ::_thesis: ex X being Subset of Y st ( y in X & ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & X = Intersect F & X <> {} ) ) deffunc H1( Element of PARTITIONS Y) -> Element of \$1 = EqClass (y,\$1); defpred S1[ set ] means \$1 in G; consider h being PartFunc of (PARTITIONS Y),(bool Y) such that A1: for d being Element of PARTITIONS Y holds ( d in dom h iff S1[d] ) and A2: for d being Element of PARTITIONS Y st d in dom h holds h /. d = H1(d) from PARTFUN2:sch_2(); A3: G c= dom h proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G or x in dom h ) assume x in G ; ::_thesis: x in dom h hence x in dom h by A1; ::_thesis: verum end; A4: for d being set st d in G holds h . d in d proof let d be set ; ::_thesis: ( d in G implies h . d in d ) assume A5: d in G ; ::_thesis: h . d in d then reconsider d = d as a_partition of Y by PARTIT1:def_3; h /. d = h . d by A3, A5, PARTFUN1:def_6; then h . d = EqClass (y,d) by A2, A3, A5; hence h . d in d ; ::_thesis: verum end; dom h c= G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom h or x in G ) assume x in dom h ; ::_thesis: x in G hence x in G by A1; ::_thesis: verum end; then A6: dom h = G by A3, XBOOLE_0:def_10; reconsider rr = rng h as Subset-Family of Y ; A7: for d being Element of PARTITIONS Y st d in dom h holds y in h . d proof let d be Element of PARTITIONS Y; ::_thesis: ( d in dom h implies y in h . d ) assume A8: d in dom h ; ::_thesis: y in h . d then h /. d = EqClass (y,d) by A2; then h . d = EqClass (y,d) by A8, PARTFUN1:def_6; hence y in h . d by EQREL_1:def_6; ::_thesis: verum end; A9: for c being set st c in rng h holds y in c proof let c be set ; ::_thesis: ( c in rng h implies y in c ) assume c in rng h ; ::_thesis: y in c then ex a being set st ( a in dom h & c = h . a ) by FUNCT_1:def_3; hence y in c by A7; ::_thesis: verum end; percases ( rng h = {} or rng h <> {} ) ; suppose rng h = {} ; ::_thesis: ex X being Subset of Y st ( y in X & ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & X = Intersect F & X <> {} ) ) then Intersect rr = Y by SETFAM_1:def_9; hence ex X being Subset of Y st ( y in X & ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & X = Intersect F & X <> {} ) ) by A6, A4; ::_thesis: verum end; suppose rng h <> {} ; ::_thesis: ex X being Subset of Y st ( y in X & ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & X = Intersect F & X <> {} ) ) then ( y in meet (rng h) & Intersect rr = meet (rng h) ) by A9, SETFAM_1:def_1, SETFAM_1:def_9; hence ex X being Subset of Y st ( y in X & ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & X = Intersect F & X <> {} ) ) by A6, A4; ::_thesis: verum end; end; end; definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); func '/\' G -> a_partition of Y means :Def1: :: BVFUNC_2:def 1 for x being set holds ( x in it iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ); existence ex b1 being a_partition of Y st for x being set holds ( x in b1 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) proof defpred S1[ set ] means ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & \$1 = Intersect F & \$1 <> {} ); consider X being set such that A1: for x being set holds ( x in X iff ( x in bool Y & S1[x] ) ) from XBOOLE_0:sch_1(); A2: for A being Subset of Y st A in X holds ( A <> {} & ( for B being Subset of Y holds ( not B in X or A = B or A misses B ) ) ) proof let A be Subset of Y; ::_thesis: ( A in X implies ( A <> {} & ( for B being Subset of Y holds ( not B in X or A = B or A misses B ) ) ) ) assume A in X ; ::_thesis: ( A <> {} & ( for B being Subset of Y holds ( not B in X or A = B or A misses B ) ) ) then consider h1 being Function, F1 being Subset-Family of Y such that A3: dom h1 = G and A4: rng h1 = F1 and A5: for d being set st d in G holds h1 . d in d and A6: A = Intersect F1 and A7: A <> {} by A1; thus A <> {} by A7; ::_thesis: for B being Subset of Y holds ( not B in X or A = B or A misses B ) let B be Subset of Y; ::_thesis: ( not B in X or A = B or A misses B ) assume B in X ; ::_thesis: ( A = B or A misses B ) then consider h2 being Function, F2 being Subset-Family of Y such that A8: dom h2 = G and A9: rng h2 = F2 and A10: for d being set st d in G holds h2 . d in d and A11: B = Intersect F2 and B <> {} by A1; percases ( G = {} or G <> {} ) ; supposeA12: G = {} ; ::_thesis: ( A = B or A misses B ) then rng h1 = {} by A3, RELAT_1:42; hence ( A = B or A misses B ) by A4, A6, A8, A9, A11, A12, RELAT_1:42; ::_thesis: verum end; supposeA13: G <> {} ; ::_thesis: ( A = B or A misses B ) now__::_thesis:_(_not_A_meets_B_or_A_=_B_or_A_misses_B_) assume A meets B ; ::_thesis: ( A = B or A misses B ) then consider p being set such that A16: p in A and A17: p in B by XBOOLE_0:3; A18: p in meet (rng h2) by A9, A11, A13, A17, SETFAM_1:def_9, A8, RELAT_1:42; A19: p in meet (rng h1) by A4, A6, A3, A13, RELAT_1:42, A16, SETFAM_1:def_9; for g being set st g in G holds h1 . g = h2 . g proof let g be set ; ::_thesis: ( g in G implies h1 . g = h2 . g ) assume A20: g in G ; ::_thesis: h1 . g = h2 . g then reconsider g = g as a_partition of Y by PARTIT1:def_3; h1 . g in rng h1 by A3, A20, FUNCT_1:def_3; then A21: p in h1 . g by A19, SETFAM_1:def_1; h2 . g in rng h2 by A8, A20, FUNCT_1:def_3; then A22: p in h2 . g by A18, SETFAM_1:def_1; ( h1 . g in g & h2 . g in g ) by A5, A10, A20; hence h1 . g = h2 . g by A21, A22, XBOOLE_0:3, EQREL_1:def_4; ::_thesis: verum end; hence ( A = B or A misses B ) by A3, A4, A6, A8, A9, A11, FUNCT_1:2; ::_thesis: verum end; hence ( A = B or A misses B ) ; ::_thesis: verum end; end; end; A23: Y c= union X proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in union X ) assume y in Y ; ::_thesis: y in union X then reconsider y = y as Element of Y ; consider a being Subset of Y such that A24: y in a and A25: ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & a = Intersect F & a <> {} ) by Th1; a in X by A1, A25; hence y in union X by A24, TARSKI:def_4; ::_thesis: verum end; B28: union X c= Y proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union X or a in Y ) assume a in union X ; ::_thesis: a in Y then consider p being set such that A26: a in p and A27: p in X by TARSKI:def_4; ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & p = Intersect F & p <> {} ) by A1, A27; hence a in Y by A26; ::_thesis: verum end; take X ; ::_thesis: ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds ( x in X iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ) ) X c= bool Y proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in bool Y ) assume a in X ; ::_thesis: a in bool Y hence a in bool Y by A1; ::_thesis: verum end; then reconsider X = X as Subset-Family of Y ; X is a_partition of Y by B28, A2, EQREL_1:def_4, A23, XBOOLE_0:def_10; hence ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds ( x in X iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being a_partition of Y st ( for x being set holds ( x in b1 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ) & ( for x being set holds ( x in b2 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ) holds b1 = b2 proof let A1, A2 be a_partition of Y; ::_thesis: ( ( for x being set holds ( x in A1 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ) & ( for x being set holds ( x in A2 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ) implies A1 = A2 ) assume that A29: for x being set holds ( x in A1 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) and A30: for x being set holds ( x in A2 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ; ::_thesis: A1 = A2 now__::_thesis:_for_y_being_set_holds_ (_y_in_A1_iff_y_in_A2_) let y be set ; ::_thesis: ( y in A1 iff y in A2 ) ( y in A1 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & y = Intersect F & y <> {} ) ) by A29; hence ( y in A1 iff y in A2 ) by A30; ::_thesis: verum end; hence A1 = A2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def1 defines '/\' BVFUNC_2:def_1_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) for b3 being a_partition of Y holds ( b3 = '/\' G iff for x being set holds ( x in b3 iff ex h being Function ex F being Subset-Family of Y st ( dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) & x = Intersect F & x <> {} ) ) ); definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); let b be set ; predb is_upper_min_depend_of G means :Def2: :: BVFUNC_2:def 2 ( ( for d being a_partition of Y st d in G holds b is_a_dependent_set_of d ) & ( for e being set st e c= b & ( for d being a_partition of Y st d in G holds e is_a_dependent_set_of d ) holds e = b ) ); end; :: deftheorem Def2 defines is_upper_min_depend_of BVFUNC_2:def_2_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) for b being set holds ( b is_upper_min_depend_of G iff ( ( for d being a_partition of Y st d in G holds b is_a_dependent_set_of d ) & ( for e being set st e c= b & ( for d being a_partition of Y st d in G holds e is_a_dependent_set_of d ) holds e = b ) ) ); theorem Th2: :: BVFUNC_2:2 for Y being non empty set for G being Subset of (PARTITIONS Y) for y being Element of Y st G <> {} holds ex X being Subset of Y st ( y in X & X is_upper_min_depend_of G ) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for y being Element of Y st G <> {} holds ex X being Subset of Y st ( y in X & X is_upper_min_depend_of G ) let G be Subset of (PARTITIONS Y); ::_thesis: for y being Element of Y st G <> {} holds ex X being Subset of Y st ( y in X & X is_upper_min_depend_of G ) let y be Element of Y; ::_thesis: ( G <> {} implies ex X being Subset of Y st ( y in X & X is_upper_min_depend_of G ) ) defpred S1[ set ] means ( y in \$1 & ( for d being a_partition of Y st d in G holds \$1 is_a_dependent_set_of d ) ); reconsider XX = { X where X is Subset of Y : S1[X] } as Subset-Family of Y from DOMAIN_1:sch_7(); reconsider XX = XX as Subset-Family of Y ; assume G <> {} ; ::_thesis: ex X being Subset of Y st ( y in X & X is_upper_min_depend_of G ) then consider g being set such that A1: g in G by XBOOLE_0:def_1; reconsider g = g as a_partition of Y by A1, PARTIT1:def_3; A2: union g = Y by EQREL_1:def_4; take Intersect XX ; ::_thesis: ( y in Intersect XX & Intersect XX is_upper_min_depend_of G ) ( Y c= Y & ( for d being a_partition of Y st d in G holds Y is_a_dependent_set_of d ) ) by PARTIT1:7; then A3: Y in XX ; A4: for A being set st A in g holds ( A <> {} & ( for B being set holds ( not B in g or A = B or A misses B ) ) ) by EQREL_1:def_4; A5: for e being set st e c= Intersect XX & ( for d being a_partition of Y st d in G holds e is_a_dependent_set_of d ) holds e = Intersect XX proof let e be set ; ::_thesis: ( e c= Intersect XX & ( for d being a_partition of Y st d in G holds e is_a_dependent_set_of d ) implies e = Intersect XX ) assume that A6: e c= Intersect XX and A7: for d being a_partition of Y st d in G holds e is_a_dependent_set_of d ; ::_thesis: e = Intersect XX consider Ad being set such that A8: Ad c= g and A9: Ad <> {} and A10: e = union Ad by PARTIT1:def_1, A1, A7; A11: e c= Y by A2, A8, A10, ZFMISC_1:77; percases ( y in e or not y in e ) ; suppose y in e ; ::_thesis: e = Intersect XX then A12: e in XX by A7, A11; Intersect XX c= e proof let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in Intersect XX or X1 in e ) assume X1 in Intersect XX ; ::_thesis: X1 in e then X1 in meet XX by A3, SETFAM_1:def_9; hence X1 in e by A12, SETFAM_1:def_1; ::_thesis: verum end; hence e = Intersect XX by A6, XBOOLE_0:def_10; ::_thesis: verum end; supposeA13: not y in e ; ::_thesis: e = Intersect XX reconsider e = e as Subset of Y by A2, A8, A10, ZFMISC_1:77; e ` = Y \ e by SUBSET_1:def_4; then A14: y in e ` by A13, XBOOLE_0:def_5; e <> Y by A13; then for d being a_partition of Y st d in G holds e ` is_a_dependent_set_of d by A7, PARTIT1:10; then A15: e ` in XX by A14; A16: Intersect XX c= e ` proof let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in Intersect XX or X1 in e ` ) assume X1 in Intersect XX ; ::_thesis: X1 in e ` then X1 in meet XX by A3, SETFAM_1:def_9; hence X1 in e ` by A15, SETFAM_1:def_1; ::_thesis: verum end; A17: e /\ e = e ; consider ad being set such that A18: ad in Ad by A9, XBOOLE_0:def_1; e /\ (e `) = {} by XBOOLE_0:def_7, SUBSET_1:24; then e /\ (Intersect XX) = {} by A16, XBOOLE_1:3, XBOOLE_1:26; then e c= {} by A6, A17, XBOOLE_1:26; then union Ad = {} by A10; then A19: ad c= {} by A18, ZFMISC_1:74; ad <> {} by A4, A8, A18; hence e = Intersect XX by A19; ::_thesis: verum end; end; end; for X1 being set st X1 in XX holds y in X1 proof let X1 be set ; ::_thesis: ( X1 in XX implies y in X1 ) assume X1 in XX ; ::_thesis: y in X1 then ex X being Subset of Y st ( X = X1 & y in X & ( for d being a_partition of Y st d in G holds X is_a_dependent_set_of d ) ) ; hence y in X1 ; ::_thesis: verum end; then A20: y in meet XX by A3, SETFAM_1:def_1; then A21: Intersect XX <> {} by SETFAM_1:def_9; for d being a_partition of Y st d in G holds Intersect XX is_a_dependent_set_of d proof let d be a_partition of Y; ::_thesis: ( d in G implies Intersect XX is_a_dependent_set_of d ) assume A22: d in G ; ::_thesis: Intersect XX is_a_dependent_set_of d for X1 being set st X1 in XX holds X1 is_a_dependent_set_of d proof let X1 be set ; ::_thesis: ( X1 in XX implies X1 is_a_dependent_set_of d ) assume X1 in XX ; ::_thesis: X1 is_a_dependent_set_of d then ex X being Subset of Y st ( X = X1 & y in X & ( for d being a_partition of Y st d in G holds X is_a_dependent_set_of d ) ) ; hence X1 is_a_dependent_set_of d by A22; ::_thesis: verum end; hence Intersect XX is_a_dependent_set_of d by A21, PARTIT1:8; ::_thesis: verum end; hence ( y in Intersect XX & Intersect XX is_upper_min_depend_of G ) by A3, A20, A5, Def2, SETFAM_1:def_9; ::_thesis: verum end; definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); func '\/' G -> a_partition of Y means :Def3: :: BVFUNC_2:def 3 for x being set holds ( x in it iff x is_upper_min_depend_of G ) if G <> {} otherwise it = %I Y; existence ( ( G <> {} implies ex b1 being a_partition of Y st for x being set holds ( x in b1 iff x is_upper_min_depend_of G ) ) & ( not G <> {} implies ex b1 being a_partition of Y st b1 = %I Y ) ) proof thus ( G <> {} implies ex X being a_partition of Y st for x being set holds ( x in X iff x is_upper_min_depend_of G ) ) ::_thesis: ( not G <> {} implies ex b1 being a_partition of Y st b1 = %I Y ) proof defpred S1[ set ] means \$1 is_upper_min_depend_of G; consider X being set such that A1: for x being set holds ( x in X iff ( x in bool Y & S1[x] ) ) from XBOOLE_0:sch_1(); A2: union X c= Y proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union X or y in Y ) assume y in union X ; ::_thesis: y in Y then consider a being set such that A3: y in a and A4: a in X by TARSKI:def_4; a in bool Y by A1, A4; hence y in Y by A3; ::_thesis: verum end; assume A5: G <> {} ; ::_thesis: ex X being a_partition of Y st for x being set holds ( x in X iff x is_upper_min_depend_of G ) then consider g being set such that A6: g in G by XBOOLE_0:def_1; reconsider g = g as a_partition of Y by A6, PARTIT1:def_3; A7: union g = Y by EQREL_1:def_4; A8: for x being set holds ( x in X iff x is_upper_min_depend_of G ) proof let x be set ; ::_thesis: ( x in X iff x is_upper_min_depend_of G ) for x being set st x is_upper_min_depend_of G holds x in bool Y proof let x be set ; ::_thesis: ( x is_upper_min_depend_of G implies x in bool Y ) assume x is_upper_min_depend_of G ; ::_thesis: x in bool Y then ex A being set st ( A c= g & A <> {} & x = union A ) by PARTIT1:def_1, A6, Def2; then x c= union g by ZFMISC_1:77; hence x in bool Y by A7; ::_thesis: verum end; hence ( x in X iff x is_upper_min_depend_of G ) by A1; ::_thesis: verum end; B11: Y c= union X proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in union X ) assume y in Y ; ::_thesis: y in union X then reconsider y = y as Element of Y ; consider a being Subset of Y such that A9: y in a and A10: a is_upper_min_depend_of G by A5, Th2; a in X by A8, A10; hence y in union X by A9, TARSKI:def_4; ::_thesis: verum end; A12: for A being set st A in g holds ( A <> {} & ( for B being set holds ( not B in g or A = B or A misses B ) ) ) by EQREL_1:def_4; A13: for A being Subset of Y st A in X holds ( A <> {} & ( for B being Subset of Y holds ( not B in X or A = B or A misses B ) ) ) proof let A be Subset of Y; ::_thesis: ( A in X implies ( A <> {} & ( for B being Subset of Y holds ( not B in X or A = B or A misses B ) ) ) ) assume A in X ; ::_thesis: ( A <> {} & ( for B being Subset of Y holds ( not B in X or A = B or A misses B ) ) ) then A14: A is_upper_min_depend_of G by A8; then consider Aa being set such that A15: Aa c= g and A16: Aa <> {} and A17: A = union Aa by PARTIT1:def_1, A6, Def2; consider aa being set such that A18: aa in Aa by A16, XBOOLE_0:def_1; A19: aa c= union Aa by A18, ZFMISC_1:74; aa <> {} by A12, A15, A18; hence A <> {} by A17, A19; ::_thesis: for B being Subset of Y holds ( not B in X or A = B or A misses B ) let B be Subset of Y; ::_thesis: ( not B in X or A = B or A misses B ) assume B in X ; ::_thesis: ( A = B or A misses B ) then A20: B is_upper_min_depend_of G by A8; now__::_thesis:_(_A_meets_B_implies_A_=_B_) assume A21: A meets B ; ::_thesis: A = B A22: for d being a_partition of Y st d in G holds A /\ B is_a_dependent_set_of d proof let d be a_partition of Y; ::_thesis: ( d in G implies A /\ B is_a_dependent_set_of d ) assume d in G ; ::_thesis: A /\ B is_a_dependent_set_of d then ( A is_a_dependent_set_of d & B is_a_dependent_set_of d ) by A14, A20, Def2; hence A /\ B is_a_dependent_set_of d by A21, PARTIT1:9; ::_thesis: verum end; A23: A /\ B = B by A20, A22, Def2, XBOOLE_1:17; A24: B c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A ) assume x in B ; ::_thesis: x in A hence x in A by A23, XBOOLE_0:def_4; ::_thesis: verum end; A25: A /\ B = A by A14, A22, Def2, XBOOLE_1:17; A c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B ) assume x in A ; ::_thesis: x in B hence x in B by A25, XBOOLE_0:def_4; ::_thesis: verum end; hence A = B by A24, XBOOLE_0:def_10; ::_thesis: verum end; hence ( A = B or A misses B ) ; ::_thesis: verum end; take X ; ::_thesis: ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds ( x in X iff x is_upper_min_depend_of G ) ) ) X c= bool Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in bool Y ) assume x in X ; ::_thesis: x in bool Y hence x in bool Y by A1; ::_thesis: verum end; then reconsider X = X as Subset-Family of Y ; X is a_partition of Y by B11, A13, EQREL_1:def_4, A2, XBOOLE_0:def_10; hence ( X is Element of bool (bool Y) & X is a_partition of Y & ( for x being set holds ( x in X iff x is_upper_min_depend_of G ) ) ) by A8; ::_thesis: verum end; thus ( not G <> {} implies ex b1 being a_partition of Y st b1 = %I Y ) ; ::_thesis: verum end; uniqueness for b1, b2 being a_partition of Y holds ( ( G <> {} & ( for x being set holds ( x in b1 iff x is_upper_min_depend_of G ) ) & ( for x being set holds ( x in b2 iff x is_upper_min_depend_of G ) ) implies b1 = b2 ) & ( not G <> {} & b1 = %I Y & b2 = %I Y implies b1 = b2 ) ) proof let A1, A2 be a_partition of Y; ::_thesis: ( ( G <> {} & ( for x being set holds ( x in A1 iff x is_upper_min_depend_of G ) ) & ( for x being set holds ( x in A2 iff x is_upper_min_depend_of G ) ) implies A1 = A2 ) & ( not G <> {} & A1 = %I Y & A2 = %I Y implies A1 = A2 ) ) now__::_thesis:_(_G_<>_{}_&_(_for_x_being_set_holds_ (_x_in_A1_iff_x_is_upper_min_depend_of_G_)_)_&_(_for_x_being_set_holds_ (_x_in_A2_iff_x_is_upper_min_depend_of_G_)_)_implies_A1_=_A2_) assume that G <> {} and A26: for x being set holds ( x in A1 iff x is_upper_min_depend_of G ) and A27: for x being set holds ( x in A2 iff x is_upper_min_depend_of G ) ; ::_thesis: A1 = A2 for y being set holds ( y in A1 iff y in A2 ) by A27, A26; hence A1 = A2 by TARSKI:1; ::_thesis: verum end; hence ( ( G <> {} & ( for x being set holds ( x in A1 iff x is_upper_min_depend_of G ) ) & ( for x being set holds ( x in A2 iff x is_upper_min_depend_of G ) ) implies A1 = A2 ) & ( not G <> {} & A1 = %I Y & A2 = %I Y implies A1 = A2 ) ) ; ::_thesis: verum end; consistency for b1 being a_partition of Y holds verum ; end; :: deftheorem Def3 defines '\/' BVFUNC_2:def_3_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) for b3 being a_partition of Y holds ( ( G <> {} implies ( b3 = '\/' G iff for x being set holds ( x in b3 iff x is_upper_min_depend_of G ) ) ) & ( not G <> {} implies ( b3 = '\/' G iff b3 = %I Y ) ) ); theorem :: BVFUNC_2:3 for Y being non empty set for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st PA in G holds PA '>' '/\' G proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st PA in G holds PA '>' '/\' G let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st PA in G holds PA '>' '/\' G let PA be a_partition of Y; ::_thesis: ( PA in G implies PA '>' '/\' G ) assume A1: PA in G ; ::_thesis: PA '>' '/\' G for x being set st x in '/\' G holds ex a being set st ( a in PA & x c= a ) proof let x be set ; ::_thesis: ( x in '/\' G implies ex a being set st ( a in PA & x c= a ) ) assume x in '/\' G ; ::_thesis: ex a being set st ( a in PA & x c= a ) then consider h being Function, F being Subset-Family of Y such that A2: dom h = G and A3: rng h = F and A4: for d being set st d in G holds h . d in d and A5: x = Intersect F and x <> {} by Def1; set a = h . PA; A6: h . PA in PA by A1, A4; A7: h . PA in rng h by A1, A2, FUNCT_1:def_3; then Intersect F = meet F by A3, SETFAM_1:def_9; hence ex a being set st ( a in PA & x c= a ) by A3, A5, A6, A7, SETFAM_1:3; ::_thesis: verum end; hence PA '>' '/\' G by SETFAM_1:def_2; ::_thesis: verum end; theorem :: BVFUNC_2:4 for Y being non empty set for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st PA in G holds PA '<' '\/' G proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st PA in G holds PA '<' '\/' G let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st PA in G holds PA '<' '\/' G let PA be a_partition of Y; ::_thesis: ( PA in G implies PA '<' '\/' G ) assume A1: PA in G ; ::_thesis: PA '<' '\/' G for a being set st a in PA holds ex b being set st ( b in '\/' G & a c= b ) proof let a be set ; ::_thesis: ( a in PA implies ex b being set st ( b in '\/' G & a c= b ) ) set x = the Element of a; A2: union ('\/' G) = Y by EQREL_1:def_4; assume A3: a in PA ; ::_thesis: ex b being set st ( b in '\/' G & a c= b ) then A4: a <> {} by EQREL_1:def_4; then the Element of a in Y by A3, TARSKI:def_3; then consider b being set such that A5: the Element of a in b and A6: b in '\/' G by A2, TARSKI:def_4; b is_upper_min_depend_of G by A1, A6, Def3; then consider B being set such that A7: B c= PA and B <> {} and A8: b = union B by PARTIT1:def_1, A1, Def2; a in B proof consider u being set such that A9: the Element of a in u and A10: u in B by A5, A8, TARSKI:def_4; B11: a /\ u <> {} by A4, A9, XBOOLE_0:def_4; u in PA by A7, A10; hence a in B by A3, A10, B11, EQREL_1:def_4, XBOOLE_0:def_7; ::_thesis: verum end; hence ex b being set st ( b in '\/' G & a c= b ) by A6, A8, ZFMISC_1:74; ::_thesis: verum end; hence PA '<' '\/' G by SETFAM_1:def_2; ::_thesis: verum end; begin definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); attrG is generating means :: BVFUNC_2:def 4 '/\' G = %I Y; end; :: deftheorem defines generating BVFUNC_2:def_4_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) holds ( G is generating iff '/\' G = %I Y ); definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); attrG is independent means :: BVFUNC_2:def 5 for h being Function for F being Subset-Family of Y st dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) holds Intersect F <> {} ; end; :: deftheorem defines independent BVFUNC_2:def_5_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) holds ( G is independent iff for h being Function for F being Subset-Family of Y st dom h = G & rng h = F & ( for d being set st d in G holds h . d in d ) holds Intersect F <> {} ); definition let Y be non empty set ; let G be Subset of (PARTITIONS Y); predG is_a_coordinate means :: BVFUNC_2:def 6 ( G is independent & G is generating ); end; :: deftheorem defines is_a_coordinate BVFUNC_2:def_6_:_ for Y being non empty set for G being Subset of (PARTITIONS Y) holds ( G is_a_coordinate iff ( G is independent & G is generating ) ); definition let Y be non empty set ; let PA be a_partition of Y; :: original: { redefine func{PA} -> Subset of (PARTITIONS Y); coherence {PA} is Subset of (PARTITIONS Y) proof PA in PARTITIONS Y by PARTIT1:def_3; hence {PA} is Subset of (PARTITIONS Y) by ZFMISC_1:31; ::_thesis: verum end; end; definition let Y be non empty set ; let PA be a_partition of Y; let G be Subset of (PARTITIONS Y); func CompF (PA,G) -> a_partition of Y equals :: BVFUNC_2:def 7 '/\' (G \ {PA}); correctness coherence '/\' (G \ {PA}) is a_partition of Y; ; end; :: deftheorem defines CompF BVFUNC_2:def_7_:_ for Y being non empty set for PA being a_partition of Y for G being Subset of (PARTITIONS Y) holds CompF (PA,G) = '/\' (G \ {PA}); definition let Y be non empty set ; let a be Function of Y,BOOLEAN; let G be Subset of (PARTITIONS Y); let PA be a_partition of Y; preda is_independent_of PA,G means :Def8: :: BVFUNC_2:def 8 a is_dependent_of CompF (PA,G); end; :: deftheorem Def8 defines is_independent_of BVFUNC_2:def_8_:_ for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds ( a is_independent_of PA,G iff a is_dependent_of CompF (PA,G) ); definition let Y be non empty set ; let a be Function of Y,BOOLEAN; let G be Subset of (PARTITIONS Y); let PA be a_partition of Y; func All (a,PA,G) -> Function of Y,BOOLEAN equals :: BVFUNC_2:def 9 B_INF (a,(CompF (PA,G))); correctness coherence B_INF (a,(CompF (PA,G))) is Function of Y,BOOLEAN; ; end; :: deftheorem defines All BVFUNC_2:def_9_:_ for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All (a,PA,G) = B_INF (a,(CompF (PA,G))); definition let Y be non empty set ; let a be Function of Y,BOOLEAN; let G be Subset of (PARTITIONS Y); let PA be a_partition of Y; func Ex (a,PA,G) -> Function of Y,BOOLEAN equals :: BVFUNC_2:def 10 B_SUP (a,(CompF (PA,G))); correctness coherence B_SUP (a,(CompF (PA,G))) is Function of Y,BOOLEAN; ; end; :: deftheorem defines Ex BVFUNC_2:def_10_:_ for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds Ex (a,PA,G) = B_SUP (a,(CompF (PA,G))); theorem :: BVFUNC_2:5 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G) let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G) let PA be a_partition of Y; ::_thesis: All (a,PA,G) is_dependent_of CompF (PA,G) let F be set ; :: according to BVFUNC_1:def_15 ::_thesis: ( not F in CompF (PA,G) or for b1, b2 being set holds ( not b1 in F or not b2 in F or (All (a,PA,G)) . b1 = (All (a,PA,G)) . b2 ) ) assume A1: F in CompF (PA,G) ; ::_thesis: for b1, b2 being set holds ( not b1 in F or not b2 in F or (All (a,PA,G)) . b1 = (All (a,PA,G)) . b2 ) thus for x1, x2 being set st x1 in F & x2 in F holds (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 ::_thesis: verum proof let x1, x2 be set ; ::_thesis: ( x1 in F & x2 in F implies (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 ) assume A2: ( x1 in F & x2 in F ) ; ::_thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 then reconsider x1 = x1, x2 = x2 as Element of Y by A1; A3: x2 in EqClass (x2,(CompF (PA,G))) by EQREL_1:def_6; ( F = EqClass (x2,(CompF (PA,G))) or F misses EqClass (x2,(CompF (PA,G))) ) by A1, EQREL_1:def_4; then A4: EqClass (x1,(CompF (PA,G))) = EqClass (x2,(CompF (PA,G))) by A2, A3, EQREL_1:def_6, XBOOLE_0:3; percases ( ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds a . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) ) ; supposeA5: ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds a . x = TRUE ) ) ; ::_thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 then (All (a,PA,G)) . x2 = TRUE by BVFUNC_1:def_16; hence (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by A5, BVFUNC_1:def_16; ::_thesis: verum end; suppose ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) ; ::_thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 hence (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by A4; ::_thesis: verum end; suppose ( ex x being Element of Y st ( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds a . x = TRUE ) ) ; ::_thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 hence (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by A4; ::_thesis: verum end; supposeA6: ( ex x being Element of Y st ( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) ; ::_thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 then (All (a,PA,G)) . x2 = FALSE by BVFUNC_1:def_16; hence (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by A6, BVFUNC_1:def_16; ::_thesis: verum end; end; end; end; theorem :: BVFUNC_2:6 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex (a,PA,G) is_dependent_of CompF (PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex (a,PA,G) is_dependent_of CompF (PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex (a,PA,G) is_dependent_of CompF (PA,G) let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds Ex (a,PA,G) is_dependent_of CompF (PA,G) let PA be a_partition of Y; ::_thesis: Ex (a,PA,G) is_dependent_of CompF (PA,G) let F be set ; :: according to BVFUNC_1:def_15 ::_thesis: ( not F in CompF (PA,G) or for b1, b2 being set holds ( not b1 in F or not b2 in F or (Ex (a,PA,G)) . b1 = (Ex (a,PA,G)) . b2 ) ) assume A1: F in CompF (PA,G) ; ::_thesis: for b1, b2 being set holds ( not b1 in F or not b2 in F or (Ex (a,PA,G)) . b1 = (Ex (a,PA,G)) . b2 ) thus for x1, x2 being set st x1 in F & x2 in F holds (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 ::_thesis: verum proof let x1, x2 be set ; ::_thesis: ( x1 in F & x2 in F implies (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 ) assume A2: ( x1 in F & x2 in F ) ; ::_thesis: (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 then reconsider x1 = x1, x2 = x2 as Element of Y by A1; A3: x2 in EqClass (x2,(CompF (PA,G))) by EQREL_1:def_6; ( F = EqClass (x2,(CompF (PA,G))) or F misses EqClass (x2,(CompF (PA,G))) ) by A1, EQREL_1:def_4; then A4: EqClass (x1,(CompF (PA,G))) = EqClass (x2,(CompF (PA,G))) by A2, A3, EQREL_1:def_6, XBOOLE_0:3; percases ( ( ex x being Element of Y st ( x in EqClass (x1,(CompF (PA,G))) & a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (x2,(CompF (PA,G))) & a . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (x1,(CompF (PA,G))) & a . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (x2,(CompF (PA,G))) or not a . x = TRUE ) ) ) or ( ( for x being Element of Y holds ( not x in EqClass (x1,(CompF (PA,G))) or not a . x = TRUE ) ) & ex x being Element of Y st ( x in EqClass (x2,(CompF (PA,G))) & a . x = TRUE ) ) or ( ( for x being Element of Y holds ( not x in EqClass (x1,(CompF (PA,G))) or not a . x = TRUE ) ) & ( for x being Element of Y holds ( not x in EqClass (x2,(CompF (PA,G))) or not a . x = TRUE ) ) ) ) ; supposeA5: ( ex x being Element of Y st ( x in EqClass (x1,(CompF (PA,G))) & a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (x2,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 then (B_SUP (a,(CompF (PA,G)))) . x1 = TRUE by BVFUNC_1:def_17; hence (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A5, BVFUNC_1:def_17; ::_thesis: verum end; suppose ( ex x being Element of Y st ( x in EqClass (x1,(CompF (PA,G))) & a . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (x2,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 hence (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A4; ::_thesis: verum end; suppose ( ( for x being Element of Y holds ( not x in EqClass (x1,(CompF (PA,G))) or not a . x = TRUE ) ) & ex x being Element of Y st ( x in EqClass (x2,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 hence (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A4; ::_thesis: verum end; supposeA6: ( ( for x being Element of Y holds ( not x in EqClass (x1,(CompF (PA,G))) or not a . x = TRUE ) ) & ( for x being Element of Y holds ( not x in EqClass (x2,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 then (B_SUP (a,(CompF (PA,G)))) . x1 = FALSE by BVFUNC_1:def_17; hence (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A6, BVFUNC_1:def_17; ::_thesis: verum end; end; end; end; theorem :: BVFUNC_2:7 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((I_el Y),PA,G) = I_el Y proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((I_el Y),PA,G) = I_el Y let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((I_el Y),PA,G) = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((I_el Y),PA,G) = I_el Y let PA be a_partition of Y; ::_thesis: All ((I_el Y),PA,G) = I_el Y for z being Element of Y holds (All ((I_el Y),PA,G)) . z = TRUE proof let z be Element of Y; ::_thesis: (All ((I_el Y),PA,G)) . z = TRUE for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (I_el Y) . x = TRUE by BVFUNC_1:def_11; hence (All ((I_el Y),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum end; hence All ((I_el Y),PA,G) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_2:8 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex ((I_el Y),PA,G) = I_el Y proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex ((I_el Y),PA,G) = I_el Y let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex ((I_el Y),PA,G) = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds Ex ((I_el Y),PA,G) = I_el Y let PA be a_partition of Y; ::_thesis: Ex ((I_el Y),PA,G) = I_el Y for z being Element of Y holds (Ex ((I_el Y),PA,G)) . z = TRUE proof let z be Element of Y; ::_thesis: (Ex ((I_el Y),PA,G)) . z = TRUE ( z in EqClass (z,(CompF (PA,G))) & (I_el Y) . z = TRUE ) by BVFUNC_1:def_11, EQREL_1:def_6; hence (Ex ((I_el Y),PA,G)) . z = TRUE by BVFUNC_1:def_17; ::_thesis: verum end; hence Ex ((I_el Y),PA,G) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_2:9 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((O_el Y),PA,G) = O_el Y proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((O_el Y),PA,G) = O_el Y let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((O_el Y),PA,G) = O_el Y let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((O_el Y),PA,G) = O_el Y let PA be a_partition of Y; ::_thesis: All ((O_el Y),PA,G) = O_el Y for z being Element of Y holds (All ((O_el Y),PA,G)) . z = FALSE proof let z be Element of Y; ::_thesis: (All ((O_el Y),PA,G)) . z = FALSE ( z in EqClass (z,(CompF (PA,G))) & (O_el Y) . z = FALSE ) by BVFUNC_1:def_10, EQREL_1:def_6; hence (All ((O_el Y),PA,G)) . z = FALSE by BVFUNC_1:def_16; ::_thesis: verum end; hence All ((O_el Y),PA,G) = O_el Y by BVFUNC_1:def_10; ::_thesis: verum end; theorem :: BVFUNC_2:10 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex ((O_el Y),PA,G) = O_el Y proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex ((O_el Y),PA,G) = O_el Y let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN for PA being a_partition of Y holds Ex ((O_el Y),PA,G) = O_el Y let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds Ex ((O_el Y),PA,G) = O_el Y let PA be a_partition of Y; ::_thesis: Ex ((O_el Y),PA,G) = O_el Y for z being Element of Y holds (Ex ((O_el Y),PA,G)) . z = FALSE proof let z be Element of Y; ::_thesis: (Ex ((O_el Y),PA,G)) . z = FALSE for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (O_el Y) . x <> TRUE by BVFUNC_1:def_10; hence (Ex ((O_el Y),PA,G)) . z = FALSE by BVFUNC_1:def_17; ::_thesis: verum end; hence Ex ((O_el Y),PA,G) = O_el Y by BVFUNC_1:def_10; ::_thesis: verum end; theorem :: BVFUNC_2:11 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All (a,PA,G) '<' a proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All (a,PA,G) '<' a let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN for PA being a_partition of Y holds All (a,PA,G) '<' a let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All (a,PA,G) '<' a let PA be a_partition of Y; ::_thesis: All (a,PA,G) '<' a let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All (a,PA,G)) . z = TRUE or a . z = TRUE ) A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume (All (a,PA,G)) . z = TRUE ; ::_thesis: a . z = TRUE hence a . z = TRUE by A1, BVFUNC_1:def_16; ::_thesis: verum end; theorem :: BVFUNC_2:12 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds a '<' Ex (a,PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds a '<' Ex (a,PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN for PA being a_partition of Y holds a '<' Ex (a,PA,G) let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds a '<' Ex (a,PA,G) let PA be a_partition of Y; ::_thesis: a '<' Ex (a,PA,G) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not a . z = TRUE or (Ex (a,PA,G)) . z = TRUE ) A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume a . z = TRUE ; ::_thesis: (Ex (a,PA,G)) . z = TRUE hence (Ex (a,PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ::_thesis: verum end; theorem :: BVFUNC_2:13 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G) let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G) let PA be a_partition of Y; ::_thesis: (All (a,PA,G)) 'or' (All (b,PA,G)) '<' All ((a 'or' b),PA,G) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE or (All ((a 'or' b),PA,G)) . z = TRUE ) assume ((All (a,PA,G)) 'or' (All (b,PA,G))) . z = TRUE ; ::_thesis: (All ((a 'or' b),PA,G)) . z = TRUE then A1: ((All (a,PA,G)) . z) 'or' ((All (b,PA,G)) . z) = TRUE by BVFUNC_1:def_4; A2: ( (All (b,PA,G)) . z = TRUE or (All (b,PA,G)) . z = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_(All_(a,PA,G))_._z_=_TRUE_&_(All_((a_'or'_b),PA,G))_._z_=_TRUE_)_or_(_(All_(b,PA,G))_._z_=_TRUE_&_(All_((a_'or'_b),PA,G))_._z_=_TRUE_)_) percases ( (All (a,PA,G)) . z = TRUE or (All (b,PA,G)) . z = TRUE ) by A1, A2, BINARITH:3; caseA3: (All (a,PA,G)) . z = TRUE ; ::_thesis: (All ((a 'or' b),PA,G)) . z = TRUE for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (a 'or' b) . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'or' b) . x = TRUE ) assume A4: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'or' b) . x = TRUE (a 'or' b) . x = (a . x) 'or' (b . x) by BVFUNC_1:def_4 .= TRUE 'or' (b . x) by A3, A4, BVFUNC_1:def_16 .= TRUE by BINARITH:10 ; hence (a 'or' b) . x = TRUE ; ::_thesis: verum end; hence (All ((a 'or' b),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum end; caseA5: (All (b,PA,G)) . z = TRUE ; ::_thesis: (All ((a 'or' b),PA,G)) . z = TRUE for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (a 'or' b) . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'or' b) . x = TRUE ) assume A6: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'or' b) . x = TRUE (a 'or' b) . x = (a . x) 'or' (b . x) by BVFUNC_1:def_4 .= (a . x) 'or' TRUE by A5, A6, BVFUNC_1:def_16 .= TRUE by BINARITH:10 ; hence (a 'or' b) . x = TRUE ; ::_thesis: verum end; hence (All ((a 'or' b),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum end; end; end; hence (All ((a 'or' b),PA,G)) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC_2:14 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G)) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G)) let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G)) let PA be a_partition of Y; ::_thesis: All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (All (b,PA,G)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'imp' b),PA,G)) . z = TRUE or ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE ) assume A1: (All ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE A2: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' ((All (b,PA,G)) . z) by BVFUNC_1:def_8; percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds b . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds b . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ) ; suppose ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE then (B_INF (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16; then ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by BVFUNC_1:def_8 .= TRUE by BINARITH:10 ; hence ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE ; ::_thesis: verum end; supposeA3: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE then consider x1 being Element of Y such that A4: x1 in EqClass (z,(CompF (PA,G))) and A5: b . x1 <> TRUE ; A6: a . x1 = TRUE by A3, A4; (a 'imp' b) . x1 = ('not' (a . x1)) 'or' (b . x1) by BVFUNC_1:def_8 .= ('not' TRUE) 'or' FALSE by A5, A6, XBOOLEAN:def_3 .= FALSE 'or' FALSE by MARGREL1:11 .= FALSE ; hence ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE by A1, A4, BVFUNC_1:def_16; ::_thesis: verum end; suppose ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE then ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = ('not' ((All (a,PA,G)) . z)) 'or' TRUE by A2, BVFUNC_1:def_16 .= TRUE by BINARITH:10 ; hence ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE ; ::_thesis: verum end; suppose ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE then ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE 'or' ((All (b,PA,G)) . z) by MARGREL1:11, A2, BVFUNC_1:def_16 .= TRUE by BINARITH:10 ; hence ((All (a,PA,G)) 'imp' (All (b,PA,G))) . z = TRUE ; ::_thesis: verum end; end; end; theorem :: BVFUNC_2:15 for Y being non empty set for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,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 PA being a_partition of Y holds Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G)) let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y holds Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G)) let PA be a_partition of Y; ::_thesis: Ex ((a '&' b),PA,G) '<' (Ex (a,PA,G)) '&' (Ex (b,PA,G)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((a '&' b),PA,G)) . z = TRUE or ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = TRUE ) assume (Ex ((a '&' b),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = TRUE then consider x1 being Element of Y such that A1: x1 in EqClass (z,(CompF (PA,G))) and A2: (a '&' b) . x1 = TRUE by BVFUNC_1:def_17; A3: (a . x1) '&' (b . x1) = TRUE by A2, MARGREL1:def_20; then A4: b . x1 = TRUE by MARGREL1:12; a . x1 = TRUE by A3, MARGREL1:12; then A5: (Ex (a,PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = ((Ex (a,PA,G)) . z) '&' ((Ex (b,PA,G)) . z) by MARGREL1:def_20 .= TRUE '&' TRUE by A1, A4, A5, BVFUNC_1:def_17 .= TRUE ; hence ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC_2:16 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G) let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G) let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) 'xor' (Ex (b,PA,G)) '<' Ex ((a 'xor' b),PA,G) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) 'xor' (Ex (b,PA,G))) . z = TRUE or (Ex ((a 'xor' b),PA,G)) . z = TRUE ) A1: ((Ex (a,PA,G)) 'xor' (Ex (b,PA,G))) . z = ((Ex (a,PA,G)) . z) 'xor' ((Ex (b,PA,G)) . z) by BVFUNC_1:def_5 .= (('not' ((Ex (a,PA,G)) . z)) '&' ((Ex (b,PA,G)) . z)) 'or' (((Ex (a,PA,G)) . z) '&' ('not' ((Ex (b,PA,G)) . z))) ; A2: ( ('not' ((Ex (a,PA,G)) . z)) '&' ((Ex (b,PA,G)) . z) = TRUE or ('not' ((Ex (a,PA,G)) . z)) '&' ((Ex (b,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3; A3: 'not' FALSE = TRUE by MARGREL1:11; assume A4: ((Ex (a,PA,G)) 'xor' (Ex (b,PA,G))) . z = TRUE ; ::_thesis: (Ex ((a 'xor' b),PA,G)) . z = TRUE now__::_thesis:_(_(_('not'_((Ex_(a,PA,G))_._z))_'&'_((Ex_(b,PA,G))_._z)_=_TRUE_&_(Ex_((a_'xor'_b),PA,G))_._z_=_TRUE_)_or_(_((Ex_(a,PA,G))_._z)_'&'_('not'_((Ex_(b,PA,G))_._z))_=_TRUE_&_(Ex_((a_'xor'_b),PA,G))_._z_=_TRUE_)_) percases ( ('not' ((Ex (a,PA,G)) . z)) '&' ((Ex (b,PA,G)) . z) = TRUE or ((Ex (a,PA,G)) . z) '&' ('not' ((Ex (b,PA,G)) . z)) = TRUE ) by A4, A1, A2, BINARITH:3; caseA5: ('not' ((Ex (a,PA,G)) . z)) '&' ((Ex (b,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((a 'xor' b),PA,G)) . z = TRUE then (Ex (b,PA,G)) . z = TRUE by MARGREL1:12; then consider x1 being Element of Y such that A6: x1 in EqClass (z,(CompF (PA,G))) and A7: b . x1 = TRUE by BVFUNC_1:def_17; 'not' ((Ex (a,PA,G)) . z) = TRUE by A5, MARGREL1:12; then a . x1 <> TRUE by A6, BVFUNC_1:def_17, MARGREL1:11; then A8: a . x1 = FALSE by XBOOLEAN:def_3; (a 'xor' b) . x1 = (a . x1) 'xor' (b . x1) by BVFUNC_1:def_5 .= TRUE 'or' FALSE by A3, A7, A8 .= TRUE by BINARITH:10 ; hence (Ex ((a 'xor' b),PA,G)) . z = TRUE by A6, BVFUNC_1:def_17; ::_thesis: verum end; caseA9: ((Ex (a,PA,G)) . z) '&' ('not' ((Ex (b,PA,G)) . z)) = TRUE ; ::_thesis: (Ex ((a 'xor' b),PA,G)) . z = TRUE then (Ex (a,PA,G)) . z = TRUE by MARGREL1:12; then consider x1 being Element of Y such that A10: x1 in EqClass (z,(CompF (PA,G))) and A11: a . x1 = TRUE by BVFUNC_1:def_17; 'not' ((Ex (b,PA,G)) . z) = TRUE by A9, MARGREL1:12; then b . x1 <> TRUE by A10, BVFUNC_1:def_17, MARGREL1:11; then A12: b . x1 = FALSE by XBOOLEAN:def_3; (a 'xor' b) . x1 = (a . x1) 'xor' (b . x1) by BVFUNC_1:def_5 .= FALSE 'or' TRUE by A3, A11, A12 .= TRUE by BINARITH:10 ; hence (Ex ((a 'xor' b),PA,G)) . z = TRUE by A10, BVFUNC_1:def_17; ::_thesis: verum end; end; end; hence (Ex ((a 'xor' b),PA,G)) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC_2:17 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for a, b being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G) let a, b be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G) let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' Ex ((a 'imp' b),PA,G) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE or (Ex ((a 'imp' b),PA,G)) . z = TRUE ) A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) . z = TRUE ; ::_thesis: (Ex ((a 'imp' b),PA,G)) . z = TRUE then A2: ('not' ((Ex (a,PA,G)) . z)) 'or' ((Ex (b,PA,G)) . z) = TRUE by BVFUNC_1:def_8; A3: ( 'not' ((Ex (a,PA,G)) . z) = TRUE or 'not' ((Ex (a,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_((Ex_(a,PA,G))_._z)_=_TRUE_&_(Ex_((a_'imp'_b),PA,G))_._z_=_TRUE_)_or_(_(Ex_(b,PA,G))_._z_=_TRUE_&_(Ex_((a_'imp'_b),PA,G))_._z_=_TRUE_)_) percases ( 'not' ((Ex (a,PA,G)) . z) = TRUE or (Ex (b,PA,G)) . z = TRUE ) by A2, A3, BINARITH:3; case 'not' ((Ex (a,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((a 'imp' b),PA,G)) . z = TRUE then A4: a . z <> TRUE by A1, BVFUNC_1:def_17, MARGREL1:11; (a 'imp' b) . z = ('not' (a . z)) 'or' (b . z) by BVFUNC_1:def_8 .= TRUE 'or' (b . z) by MARGREL1:11, A4, XBOOLEAN:def_3 .= TRUE by BINARITH:10 ; hence (Ex ((a 'imp' b),PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ::_thesis: verum end; case (Ex (b,PA,G)) . z = TRUE ; ::_thesis: (Ex ((a 'imp' b),PA,G)) . z = TRUE then consider x1 being Element of Y such that A5: x1 in EqClass (z,(CompF (PA,G))) and A6: b . x1 = TRUE by BVFUNC_1:def_17; (a 'imp' b) . x1 = ('not' (a . x1)) 'or' (b . x1) by BVFUNC_1:def_8 .= TRUE by A6, BINARITH:10 ; hence (Ex ((a 'imp' b),PA,G)) . z = TRUE by A5, BVFUNC_1:def_17; ::_thesis: verum end; end; end; hence (Ex ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC_2:18 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds 'not' (All (a,PA,G)) = Ex (('not' a),PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds 'not' (All (a,PA,G)) = Ex (('not' a),PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN for PA being a_partition of Y holds 'not' (All (a,PA,G)) = Ex (('not' a),PA,G) let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds 'not' (All (a,PA,G)) = Ex (('not' a),PA,G) let PA be a_partition of Y; ::_thesis: 'not' (All (a,PA,G)) = Ex (('not' a),PA,G) let z be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & ('not' a) . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not ('not' a) . x = TRUE ) ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & ('not' a) . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not ('not' a) . x = TRUE ) ) ) ) ; supposeA5: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & ('not' a) . x = TRUE ) ) ; ::_thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z then consider x1 being Element of Y such that A6: x1 in EqClass (z,(CompF (PA,G))) and A7: ('not' a) . x1 = TRUE ; 'not' (a . x1) = TRUE by A7, MARGREL1:def_19; hence ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z by A5, A6, MARGREL1:11; ::_thesis: verum end; supposeA8: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not ('not' a) . x = TRUE ) ) ) ; ::_thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z then (B_INF (a,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16; then A9: ('not' (B_INF (a,(CompF (PA,G))))) . z = 'not' TRUE by MARGREL1:def_19; (B_SUP (('not' a),(CompF (PA,G)))) . z = FALSE by A8, BVFUNC_1:def_17; hence ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z by A9, MARGREL1:11; ::_thesis: verum end; supposeA10: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & ('not' a) . x = TRUE ) ) ; ::_thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z then (B_INF (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16; then A11: ('not' (B_INF (a,(CompF (PA,G))))) . z = 'not' FALSE by MARGREL1:def_19; (B_SUP (('not' a),(CompF (PA,G)))) . z = TRUE by A10, BVFUNC_1:def_17; hence ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z by A11, MARGREL1:11; ::_thesis: verum end; supposeA12: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not ('not' a) . x = TRUE ) ) ) ; ::_thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z then consider x1 being Element of Y such that A13: x1 in EqClass (z,(CompF (PA,G))) and A14: a . x1 <> TRUE ; ('not' a) . x1 <> TRUE by A12, A13; then 'not' (a . x1) <> TRUE by MARGREL1:def_19; hence ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z by A14, MARGREL1:11, XBOOLEAN:def_3; ::_thesis: verum end; end; end; theorem :: BVFUNC_2:19 for Y being non empty set for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a being Function of Y,BOOLEAN for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for a being Function of Y,BOOLEAN for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G) let a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G) let PA be a_partition of Y; ::_thesis: 'not' (Ex (a,PA,G)) = All (('not' a),PA,G) let z be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds ('not' a) . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds ('not' a) . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ) ; supposeA5: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds ('not' a) . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z then consider x1 being Element of Y such that A6: x1 in EqClass (z,(CompF (PA,G))) and A7: a . x1 = TRUE ; ('not' a) . x1 = 'not' TRUE by A7, MARGREL1:def_19; hence ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z by A5, A6, MARGREL1:11; ::_thesis: verum end; supposeA8: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds ('not' a) . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z then 'not' ((B_SUP (a,(CompF (PA,G)))) . z) = TRUE by MARGREL1:11, BVFUNC_1:def_17; then ('not' (B_SUP (a,(CompF (PA,G))))) . z = TRUE by MARGREL1:def_19; hence ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z by A8, BVFUNC_1:def_16; ::_thesis: verum end; supposeA9: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z then (B_SUP (a,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_17; then A10: ('not' (B_SUP (a,(CompF (PA,G))))) . z = 'not' TRUE by MARGREL1:def_19; (B_INF (('not' a),(CompF (PA,G)))) . z = FALSE by A9, BVFUNC_1:def_16; hence ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z by A10, MARGREL1:11; ::_thesis: verum end; supposeA11: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z then consider x1 being Element of Y such that A12: x1 in EqClass (z,(CompF (PA,G))) and A13: ('not' a) . x1 <> TRUE ; ('not' a) . x1 = FALSE by A13, XBOOLEAN:def_3; then 'not' (a . x1) = FALSE by MARGREL1:def_19; hence ('not' (Ex (a,PA,G))) . z = (All (('not' a),PA,G)) . z by A11, A12, MARGREL1:11; ::_thesis: verum end; end; end; theorem :: BVFUNC_2:20 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G)) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G)) let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G)) let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G)) ) assume Z: u is_independent_of PA,G ; ::_thesis: All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G)) A2: u 'imp' (All (a,PA,G)) '<' All ((u 'imp' a),PA,G) proof let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u 'imp' (All (a,PA,G))) . z = TRUE or (All ((u 'imp' a),PA,G)) . z = TRUE ) assume (u 'imp' (All (a,PA,G))) . z = TRUE ; ::_thesis: (All ((u 'imp' a),PA,G)) . z = TRUE then A3: ('not' (u . z)) 'or' ((All (a,PA,G)) . z) = TRUE by BVFUNC_1:def_8; A4: ( (All (a,PA,G)) . z = TRUE or (All (a,PA,G)) . z = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(All_((u_'imp'_a),PA,G))_._z_=_TRUE percases ( (All (a,PA,G)) . z = TRUE or ( (All (a,PA,G)) . z <> TRUE & 'not' (u . z) = TRUE ) ) by A3, A4, BINARITH:3; supposeA5: (All (a,PA,G)) . z = TRUE ; ::_thesis: (All ((u 'imp' a),PA,G)) . z = TRUE for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (u 'imp' a) . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u 'imp' a) . x = TRUE ) assume A6: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (u 'imp' a) . x = TRUE (u 'imp' a) . x = ('not' (u . x)) 'or' (a . x) by BVFUNC_1:def_8 .= ('not' (u . x)) 'or' TRUE by A5, A6, BVFUNC_1:def_16 .= TRUE by BINARITH:10 ; hence (u 'imp' a) . x = TRUE ; ::_thesis: verum end; hence (All ((u 'imp' a),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum end; supposeA7: ( (All (a,PA,G)) . z <> TRUE & 'not' (u . z) = TRUE ) ; ::_thesis: (All ((u 'imp' a),PA,G)) . z = TRUE A8: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (u 'imp' a) . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u 'imp' a) . x = TRUE ) assume x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (u 'imp' a) . x = TRUE then ( (u 'imp' a) . x = ('not' (u . x)) 'or' (a . x) & u . x = u . z ) by Z, Def8, A8, BVFUNC_1:def_8, BVFUNC_1:def_15; hence (u 'imp' a) . x = TRUE by A7, BINARITH:10; ::_thesis: verum end; hence (All ((u 'imp' a),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum end; end; end; hence (All ((u 'imp' a),PA,G)) . z = TRUE ; ::_thesis: verum end; All ((u 'imp' a),PA,G) '<' u 'imp' (All (a,PA,G)) proof let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((u 'imp' a),PA,G)) . z = TRUE or (u 'imp' (All (a,PA,G))) . z = TRUE ) assume A9: (All ((u 'imp' a),PA,G)) . z = TRUE ; ::_thesis: (u 'imp' (All (a,PA,G))) . z = TRUE A11: (u 'imp' (All (a,PA,G))) . z = ('not' (u . z)) 'or' ((All (a,PA,G)) . z) by BVFUNC_1:def_8; percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds 'not' (u . x) = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not 'not' (u . x) = TRUE ) ) ) ; suppose for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ; ::_thesis: (u 'imp' (All (a,PA,G))) . z = TRUE then (All (a,PA,G)) . z = TRUE by BVFUNC_1:def_16; hence (u 'imp' (All (a,PA,G))) . z = TRUE by A11, BINARITH:10; ::_thesis: verum end; suppose ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds 'not' (u . x) = TRUE ) ) ; ::_thesis: (u 'imp' (All (a,PA,G))) . z = TRUE then 'not' (u . z) = TRUE by EQREL_1:def_6; hence (u 'imp' (All (a,PA,G))) . z = TRUE by A11, BINARITH:10; ::_thesis: verum end; supposeA12: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not 'not' (u . x) = TRUE ) ) ; ::_thesis: (u 'imp' (All (a,PA,G))) . z = TRUE then consider x1 being Element of Y such that A13: x1 in EqClass (z,(CompF (PA,G))) and A14: 'not' (u . x1) <> TRUE ; consider x2 being Element of Y such that A15: x2 in EqClass (z,(CompF (PA,G))) and A16: a . x2 <> TRUE by A12; u . x1 = u . x2 by Z, Def8, A13, A15, BVFUNC_1:def_15; then A17: u . x2 = TRUE by MARGREL1:11, A14, XBOOLEAN:def_3; a . x2 = FALSE by A16, XBOOLEAN:def_3; then (u 'imp' a) . x2 = ('not' TRUE) 'or' FALSE by A17, BVFUNC_1:def_8; then (u 'imp' a) . x2 = FALSE 'or' FALSE by MARGREL1:11 .= FALSE ; hence (u 'imp' (All (a,PA,G))) . z = TRUE by A9, A15, BVFUNC_1:def_16; ::_thesis: verum end; end; end; hence All ((u 'imp' a),PA,G) = u 'imp' (All (a,PA,G)) by A2, BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC_2:21 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u ) assume Z: u is_independent_of PA,G ; ::_thesis: All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u A2: (Ex (a,PA,G)) 'imp' u '<' All ((a 'imp' u),PA,G) proof let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) 'imp' u) . z = TRUE or (All ((a 'imp' u),PA,G)) . z = TRUE ) A3: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume ((Ex (a,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: (All ((a 'imp' u),PA,G)) . z = TRUE then A4: ('not' ((Ex (a,PA,G)) . z)) 'or' (u . z) = TRUE by BVFUNC_1:def_8; A5: ( 'not' ((Ex (a,PA,G)) . z) = TRUE or 'not' ((Ex (a,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_u_._z_=_TRUE_&_(All_((a_'imp'_u),PA,G))_._z_=_TRUE_)_or_(_'not'_((Ex_(a,PA,G))_._z)_=_TRUE_&_u_._z_=_FALSE_&_(All_((a_'imp'_u),PA,G))_._z_=_TRUE_)_) percases ( u . z = TRUE or ( 'not' ((Ex (a,PA,G)) . z) = TRUE & u . z = FALSE ) ) by A4, A5, BINARITH:3, XBOOLEAN:def_3; caseA6: u . z = TRUE ; ::_thesis: (All ((a 'imp' u),PA,G)) . z = TRUE for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (a 'imp' u) . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' u) . x = TRUE ) assume x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' u) . x = TRUE then ( (a 'imp' u) . x = ('not' (a . x)) 'or' (u . x) & u . x = u . z ) by Z, Def8, A3, BVFUNC_1:def_8, BVFUNC_1:def_15; hence (a 'imp' u) . x = TRUE by A6, BINARITH:10; ::_thesis: verum end; hence (All ((a 'imp' u),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum end; caseC: ( 'not' ((Ex (a,PA,G)) . z) = TRUE & u . z = FALSE ) ; ::_thesis: (All ((a 'imp' u),PA,G)) . z = TRUE for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (a 'imp' u) . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (a 'imp' u) . x = TRUE ) assume x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (a 'imp' u) . x = TRUE then a . x <> TRUE by C, BVFUNC_1:def_17, MARGREL1:11; then ( (a 'imp' u) . x = ('not' (a . x)) 'or' (u . x) & a . x = FALSE ) by BVFUNC_1:def_8, XBOOLEAN:def_3; then (a 'imp' u) . x = TRUE 'or' (u . x) by MARGREL1:11 .= TRUE by BINARITH:10 ; hence (a 'imp' u) . x = TRUE ; ::_thesis: verum end; hence (All ((a 'imp' u),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum end; end; end; hence (All ((a 'imp' u),PA,G)) . z = TRUE ; ::_thesis: verum end; All ((a 'imp' u),PA,G) '<' (Ex (a,PA,G)) 'imp' u proof let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'imp' u),PA,G)) . z = TRUE or ((Ex (a,PA,G)) 'imp' u) . z = TRUE ) assume A8: (All ((a 'imp' u),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'imp' u) . z = TRUE A10: ((Ex (a,PA,G)) 'imp' u) . z = ('not' ((Ex (a,PA,G)) . z)) 'or' (u . z) by BVFUNC_1:def_8; percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ) ; suppose for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'imp' u) . z = TRUE then ((Ex (a,PA,G)) 'imp' u) . z = ('not' ((Ex (a,PA,G)) . z)) 'or' TRUE by EQREL_1:def_6, A10 .= TRUE by BINARITH:10 ; hence ((Ex (a,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: verum end; supposeA11: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: ((Ex (a,PA,G)) 'imp' u) . z = TRUE then consider x1 being Element of Y such that A12: x1 in EqClass (z,(CompF (PA,G))) and A13: u . x1 <> TRUE ; consider x2 being Element of Y such that A14: x2 in EqClass (z,(CompF (PA,G))) and A15: a . x2 = TRUE by A11; A16: u . x1 = u . x2 by Z, Def8, A12, A14, BVFUNC_1:def_15; (a 'imp' u) . x2 = ('not' (a . x2)) 'or' (u . x2) by BVFUNC_1:def_8 .= ('not' TRUE) 'or' FALSE by A13, A15, A16, XBOOLEAN:def_3 .= FALSE 'or' FALSE by MARGREL1:11 .= FALSE ; hence ((Ex (a,PA,G)) 'imp' u) . z = TRUE by A8, A14, BVFUNC_1:def_16; ::_thesis: verum end; suppose ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: ((Ex (a,PA,G)) 'imp' u) . z = TRUE then ((Ex (a,PA,G)) 'imp' u) . z = ('not' FALSE) 'or' (u . z) by A10, BVFUNC_1:def_17 .= TRUE 'or' (u . z) by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ((Ex (a,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: verum end; end; end; hence All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u by A2, BVFUNC_1:15; ::_thesis: verum end; theorem Th22: :: BVFUNC_2:22 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G)) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G)) let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G)) let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G)) ) assume Z: u is_independent_of PA,G ; ::_thesis: All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G)) let z be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z A6: (u 'or' (B_INF (a,(CompF (PA,G))))) . z = (u . z) 'or' ((B_INF (a,(CompF (PA,G)))) . z) by BVFUNC_1:def_4; percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ) ) ; supposeA7: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ; ::_thesis: (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z A8: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (u 'or' a) . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u 'or' a) . x = TRUE ) assume A9: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (u 'or' a) . x = TRUE (u 'or' a) . x = (u . x) 'or' (a . x) by BVFUNC_1:def_4 .= (u . x) 'or' TRUE by A7, A9 .= TRUE by BINARITH:10 ; hence (u 'or' a) . x = TRUE ; ::_thesis: verum end; (B_INF (a,(CompF (PA,G)))) . z = TRUE by A7, BVFUNC_1:def_16; then (u 'or' (B_INF (a,(CompF (PA,G))))) . z = TRUE by A6, BINARITH:10; hence (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z by A8, BVFUNC_1:def_16; ::_thesis: verum end; supposeA10: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ) ) ; ::_thesis: (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z A11: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (u 'or' a) . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u 'or' a) . x = TRUE ) assume A12: x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (u 'or' a) . x = TRUE (u 'or' a) . x = (u . x) 'or' (a . x) by BVFUNC_1:def_4 .= TRUE 'or' (a . x) by A10, A12 .= TRUE by BINARITH:10 ; hence (u 'or' a) . x = TRUE ; ::_thesis: verum end; (u 'or' (B_INF (a,(CompF (PA,G))))) . z = TRUE 'or' ((B_INF (a,(CompF (PA,G)))) . z) by A6, A10, EQREL_1:def_6; then (u 'or' (B_INF (a,(CompF (PA,G))))) . z = TRUE by BINARITH:10; hence (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z by A11, BVFUNC_1:def_16; ::_thesis: verum end; supposeA13: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ) ; ::_thesis: (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z then consider x2 being Element of Y such that A14: x2 in EqClass (z,(CompF (PA,G))) and A15: u . x2 <> TRUE ; consider x1 being Element of Y such that A16: x1 in EqClass (z,(CompF (PA,G))) and A17: a . x1 <> TRUE by A13; u . x1 = u . x2 by Z, Def8, A16, A14, BVFUNC_1:def_15; then A18: u . x1 = FALSE by A15, XBOOLEAN:def_3; A19: (B_INF (a,(CompF (PA,G)))) . z = FALSE by A13, BVFUNC_1:def_16; z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; then A20: u . x1 = u . z by Z, Def8, A16, BVFUNC_1:def_15; a . x1 = FALSE by A17, XBOOLEAN:def_3; then (u 'or' a) . x1 = FALSE 'or' FALSE by A18, BVFUNC_1:def_4; hence (All ((u 'or' a),PA,G)) . z = (u 'or' (All (a,PA,G))) . z by A6, A19, A16, A18, A20, BVFUNC_1:def_16; ::_thesis: verum end; end; end; theorem :: BVFUNC_2:23 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'or' u),PA,G) = (All (a,PA,G)) 'or' u by Th22; theorem :: BVFUNC_2:24 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u ) assume Z: u is_independent_of PA,G ; ::_thesis: All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'or' u),PA,G)) . z = TRUE or ((Ex (a,PA,G)) 'or' u) . z = TRUE ) assume A3: (All ((a 'or' u),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' u) . z = TRUE A4: for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or a . x = TRUE or u . x = TRUE ) proof let x be Element of Y; ::_thesis: ( not x in EqClass (z,(CompF (PA,G))) or a . x = TRUE or u . x = TRUE ) assume x in EqClass (z,(CompF (PA,G))) ; ::_thesis: ( a . x = TRUE or u . x = TRUE ) then (a 'or' u) . x = TRUE by A3, BVFUNC_1:def_16; then A5: (a . x) 'or' (u . x) = TRUE by BVFUNC_1:def_4; ( u . x = TRUE or u . x = FALSE ) by XBOOLEAN:def_3; hence ( a . x = TRUE or u . x = TRUE ) by A5, BINARITH:3; ::_thesis: verum end; A6: ((Ex (a,PA,G)) 'or' u) . z = ((Ex (a,PA,G)) . z) 'or' (u . z) by BVFUNC_1:def_4; percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ) ; suppose for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ; ::_thesis: ((Ex (a,PA,G)) 'or' u) . z = TRUE then ((Ex (a,PA,G)) 'or' u) . z = ((Ex (a,PA,G)) . z) 'or' TRUE by EQREL_1:def_6, A6 .= TRUE by BINARITH:10 ; hence ((Ex (a,PA,G)) 'or' u) . z = TRUE ; ::_thesis: verum end; suppose ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) ; ::_thesis: ((Ex (a,PA,G)) 'or' u) . z = TRUE then ((Ex (a,PA,G)) 'or' u) . z = TRUE 'or' (u . z) by A6, BVFUNC_1:def_17 .= TRUE by BINARITH:10 ; hence ((Ex (a,PA,G)) 'or' u) . z = TRUE ; ::_thesis: verum end; supposeA7: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; ::_thesis: ((Ex (a,PA,G)) 'or' u) . z = TRUE A8: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; A9: a . z <> TRUE by A7, EQREL_1:def_6; consider x1 being Element of Y such that A10: x1 in EqClass (z,(CompF (PA,G))) and A11: u . x1 <> TRUE by A7; u . x1 = u . z by Z, Def8, A8, A10, BVFUNC_1:def_15; hence ((Ex (a,PA,G)) 'or' u) . z = TRUE by A4, EQREL_1:def_6, A9, A11; ::_thesis: verum end; end; end; theorem Th25: :: BVFUNC_2:25 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) ) A1: All ((u '&' a),PA,G) '<' u '&' (All (a,PA,G)) proof let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((u '&' a),PA,G)) . z = TRUE or (u '&' (All (a,PA,G))) . z = TRUE ) assume A2: (All ((u '&' a),PA,G)) . z = TRUE ; ::_thesis: (u '&' (All (a,PA,G))) . z = TRUE A3: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies u . x = TRUE ) assume x in EqClass (z,(CompF (PA,G))) ; ::_thesis: u . x = TRUE then A4: (u '&' a) . x = TRUE by A2, BVFUNC_1:def_16; (u '&' a) . x = (u . x) '&' (a . x) by MARGREL1:def_20; hence u . x = TRUE by A4, MARGREL1:12; ::_thesis: verum end; for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies a . x = TRUE ) assume x in EqClass (z,(CompF (PA,G))) ; ::_thesis: a . x = TRUE then A5: (u '&' a) . x = TRUE by A2, BVFUNC_1:def_16; (u '&' a) . x = (u . x) '&' (a . x) by MARGREL1:def_20; hence a . x = TRUE by A5, MARGREL1:12; ::_thesis: verum end; then A6: ( (u '&' (All (a,PA,G))) . z = (u . z) '&' ((All (a,PA,G)) . z) & (All (a,PA,G)) . z = TRUE ) by BVFUNC_1:def_16, MARGREL1:def_20; u . z = TRUE by A3, EQREL_1:def_6; hence (u '&' (All (a,PA,G))) . z = TRUE by A6; ::_thesis: verum end; assume Z: u is_independent_of PA,G ; ::_thesis: All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) u '&' (All (a,PA,G)) '<' All ((u '&' a),PA,G) proof let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u '&' (All (a,PA,G))) . z = TRUE or (All ((u '&' a),PA,G)) . z = TRUE ) A8: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume (u '&' (All (a,PA,G))) . z = TRUE ; ::_thesis: (All ((u '&' a),PA,G)) . z = TRUE then A9: (u . z) '&' ((All (a,PA,G)) . z) = TRUE by MARGREL1:def_20; then A10: (All (a,PA,G)) . z = TRUE by MARGREL1:12; A11: u . z = TRUE by A9, MARGREL1:12; for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds (u '&' a) . x = TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u '&' a) . x = TRUE ) assume x in EqClass (z,(CompF (PA,G))) ; ::_thesis: (u '&' a) . x = TRUE then ( a . x = TRUE & u . x = u . z ) by Z, Def8, A10, A8, BVFUNC_1:def_15, BVFUNC_1:def_16; then (u '&' a) . x = TRUE '&' TRUE by A11, MARGREL1:def_20 .= TRUE ; hence (u '&' a) . x = TRUE ; ::_thesis: verum end; hence (All ((u '&' a),PA,G)) . z = TRUE by BVFUNC_1:def_16; ::_thesis: verum end; hence All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) by A1, BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC_2:26 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a '&' u),PA,G) = (All (a,PA,G)) '&' u by Th25; theorem :: BVFUNC_2:27 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, u being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a, u being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u let G be Subset of (PARTITIONS Y); ::_thesis: for a, u being Function of Y,BOOLEAN for PA being a_partition of Y holds All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u let a, u be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u let PA be a_partition of Y; ::_thesis: All ((a '&' u),PA,G) '<' (Ex (a,PA,G)) '&' u let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a '&' u),PA,G)) . z = TRUE or ((Ex (a,PA,G)) '&' u) . z = TRUE ) A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume A2: (All ((a '&' u),PA,G)) . z = TRUE ; ::_thesis: ((Ex (a,PA,G)) '&' u) . z = TRUE A3: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds ( a . x = TRUE & u . x = TRUE ) proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (PA,G))) implies ( a . x = TRUE & u . x = TRUE ) ) assume x in EqClass (z,(CompF (PA,G))) ; ::_thesis: ( a . x = TRUE & u . x = TRUE ) then (a '&' u) . x = TRUE by A2, BVFUNC_1:def_16; then (a . x) '&' (u . x) = TRUE by MARGREL1:def_20; hence ( a . x = TRUE & u . x = TRUE ) by MARGREL1:12; ::_thesis: verum end; A4: ((Ex (a,PA,G)) '&' u) . z = ((Ex (a,PA,G)) . z) '&' (u . z) by MARGREL1:def_20; percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE or ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ) ; supposeA5: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ; ::_thesis: ((Ex (a,PA,G)) '&' u) . z = TRUE now__::_thesis:_((Ex_(a,PA,G))_'&'_u)_._z_=_TRUE percases ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) or for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ; suppose ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ; ::_thesis: ((Ex (a,PA,G)) '&' u) . z = TRUE then (Ex (a,PA,G)) . z = TRUE by BVFUNC_1:def_17; hence ((Ex (a,PA,G)) '&' u) . z = TRUE '&' TRUE by EQREL_1:def_6, A4, A5 .= TRUE ; ::_thesis: verum end; suppose for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ; ::_thesis: ((Ex (a,PA,G)) '&' u) . z = TRUE then a . z <> TRUE by EQREL_1:def_6; hence ((Ex (a,PA,G)) '&' u) . z = TRUE by A3, A1; ::_thesis: verum end; end; end; hence ((Ex (a,PA,G)) '&' u) . z = TRUE ; ::_thesis: verum end; suppose ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ; ::_thesis: ((Ex (a,PA,G)) '&' u) . z = TRUE hence ((Ex (a,PA,G)) '&' u) . z = TRUE by A3; ::_thesis: verum end; end; end; theorem Th28: :: BVFUNC_2:28 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G)) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G)) let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G)) let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G)) ) assume Z: u is_independent_of PA,G ; ::_thesis: All ((u 'xor' a),PA,G) '<' u 'xor' (All (a,PA,G)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((u 'xor' a),PA,G)) . z = TRUE or (u 'xor' (All (a,PA,G))) . z = TRUE ) assume A2: (All ((u 'xor' a),PA,G)) . z = TRUE ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE A3: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; A4: ( 'not' FALSE = TRUE & (u 'xor' (All (a,PA,G))) . z = ((All (a,PA,G)) . z) 'xor' (u . z) ) by BVFUNC_1:def_5, MARGREL1:11; percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) or ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ) ; suppose ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) ) ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE then A5: ( u . z = TRUE & a . z = TRUE ) by EQREL_1:def_6; A6: FALSE '&' TRUE = FALSE by MARGREL1:12; (u 'xor' a) . z = (a . z) 'xor' (u . z) by BVFUNC_1:def_5 .= FALSE by A5, A6, MARGREL1:11 ; hence (u 'xor' (All (a,PA,G))) . z = TRUE by A2, A3, BVFUNC_1:def_16; ::_thesis: verum end; supposeA7: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE then consider x1 being Element of Y such that A8: x1 in EqClass (z,(CompF (PA,G))) and a . x1 <> TRUE ; A9: u . x1 = TRUE by A7, A8; A10: (All (a,PA,G)) . z = FALSE by A7, BVFUNC_1:def_16; u . z = u . x1 by Z, Def8, A3, A8, BVFUNC_1:def_15; then (u 'xor' (All (a,PA,G))) . z = TRUE 'or' FALSE by A4, A10, A9 .= TRUE by BINARITH:3 ; hence (u 'xor' (All (a,PA,G))) . z = TRUE ; ::_thesis: verum end; suppose ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE then consider x1 being Element of Y such that A11: x1 in EqClass (z,(CompF (PA,G))) and A12: u . x1 <> TRUE ; now__::_thesis:_(u_'xor'_(All_(a,PA,G)))_._z_=_TRUE percases ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE or ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ; supposeA13: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE u . z = u . x1 by Z, Def8, A3, A11, BVFUNC_1:def_15; then A14: u . z = FALSE by A12, XBOOLEAN:def_3; (All (a,PA,G)) . z = TRUE by A13, BVFUNC_1:def_16; then (u 'xor' (All (a,PA,G))) . z = FALSE 'or' TRUE by A4, A14 .= TRUE by BINARITH:3 ; hence (u 'xor' (All (a,PA,G))) . z = TRUE ; ::_thesis: verum end; suppose ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ; ::_thesis: (u 'xor' (All (a,PA,G))) . z = TRUE then consider x2 being Element of Y such that A15: x2 in EqClass (z,(CompF (PA,G))) and A16: a . x2 <> TRUE ; A17: a . x2 = FALSE by A16, XBOOLEAN:def_3; u . x1 = u . x2 by Z, Def8, A11, A15, BVFUNC_1:def_15; then A18: u . x2 = FALSE by A12, XBOOLEAN:def_3; (u 'xor' a) . x2 = (a . x2) 'xor' (u . x2) by BVFUNC_1:def_5 .= FALSE by A18, A17, MARGREL1:12 ; hence (u 'xor' (All (a,PA,G))) . z = TRUE by A2, A15, BVFUNC_1:def_16; ::_thesis: verum end; end; end; hence (u 'xor' (All (a,PA,G))) . z = TRUE ; ::_thesis: verum end; end; end; theorem :: BVFUNC_2:29 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'xor' u),PA,G) '<' (All (a,PA,G)) 'xor' u by Th28; theorem Th30: :: BVFUNC_2:30 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G)) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G)) let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G)) let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G)) ) A1: 'not' FALSE = TRUE by MARGREL1:11; assume Z: u is_independent_of PA,G ; ::_thesis: All ((u 'eqv' a),PA,G) '<' u 'eqv' (All (a,PA,G)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((u 'eqv' a),PA,G)) . z = TRUE or (u 'eqv' (All (a,PA,G))) . z = TRUE ) assume A3: (All ((u 'eqv' a),PA,G)) . z = TRUE ; ::_thesis: (u 'eqv' (All (a,PA,G))) . z = TRUE A4: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ) ; suppose ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) ) ; ::_thesis: (u 'eqv' (All (a,PA,G))) . z = TRUE then A5: ( (All (a,PA,G)) . z = TRUE & u . z = TRUE ) by EQREL_1:def_6, BVFUNC_1:def_16; (u 'eqv' (All (a,PA,G))) . z = 'not' ((u . z) 'xor' ((All (a,PA,G)) . z)) by BVFUNC_1:def_9 .= TRUE by A1, A5, MARGREL1:13 ; hence (u 'eqv' (All (a,PA,G))) . z = TRUE ; ::_thesis: verum end; supposeA6: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ; ::_thesis: (u 'eqv' (All (a,PA,G))) . z = TRUE then consider x1 being Element of Y such that A7: x1 in EqClass (z,(CompF (PA,G))) and A8: a . x1 <> TRUE ; A9: u . x1 = TRUE by A6, A7; A10: a . x1 = FALSE by A8, XBOOLEAN:def_3; (u 'eqv' a) . x1 = 'not' ((u . x1) 'xor' (a . x1)) by BVFUNC_1:def_9 .= 'not' (FALSE 'or' TRUE) by A1, A9, A10 .= FALSE by MARGREL1:11, BINARITH:3 ; hence (u 'eqv' (All (a,PA,G))) . z = TRUE by A3, A7, BVFUNC_1:def_16; ::_thesis: verum end; supposeA11: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) ) ; ::_thesis: (u 'eqv' (All (a,PA,G))) . z = TRUE then consider x1 being Element of Y such that A12: x1 in EqClass (z,(CompF (PA,G))) and A13: u . x1 <> TRUE ; A14: a . x1 = TRUE by A11, A12; A15: u . x1 = FALSE by A13, XBOOLEAN:def_3; (u 'eqv' a) . x1 = 'not' ((u . x1) 'xor' (a . x1)) by BVFUNC_1:def_9 .= 'not' (TRUE 'or' FALSE) by A1, A15, A14 .= FALSE by MARGREL1:11, BINARITH:3 ; hence (u 'eqv' (All (a,PA,G))) . z = TRUE by A3, A12, BVFUNC_1:def_16; ::_thesis: verum end; supposeA16: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ) ; ::_thesis: (u 'eqv' (All (a,PA,G))) . z = TRUE then consider x1 being Element of Y such that A17: x1 in EqClass (z,(CompF (PA,G))) and A18: u . x1 <> TRUE ; u . x1 = u . z by Z, Def8, A4, A17, BVFUNC_1:def_15; then A19: u . z = FALSE by A18, XBOOLEAN:def_3; A20: (All (a,PA,G)) . z = FALSE by A16, BVFUNC_1:def_16; (u 'eqv' (All (a,PA,G))) . z = 'not' ((u . z) 'xor' ((All (a,PA,G)) . z)) by BVFUNC_1:def_9 .= TRUE by MARGREL1:11, A20, A19, MARGREL1:13 ; hence (u 'eqv' (All (a,PA,G))) . z = TRUE ; ::_thesis: verum end; end; end; theorem :: BVFUNC_2:31 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds All ((a 'eqv' u),PA,G) '<' (All (a,PA,G)) 'eqv' u by Th30; theorem Th32: :: BVFUNC_2:32 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) ) assume Z: u is_independent_of PA,G ; ::_thesis: Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) A2: Ex ((u 'or' a),PA,G) '<' u 'or' (Ex (a,PA,G)) proof let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((u 'or' a),PA,G)) . z = TRUE or (u 'or' (Ex (a,PA,G))) . z = TRUE ) A3: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; A4: (u 'or' (Ex (a,PA,G))) . z = (u . z) 'or' ((Ex (a,PA,G)) . z) by BVFUNC_1:def_4; assume (Ex ((u 'or' a),PA,G)) . z = TRUE ; ::_thesis: (u 'or' (Ex (a,PA,G))) . z = TRUE then consider x1 being Element of Y such that A5: x1 in EqClass (z,(CompF (PA,G))) and A6: (u 'or' a) . x1 = TRUE by BVFUNC_1:def_17; A7: ( u . x1 = TRUE or u . x1 = FALSE ) by XBOOLEAN:def_3; A8: (u . x1) 'or' (a . x1) = TRUE by A6, BVFUNC_1:def_4; now__::_thesis:_(_(_u_._x1_=_TRUE_&_(u_'or'_(Ex_(a,PA,G)))_._z_=_TRUE_)_or_(_a_._x1_=_TRUE_&_(u_'or'_(Ex_(a,PA,G)))_._z_=_TRUE_)_) percases ( u . x1 = TRUE or a . x1 = TRUE ) by A8, A7, BINARITH:3; caseA9: u . x1 = TRUE ; ::_thesis: (u 'or' (Ex (a,PA,G))) . z = TRUE u . z = u . x1 by Z, Def8, A5, A3, BVFUNC_1:def_15; hence (u 'or' (Ex (a,PA,G))) . z = TRUE by A4, A9, BINARITH:10; ::_thesis: verum end; case a . x1 = TRUE ; ::_thesis: (u 'or' (Ex (a,PA,G))) . z = TRUE then (u 'or' (Ex (a,PA,G))) . z = (u . z) 'or' TRUE by A5, A4, BVFUNC_1:def_17 .= TRUE by BINARITH:10 ; hence (u 'or' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: verum end; end; end; hence (u 'or' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: verum end; u 'or' (Ex (a,PA,G)) '<' Ex ((u 'or' a),PA,G) proof let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u 'or' (Ex (a,PA,G))) . z = TRUE or (Ex ((u 'or' a),PA,G)) . z = TRUE ) A10: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume (u 'or' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: (Ex ((u 'or' a),PA,G)) . z = TRUE then A11: (u . z) 'or' ((Ex (a,PA,G)) . z) = TRUE by BVFUNC_1:def_4; A12: ( (Ex (a,PA,G)) . z = TRUE or (Ex (a,PA,G)) . z = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_u_._z_=_TRUE_&_(Ex_((u_'or'_a),PA,G))_._z_=_TRUE_)_or_(_(Ex_(a,PA,G))_._z_=_TRUE_&_(Ex_((u_'or'_a),PA,G))_._z_=_TRUE_)_) percases ( u . z = TRUE or (Ex (a,PA,G)) . z = TRUE ) by A11, A12, BINARITH:3; case u . z = TRUE ; ::_thesis: (Ex ((u 'or' a),PA,G)) . z = TRUE then (u 'or' a) . z = TRUE 'or' (a . z) by BVFUNC_1:def_4 .= TRUE by BINARITH:10 ; hence (Ex ((u 'or' a),PA,G)) . z = TRUE by A10, BVFUNC_1:def_17; ::_thesis: verum end; case (Ex (a,PA,G)) . z = TRUE ; ::_thesis: (Ex ((u 'or' a),PA,G)) . z = TRUE then consider x1 being Element of Y such that A13: x1 in EqClass (z,(CompF (PA,G))) and A14: a . x1 = TRUE by BVFUNC_1:def_17; (u 'or' a) . x1 = (u . x1) 'or' (a . x1) by BVFUNC_1:def_4 .= TRUE by A14, BINARITH:10 ; hence (Ex ((u 'or' a),PA,G)) . z = TRUE by A13, BVFUNC_1:def_17; ::_thesis: verum end; end; end; hence (Ex ((u 'or' a),PA,G)) . z = TRUE ; ::_thesis: verum end; hence Ex ((u 'or' a),PA,G) = u 'or' (Ex (a,PA,G)) by A2, BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC_2:33 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((a 'or' u),PA,G) = (Ex (a,PA,G)) 'or' u by Th32; theorem Th34: :: BVFUNC_2:34 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) ) assume Z: u is_independent_of PA,G ; ::_thesis: Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) A2: Ex ((u '&' a),PA,G) '<' u '&' (Ex (a,PA,G)) proof let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((u '&' a),PA,G)) . z = TRUE or (u '&' (Ex (a,PA,G))) . z = TRUE ) assume (Ex ((u '&' a),PA,G)) . z = TRUE ; ::_thesis: (u '&' (Ex (a,PA,G))) . z = TRUE then consider x1 being Element of Y such that A3: x1 in EqClass (z,(CompF (PA,G))) and A4: (u '&' a) . x1 = TRUE by BVFUNC_1:def_17; A5: (u . x1) '&' (a . x1) = TRUE by A4, MARGREL1:def_20; then a . x1 = TRUE by MARGREL1:12; then A6: (Ex (a,PA,G)) . z = TRUE by A3, BVFUNC_1:def_17; z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; then A7: u . z = u . x1 by Z, Def8, A3, BVFUNC_1:def_15; u . x1 = TRUE by A5, MARGREL1:12; then (u '&' (Ex (a,PA,G))) . z = TRUE '&' TRUE by A6, A7, MARGREL1:def_20 .= TRUE ; hence (u '&' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: verum end; u '&' (Ex (a,PA,G)) '<' Ex ((u '&' a),PA,G) proof let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u '&' (Ex (a,PA,G))) . z = TRUE or (Ex ((u '&' a),PA,G)) . z = TRUE ) assume (u '&' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: (Ex ((u '&' a),PA,G)) . z = TRUE then A8: (u . z) '&' ((Ex (a,PA,G)) . z) = TRUE by MARGREL1:def_20; then A9: u . z = TRUE by MARGREL1:12; (Ex (a,PA,G)) . z = TRUE by A8, MARGREL1:12; then consider x1 being Element of Y such that A10: x1 in EqClass (z,(CompF (PA,G))) and A11: a . x1 = TRUE by BVFUNC_1:def_17; z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; then u . x1 = u . z by Z, Def8, A10, BVFUNC_1:def_15; then (u '&' a) . x1 = TRUE '&' TRUE by A9, A11, MARGREL1:def_20 .= TRUE ; hence (Ex ((u '&' a),PA,G)) . z = TRUE by A10, BVFUNC_1:def_17; ::_thesis: verum end; hence Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) by A2, BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC_2:35 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds Ex ((a '&' u),PA,G) = (Ex (a,PA,G)) '&' u by Th34; theorem :: BVFUNC_2:36 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y holds u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y holds u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y holds u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G) let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G) let PA be a_partition of Y; ::_thesis: u 'imp' (Ex (a,PA,G)) '<' Ex ((u 'imp' a),PA,G) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u 'imp' (Ex (a,PA,G))) . z = TRUE or (Ex ((u 'imp' a),PA,G)) . z = TRUE ) A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume (u 'imp' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: (Ex ((u 'imp' a),PA,G)) . z = TRUE then A2: ('not' (u . z)) 'or' ((Ex (a,PA,G)) . z) = TRUE by BVFUNC_1:def_8; A3: ( (Ex (a,PA,G)) . z = TRUE or (Ex (a,PA,G)) . z = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_(u_._z)_=_TRUE_&_(Ex_((u_'imp'_a),PA,G))_._z_=_TRUE_)_or_(_(Ex_(a,PA,G))_._z_=_TRUE_&_(Ex_((u_'imp'_a),PA,G))_._z_=_TRUE_)_) percases ( 'not' (u . z) = TRUE or (Ex (a,PA,G)) . z = TRUE ) by A2, A3, BINARITH:3; caseA4: 'not' (u . z) = TRUE ; ::_thesis: (Ex ((u 'imp' a),PA,G)) . z = TRUE (u 'imp' a) . z = ('not' (u . z)) 'or' (a . z) by BVFUNC_1:def_8 .= TRUE by A4, BINARITH:10 ; hence (Ex ((u 'imp' a),PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ::_thesis: verum end; case (Ex (a,PA,G)) . z = TRUE ; ::_thesis: (Ex ((u 'imp' a),PA,G)) . z = TRUE then consider x1 being Element of Y such that A5: x1 in EqClass (z,(CompF (PA,G))) and A6: a . x1 = TRUE by BVFUNC_1:def_17; (u 'imp' a) . x1 = ('not' (u . x1)) 'or' (a . x1) by BVFUNC_1:def_8 .= TRUE by A6, BINARITH:10 ; hence (Ex ((u 'imp' a),PA,G)) . z = TRUE by A5, BVFUNC_1:def_17; ::_thesis: verum end; end; end; hence (Ex ((u 'imp' a),PA,G)) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC_2:37 for Y being non empty set for G being Subset of (PARTITIONS Y) for a, u being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for a, u being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for a, u being Function of Y,BOOLEAN for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) let a, u be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) let PA be a_partition of Y; ::_thesis: (Ex (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((Ex (a,PA,G)) 'imp' u) . z = TRUE or (Ex ((a 'imp' u),PA,G)) . z = TRUE ) A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume ((Ex (a,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . z = TRUE then A2: ('not' ((Ex (a,PA,G)) . z)) 'or' (u . z) = TRUE by BVFUNC_1:def_8; A3: ( u . z = TRUE or u . z = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_((Ex_(a,PA,G))_._z)_=_TRUE_&_(Ex_((a_'imp'_u),PA,G))_._z_=_TRUE_)_or_(_u_._z_=_TRUE_&_(Ex_((a_'imp'_u),PA,G))_._z_=_TRUE_)_) percases ( 'not' ((Ex (a,PA,G)) . z) = TRUE or u . z = TRUE ) by A2, A3, BINARITH:3; case 'not' ((Ex (a,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . z = TRUE then A4: a . z <> TRUE by A1, BVFUNC_1:def_17, MARGREL1:11; (a 'imp' u) . z = ('not' (a . z)) 'or' (u . z) by BVFUNC_1:def_8 .= TRUE 'or' (u . z) by MARGREL1:11, A4, XBOOLEAN:def_3 .= TRUE by BINARITH:10 ; hence (Ex ((a 'imp' u),PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ::_thesis: verum end; caseA5: u . z = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . z = TRUE (a 'imp' u) . z = ('not' (a . z)) 'or' (u . z) by BVFUNC_1:def_8 .= TRUE by A5, BINARITH:10 ; hence (Ex ((a 'imp' u),PA,G)) . z = TRUE by A1, BVFUNC_1:def_17; ::_thesis: verum end; end; end; hence (Ex ((a 'imp' u),PA,G)) . z = TRUE ; ::_thesis: verum end; theorem Th38: :: BVFUNC_2:38 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G) proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G) let u, a be Function of Y,BOOLEAN; ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G) let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G) ) A1: 'not' FALSE = TRUE by MARGREL1:11; assume Z: u is_independent_of PA,G ; ::_thesis: u 'xor' (Ex (a,PA,G)) '<' Ex ((u 'xor' a),PA,G) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (u 'xor' (Ex (a,PA,G))) . z = TRUE or (Ex ((u 'xor' a),PA,G)) . z = TRUE ) A3: (u 'xor' (Ex (a,PA,G))) . z = (u . z) 'xor' ((Ex (a,PA,G)) . z) by BVFUNC_1:def_5 .= (('not' (u . z)) '&' ((Ex (a,PA,G)) . z)) 'or' ((u . z) '&' ('not' ((Ex (a,PA,G)) . z))) ; A4: ( (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = TRUE or (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = FALSE ) by XBOOLEAN:def_3; A5: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume A6: (u 'xor' (Ex (a,PA,G))) . z = TRUE ; ::_thesis: (Ex ((u 'xor' a),PA,G)) . z = TRUE now__::_thesis:_(_(_('not'_(u_._z))_'&'_((Ex_(a,PA,G))_._z)_=_TRUE_&_(Ex_((u_'xor'_a),PA,G))_._z_=_TRUE_)_or_(_(u_._z)_'&'_('not'_((Ex_(a,PA,G))_._z))_=_TRUE_&_(Ex_((u_'xor'_a),PA,G))_._z_=_TRUE_)_) percases ( ('not' (u . z)) '&' ((Ex (a,PA,G)) . z) = TRUE or (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = TRUE ) by A6, A3, A4, BINARITH:3; caseA7: ('not' (u . z)) '&' ((Ex (a,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((u 'xor' a),PA,G)) . z = TRUE then (Ex (a,PA,G)) . z = TRUE by MARGREL1:12; then consider x1 being Element of Y such that A8: x1 in EqClass (z,(CompF (PA,G))) and A9: a . x1 = TRUE by BVFUNC_1:def_17; A10: u . z = u . x1 by Z, Def8, A5, A8, BVFUNC_1:def_15; A11: 'not' (u . z) = TRUE by A7, MARGREL1:12; (u 'xor' a) . x1 = (u . x1) 'xor' (a . x1) by BVFUNC_1:def_5 .= TRUE 'or' FALSE by A11, A9, A10, MARGREL1:11 .= TRUE by BINARITH:10 ; hence (Ex ((u 'xor' a),PA,G)) . z = TRUE by A8, BVFUNC_1:def_17; ::_thesis: verum end; caseA12: (u . z) '&' ('not' ((Ex (a,PA,G)) . z)) = TRUE ; ::_thesis: (Ex ((u 'xor' a),PA,G)) . z = TRUE then 'not' ((Ex (a,PA,G)) . z) = TRUE by MARGREL1:12; then a . z <> TRUE by A5, BVFUNC_1:def_17, MARGREL1:11; then A13: a . z = FALSE by XBOOLEAN:def_3; A14: u . z = TRUE by A12, MARGREL1:12; (u 'xor' a) . z = (u . z) 'xor' (a . z) by BVFUNC_1:def_5 .= FALSE 'or' TRUE by A1, A14, A13 .= TRUE by BINARITH:10 ; hence (Ex ((u 'xor' a),PA,G)) . z = TRUE by A5, BVFUNC_1:def_17; ::_thesis: verum end; end; end; hence (Ex ((u 'xor' a),PA,G)) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC_2:39 for Y being non empty set for G being Subset of (PARTITIONS Y) for u, a being Function of Y,BOOLEAN for PA being a_partition of Y st u is_independent_of PA,G holds (Ex (a,PA,G)) 'xor' u '<' Ex ((a 'xor' u),PA,G) by Th38;