:: MBOOLEAN semantic presentation begin definition let I be set ; let A be ManySortedSet of I; func bool A -> ManySortedSet of I means :Def1: :: MBOOLEAN:def 1 for i being set st i in I holds it . i = bool (A . i); existence ex b1 being ManySortedSet of I st for i being set st i in I holds b1 . i = bool (A . i) proof deffunc H1( set ) -> set = bool (A . \$1); thus ex X being ManySortedSet of I st for i being set st i in I holds X . i = H1(i) from PBOOLE:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds b1 . i = bool (A . i) ) & ( for i being set st i in I holds b2 . i = bool (A . i) ) holds b1 = b2 proof let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds X . i = bool (A . i) ) & ( for i being set st i in I holds Y . i = bool (A . i) ) implies X = Y ) assume that A1: for i being set st i in I holds X . i = bool (A . i) and A2: for i being set st i in I holds Y . i = bool (A . i) ; ::_thesis: X = Y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_Y_._i let i be set ; ::_thesis: ( i in I implies X . i = Y . i ) assume A3: i in I ; ::_thesis: X . i = Y . i hence X . i = bool (A . i) by A1 .= Y . i by A2, A3 ; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def1 defines bool MBOOLEAN:def_1_:_ for I being set for A, b3 being ManySortedSet of I holds ( b3 = bool A iff for i being set st i in I holds b3 . i = bool (A . i) ); registration let I be set ; let A be ManySortedSet of I; cluster bool A -> V2() ; coherence bool A is non-empty proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not (bool A) . i is empty ) assume A1: i in I ; ::_thesis: not (bool A) . i is empty not bool (A . i) is empty ; hence not (bool A) . i is empty by A1, Def1; ::_thesis: verum end; end; Lm1: for i, I, X being set for M being ManySortedSet of I st i in I holds dom (M +* (i .--> X)) = I proof let i, I, X be set ; ::_thesis: for M being ManySortedSet of I st i in I holds dom (M +* (i .--> X)) = I let M be ManySortedSet of I; ::_thesis: ( i in I implies dom (M +* (i .--> X)) = I ) assume A1: i in I ; ::_thesis: dom (M +* (i .--> X)) = I thus dom (M +* (i .--> X)) = (dom M) \/ (dom (i .--> X)) by FUNCT_4:def_1 .= I \/ (dom (i .--> X)) by PARTFUN1:def_2 .= I \/ {i} by FUNCOP_1:13 .= I by A1, ZFMISC_1:40 ; ::_thesis: verum end; Lm2: for I being set for A, B being ManySortedSet of I for i being set st i in I holds (bool (A \/ B)) . i = bool ((A . i) \/ (B . i)) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for i being set st i in I holds (bool (A \/ B)) . i = bool ((A . i) \/ (B . i)) let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds (bool (A \/ B)) . i = bool ((A . i) \/ (B . i)) let i be set ; ::_thesis: ( i in I implies (bool (A \/ B)) . i = bool ((A . i) \/ (B . i)) ) assume A1: i in I ; ::_thesis: (bool (A \/ B)) . i = bool ((A . i) \/ (B . i)) hence (bool (A \/ B)) . i = bool ((A \/ B) . i) by Def1 .= bool ((A . i) \/ (B . i)) by A1, PBOOLE:def_4 ; ::_thesis: verum end; Lm3: for I being set for A, B being ManySortedSet of I for i being set st i in I holds (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for i being set st i in I holds (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) let i be set ; ::_thesis: ( i in I implies (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) ) assume A1: i in I ; ::_thesis: (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) hence (bool (A /\ B)) . i = bool ((A /\ B) . i) by Def1 .= bool ((A . i) /\ (B . i)) by A1, PBOOLE:def_5 ; ::_thesis: verum end; Lm4: for I being set for A, B being ManySortedSet of I for i being set st i in I holds (bool (A \ B)) . i = bool ((A . i) \ (B . i)) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for i being set st i in I holds (bool (A \ B)) . i = bool ((A . i) \ (B . i)) let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds (bool (A \ B)) . i = bool ((A . i) \ (B . i)) let i be set ; ::_thesis: ( i in I implies (bool (A \ B)) . i = bool ((A . i) \ (B . i)) ) assume A1: i in I ; ::_thesis: (bool (A \ B)) . i = bool ((A . i) \ (B . i)) hence (bool (A \ B)) . i = bool ((A \ B) . i) by Def1 .= bool ((A . i) \ (B . i)) by A1, PBOOLE:def_6 ; ::_thesis: verum end; Lm5: for I being set for A, B being ManySortedSet of I for i being set st i in I holds (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i)) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for i being set st i in I holds (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i)) let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i)) let i be set ; ::_thesis: ( i in I implies (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i)) ) assume A1: i in I ; ::_thesis: (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i)) hence (bool (A \+\ B)) . i = bool ((A \+\ B) . i) by Def1 .= bool ((A . i) \+\ (B . i)) by A1, PBOOLE:4 ; ::_thesis: verum end; theorem Th1: :: MBOOLEAN:1 for I being set for X, Y being ManySortedSet of I holds ( X = bool Y iff for A being ManySortedSet of I holds ( A in X iff A c= Y ) ) proof let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds ( X = bool Y iff for A being ManySortedSet of I holds ( A in X iff A c= Y ) ) let X, Y be ManySortedSet of I; ::_thesis: ( X = bool Y iff for A being ManySortedSet of I holds ( A in X iff A c= Y ) ) thus ( X = bool Y implies for A being ManySortedSet of I holds ( A in X iff A c= Y ) ) ::_thesis: ( ( for A being ManySortedSet of I holds ( A in X iff A c= Y ) ) implies X = bool Y ) proof assume A1: X = bool Y ; ::_thesis: for A being ManySortedSet of I holds ( A in X iff A c= Y ) let A be ManySortedSet of I; ::_thesis: ( A in X iff A c= Y ) thus ( A in X implies A c= Y ) ::_thesis: ( A c= Y implies A in X ) proof assume A2: A in X ; ::_thesis: A c= Y let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= Y . i ) assume A3: i in I ; ::_thesis: A . i c= Y . i then A4: A . i in X . i by A2, PBOOLE:def_1; X . i = bool (Y . i) by A1, A3, Def1; hence A . i c= Y . i by A4; ::_thesis: verum end; assume A5: A c= Y ; ::_thesis: A in X let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in X . i ) assume A6: i in I ; ::_thesis: A . i in X . i then A7: A . i c= Y . i by A5, PBOOLE:def_2; X . i = bool (Y . i) by A1, A6, Def1; hence A . i in X . i by A7; ::_thesis: verum end; assume A8: for A being ManySortedSet of I holds ( A in X iff A c= Y ) ; ::_thesis: X = bool Y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_(bool_Y)_._i let i be set ; ::_thesis: ( i in I implies X . i = (bool Y) . i ) assume A9: i in I ; ::_thesis: X . i = (bool Y) . i [[0]] I c= Y by PBOOLE:43; then A10: [[0]] I in X by A8; for A9 being set holds ( A9 in X . i iff A9 c= Y . i ) proof let A9 be set ; ::_thesis: ( A9 in X . i iff A9 c= Y . i ) A11: dom (i .--> A9) = {i} by FUNCOP_1:13; dom (([[0]] I) +* (i .--> A9)) = I by A9, Lm1; then reconsider K = ([[0]] I) +* (i .--> A9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; i in {i} by TARSKI:def_1; then A12: K . i = (i .--> A9) . i by A11, FUNCT_4:13 .= A9 by FUNCOP_1:72 ; thus ( A9 in X . i implies A9 c= Y . i ) ::_thesis: ( A9 c= Y . i implies A9 in X . i ) proof assume A13: A9 in X . i ; ::_thesis: A9 c= Y . i K in X proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in X . j ) assume A14: j in I ; ::_thesis: K . j in X . j now__::_thesis:_(_(_j_=_i_&_K_._j_in_X_._j_)_or_(_j_<>_i_&_K_._j_in_X_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: K . j in X . j hence K . j in X . j by A12, A13; ::_thesis: verum end; case j <> i ; ::_thesis: K . j in X . j then not j in dom (i .--> A9) by A11, TARSKI:def_1; then K . j = ([[0]] I) . j by FUNCT_4:11; hence K . j in X . j by A10, A14, PBOOLE:def_1; ::_thesis: verum end; end; end; hence K . j in X . j ; ::_thesis: verum end; then K c= Y by A8; hence A9 c= Y . i by A9, A12, PBOOLE:def_2; ::_thesis: verum end; assume A15: A9 c= Y . i ; ::_thesis: A9 in X . i K c= Y proof let j be set ; :: according to PBOOLE:def_2 ::_thesis: ( not j in I or K . j c= Y . j ) assume A16: j in I ; ::_thesis: K . j c= Y . j now__::_thesis:_(_(_j_=_i_&_K_._j_c=_Y_._j_)_or_(_j_<>_i_&_K_._j_c=_Y_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: K . j c= Y . j hence K . j c= Y . j by A12, A15; ::_thesis: verum end; case j <> i ; ::_thesis: K . j c= Y . j then not j in dom (i .--> A9) by A11, TARSKI:def_1; then A17: K . j = ([[0]] I) . j by FUNCT_4:11; [[0]] I c= Y by PBOOLE:43; hence K . j c= Y . j by A16, A17, PBOOLE:def_2; ::_thesis: verum end; end; end; hence K . j c= Y . j ; ::_thesis: verum end; then K in X by A8; hence A9 in X . i by A9, A12, PBOOLE:def_1; ::_thesis: verum end; then X . i = bool (Y . i) by ZFMISC_1:def_1; hence X . i = (bool Y) . i by A9, Def1; ::_thesis: verum end; hence X = bool Y by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:2 for I being set holds bool ([[0]] I) = I --> {{}} proof let I be set ; ::_thesis: bool ([[0]] I) = I --> {{}} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (bool_([[0]]_I))_._i_=_(I_-->_{{}})_._i let i be set ; ::_thesis: ( i in I implies (bool ([[0]] I)) . i = (I --> {{}}) . i ) assume A1: i in I ; ::_thesis: (bool ([[0]] I)) . i = (I --> {{}}) . i then (bool ([[0]] I)) . i = bool (([[0]] I) . i) by Def1 .= {{}} by PBOOLE:5, ZFMISC_1:1 ; hence (bool ([[0]] I)) . i = (I --> {{}}) . i by A1, FUNCOP_1:7; ::_thesis: verum end; hence bool ([[0]] I) = I --> {{}} by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:3 for I, x being set holds bool (I --> x) = I --> (bool x) proof let I, x be set ; ::_thesis: bool (I --> x) = I --> (bool x) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (bool_(I_-->_x))_._i_=_(I_-->_(bool_x))_._i let i be set ; ::_thesis: ( i in I implies (bool (I --> x)) . i = (I --> (bool x)) . i ) assume A1: i in I ; ::_thesis: (bool (I --> x)) . i = (I --> (bool x)) . i hence (bool (I --> x)) . i = bool ((I --> x) . i) by Def1 .= bool x by A1, FUNCOP_1:7 .= (I --> (bool x)) . i by A1, FUNCOP_1:7 ; ::_thesis: verum end; hence bool (I --> x) = I --> (bool x) by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:4 for I, x being set holds bool (I --> {x}) = I --> {{},{x}} proof let I, x be set ; ::_thesis: bool (I --> {x}) = I --> {{},{x}} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (bool_(I_-->_{x}))_._i_=_(I_-->_{{},{x}})_._i let i be set ; ::_thesis: ( i in I implies (bool (I --> {x})) . i = (I --> {{},{x}}) . i ) assume A1: i in I ; ::_thesis: (bool (I --> {x})) . i = (I --> {{},{x}}) . i hence (bool (I --> {x})) . i = bool ((I --> {x}) . i) by Def1 .= bool {x} by A1, FUNCOP_1:7 .= {{},{x}} by ZFMISC_1:24 .= (I --> {{},{x}}) . i by A1, FUNCOP_1:7 ; ::_thesis: verum end; hence bool (I --> {x}) = I --> {{},{x}} by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:5 for I being set for A being ManySortedSet of I holds [[0]] I c= A proof let I be set ; ::_thesis: for A being ManySortedSet of I holds [[0]] I c= A let A be ManySortedSet of I; ::_thesis: [[0]] I c= A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ([[0]] I) . i c= A . i ) assume i in I ; ::_thesis: ([[0]] I) . i c= A . i ([[0]] I) . i = {} by PBOOLE:5; hence ([[0]] I) . i c= A . i by XBOOLE_1:2; ::_thesis: verum end; theorem :: MBOOLEAN:6 for I being set for A, B being ManySortedSet of I st A c= B holds bool A c= bool B proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A c= B holds bool A c= bool B let A, B be ManySortedSet of I; ::_thesis: ( A c= B implies bool A c= bool B ) assume A1: A c= B ; ::_thesis: bool A c= bool B let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (bool A) . i c= (bool B) . i ) assume A2: i in I ; ::_thesis: (bool A) . i c= (bool B) . i then A3: A . i c= B . i by A1, PBOOLE:def_2; ( (bool A) . i = bool (A . i) & (bool B) . i = bool (B . i) ) by A2, Def1; hence (bool A) . i c= (bool B) . i by A3, ZFMISC_1:67; ::_thesis: verum end; theorem :: MBOOLEAN:7 for I being set for A, B being ManySortedSet of I holds (bool A) \/ (bool B) c= bool (A \/ B) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I holds (bool A) \/ (bool B) c= bool (A \/ B) let A, B be ManySortedSet of I; ::_thesis: (bool A) \/ (bool B) c= bool (A \/ B) let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ((bool A) \/ (bool B)) . i c= (bool (A \/ B)) . i ) assume A1: i in I ; ::_thesis: ((bool A) \/ (bool B)) . i c= (bool (A \/ B)) . i then A2: (bool (A \/ B)) . i = bool ((A . i) \/ (B . i)) by Lm2; ((bool A) \/ (bool B)) . i = ((bool A) . i) \/ ((bool B) . i) by A1, PBOOLE:def_4 .= (bool (A . i)) \/ ((bool B) . i) by A1, Def1 .= (bool (A . i)) \/ (bool (B . i)) by A1, Def1 ; hence ((bool A) \/ (bool B)) . i c= (bool (A \/ B)) . i by A2, ZFMISC_1:69; ::_thesis: verum end; theorem :: MBOOLEAN:8 for I being set for A, B being ManySortedSet of I st (bool A) \/ (bool B) = bool (A \/ B) holds for i being set st i in I holds A . i,B . i are_c=-comparable proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st (bool A) \/ (bool B) = bool (A \/ B) holds for i being set st i in I holds A . i,B . i are_c=-comparable let A, B be ManySortedSet of I; ::_thesis: ( (bool A) \/ (bool B) = bool (A \/ B) implies for i being set st i in I holds A . i,B . i are_c=-comparable ) assume A1: (bool A) \/ (bool B) = bool (A \/ B) ; ::_thesis: for i being set st i in I holds A . i,B . i are_c=-comparable let i be set ; ::_thesis: ( i in I implies A . i,B . i are_c=-comparable ) assume A2: i in I ; ::_thesis: A . i,B . i are_c=-comparable bool ((A . i) \/ (B . i)) = ((bool A) \/ (bool B)) . i by A1, A2, Lm2 .= ((bool A) . i) \/ ((bool B) . i) by A2, PBOOLE:def_4 .= ((bool A) . i) \/ (bool (B . i)) by A2, Def1 .= (bool (A . i)) \/ (bool (B . i)) by A2, Def1 ; hence A . i,B . i are_c=-comparable by ZFMISC_1:70; ::_thesis: verum end; theorem :: MBOOLEAN:9 for I being set for A, B being ManySortedSet of I holds bool (A /\ B) = (bool A) /\ (bool B) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I holds bool (A /\ B) = (bool A) /\ (bool B) let A, B be ManySortedSet of I; ::_thesis: bool (A /\ B) = (bool A) /\ (bool B) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (bool_(A_/\_B))_._i_=_((bool_A)_/\_(bool_B))_._i let i be set ; ::_thesis: ( i in I implies (bool (A /\ B)) . i = ((bool A) /\ (bool B)) . i ) assume A1: i in I ; ::_thesis: (bool (A /\ B)) . i = ((bool A) /\ (bool B)) . i hence (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) by Lm3 .= (bool (A . i)) /\ (bool (B . i)) by ZFMISC_1:71 .= (bool (A . i)) /\ ((bool B) . i) by A1, Def1 .= ((bool A) . i) /\ ((bool B) . i) by A1, Def1 .= ((bool A) /\ (bool B)) . i by A1, PBOOLE:def_5 ; ::_thesis: verum end; hence bool (A /\ B) = (bool A) /\ (bool B) by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:10 for I being set for A, B being ManySortedSet of I holds bool (A \ B) c= (I --> {{}}) \/ ((bool A) \ (bool B)) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I holds bool (A \ B) c= (I --> {{}}) \/ ((bool A) \ (bool B)) let A, B be ManySortedSet of I; ::_thesis: bool (A \ B) c= (I --> {{}}) \/ ((bool A) \ (bool B)) let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (bool (A \ B)) . i c= ((I --> {{}}) \/ ((bool A) \ (bool B))) . i ) assume A1: i in I ; ::_thesis: (bool (A \ B)) . i c= ((I --> {{}}) \/ ((bool A) \ (bool B))) . i then A2: (bool (A \ B)) . i = bool ((A . i) \ (B . i)) by Lm4; ((I --> {{}}) \/ ((bool A) \ (bool B))) . i = ((I --> {{}}) . i) \/ (((bool A) \ (bool B)) . i) by A1, PBOOLE:def_4 .= {{}} \/ (((bool A) \ (bool B)) . i) by A1, FUNCOP_1:7 .= {{}} \/ (((bool A) . i) \ ((bool B) . i)) by A1, PBOOLE:def_6 .= {{}} \/ ((bool (A . i)) \ ((bool B) . i)) by A1, Def1 .= {{}} \/ ((bool (A . i)) \ (bool (B . i))) by A1, Def1 ; hence (bool (A \ B)) . i c= ((I --> {{}}) \/ ((bool A) \ (bool B))) . i by A2, ZFMISC_1:72; ::_thesis: verum end; theorem :: MBOOLEAN:11 for I being set for X, A, B being ManySortedSet of I holds ( X c= A \ B iff ( X c= A & X misses B ) ) proof let I be set ; ::_thesis: for X, A, B being ManySortedSet of I holds ( X c= A \ B iff ( X c= A & X misses B ) ) let X, A, B be ManySortedSet of I; ::_thesis: ( X c= A \ B iff ( X c= A & X misses B ) ) thus ( X c= A \ B implies ( X c= A & X misses B ) ) ::_thesis: ( X c= A & X misses B implies X c= A \ B ) proof assume X c= A \ B ; ::_thesis: ( X c= A & X misses B ) then A1: X in bool (A \ B) by Th1; thus X c= A ::_thesis: X misses B proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= A . i ) assume A2: i in I ; ::_thesis: X . i c= A . i then X . i in (bool (A \ B)) . i by A1, PBOOLE:def_1; then X . i in bool ((A . i) \ (B . i)) by A2, Lm4; hence X . i c= A . i by XBOOLE_1:106; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_8 ::_thesis: ( not i in I or X . i misses B . i ) assume A3: i in I ; ::_thesis: X . i misses B . i then X . i in (bool (A \ B)) . i by A1, PBOOLE:def_1; then X . i in bool ((A . i) \ (B . i)) by A3, Lm4; hence X . i misses B . i by XBOOLE_1:106; ::_thesis: verum end; assume A4: ( X c= A & X misses B ) ; ::_thesis: X c= A \ B let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (A \ B) . i ) assume A5: i in I ; ::_thesis: X . i c= (A \ B) . i then ( X . i c= A . i & X . i misses B . i ) by A4, PBOOLE:def_2, PBOOLE:def_8; then X . i c= (A . i) \ (B . i) by XBOOLE_1:86; hence X . i c= (A \ B) . i by A5, PBOOLE:def_6; ::_thesis: verum end; theorem :: MBOOLEAN:12 for I being set for A, B being ManySortedSet of I holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B) let A, B be ManySortedSet of I; ::_thesis: (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B) let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ((bool (A \ B)) \/ (bool (B \ A))) . i c= (bool (A \+\ B)) . i ) assume A1: i in I ; ::_thesis: ((bool (A \ B)) \/ (bool (B \ A))) . i c= (bool (A \+\ B)) . i then A2: (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i)) by Lm5; ((bool (A \ B)) \/ (bool (B \ A))) . i = ((bool (A \ B)) . i) \/ ((bool (B \ A)) . i) by A1, PBOOLE:def_4 .= (bool ((A . i) \ (B . i))) \/ ((bool (B \ A)) . i) by A1, Lm4 .= (bool ((A . i) \ (B . i))) \/ (bool ((B . i) \ (A . i))) by A1, Lm4 ; hence ((bool (A \ B)) \/ (bool (B \ A))) . i c= (bool (A \+\ B)) . i by A2, ZFMISC_1:73; ::_thesis: verum end; theorem :: MBOOLEAN:13 for I being set for X, A, B being ManySortedSet of I holds ( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) ) proof let I be set ; ::_thesis: for X, A, B being ManySortedSet of I holds ( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) ) let X, A, B be ManySortedSet of I; ::_thesis: ( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) ) thus ( X c= A \+\ B implies ( X c= A \/ B & X misses A /\ B ) ) ::_thesis: ( X c= A \/ B & X misses A /\ B implies X c= A \+\ B ) proof assume X c= A \+\ B ; ::_thesis: ( X c= A \/ B & X misses A /\ B ) then A1: X in bool (A \+\ B) by Th1; thus X c= A \/ B ::_thesis: X misses A /\ B proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (A \/ B) . i ) assume A2: i in I ; ::_thesis: X . i c= (A \/ B) . i then X . i in (bool (A \+\ B)) . i by A1, PBOOLE:def_1; then X . i in bool ((A . i) \+\ (B . i)) by A2, Lm5; then X . i c= (A . i) \/ (B . i) by XBOOLE_1:107; hence X . i c= (A \/ B) . i by A2, PBOOLE:def_4; ::_thesis: verum end; let i be set ; :: according to PBOOLE:def_8 ::_thesis: ( not i in I or X . i misses (A /\ B) . i ) assume A3: i in I ; ::_thesis: X . i misses (A /\ B) . i then X . i in (bool (A \+\ B)) . i by A1, PBOOLE:def_1; then X . i in bool ((A . i) \+\ (B . i)) by A3, Lm5; then X . i misses (A . i) /\ (B . i) by XBOOLE_1:107; hence X . i misses (A /\ B) . i by A3, PBOOLE:def_5; ::_thesis: verum end; assume that A4: X c= A \/ B and A5: X misses A /\ B ; ::_thesis: X c= A \+\ B let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (A \+\ B) . i ) assume A6: i in I ; ::_thesis: X . i c= (A \+\ B) . i then X . i misses (A /\ B) . i by A5, PBOOLE:def_8; then A7: X . i misses (A . i) /\ (B . i) by A6, PBOOLE:def_5; X . i c= (A \/ B) . i by A4, A6, PBOOLE:def_2; then X . i c= (A . i) \/ (B . i) by A6, PBOOLE:def_4; then X . i c= (A . i) \+\ (B . i) by A7, XBOOLE_1:107; hence X . i c= (A \+\ B) . i by A6, PBOOLE:4; ::_thesis: verum end; theorem :: MBOOLEAN:14 for I being set for X, A, Y being ManySortedSet of I st ( X c= A or Y c= A ) holds X /\ Y c= A proof let I be set ; ::_thesis: for X, A, Y being ManySortedSet of I st ( X c= A or Y c= A ) holds X /\ Y c= A let X, A, Y be ManySortedSet of I; ::_thesis: ( ( X c= A or Y c= A ) implies X /\ Y c= A ) assume A1: ( X c= A or Y c= A ) ; ::_thesis: X /\ Y c= A percases ( X c= A or Y c= A ) by A1; supposeA2: X c= A ; ::_thesis: X /\ Y c= A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X /\ Y) . i c= A . i ) assume A3: i in I ; ::_thesis: (X /\ Y) . i c= A . i then X . i c= A . i by A2, PBOOLE:def_2; then (X . i) /\ (Y . i) c= A . i by XBOOLE_1:108; hence (X /\ Y) . i c= A . i by A3, PBOOLE:def_5; ::_thesis: verum end; supposeA4: Y c= A ; ::_thesis: X /\ Y c= A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X /\ Y) . i c= A . i ) assume A5: i in I ; ::_thesis: (X /\ Y) . i c= A . i then Y . i c= A . i by A4, PBOOLE:def_2; then (X . i) /\ (Y . i) c= A . i by XBOOLE_1:108; hence (X /\ Y) . i c= A . i by A5, PBOOLE:def_5; ::_thesis: verum end; end; end; theorem :: MBOOLEAN:15 for I being set for X, A, Y being ManySortedSet of I st X c= A holds X \ Y c= A proof let I be set ; ::_thesis: for X, A, Y being ManySortedSet of I st X c= A holds X \ Y c= A let X, A, Y be ManySortedSet of I; ::_thesis: ( X c= A implies X \ Y c= A ) assume A1: X c= A ; ::_thesis: X \ Y c= A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X \ Y) . i c= A . i ) assume A2: i in I ; ::_thesis: (X \ Y) . i c= A . i then X . i c= A . i by A1, PBOOLE:def_2; then (X . i) \ (Y . i) c= A . i by XBOOLE_1:109; hence (X \ Y) . i c= A . i by A2, PBOOLE:def_6; ::_thesis: verum end; theorem :: MBOOLEAN:16 for I being set for X, A, Y being ManySortedSet of I st X c= A & Y c= A holds X \+\ Y c= A proof let I be set ; ::_thesis: for X, A, Y being ManySortedSet of I st X c= A & Y c= A holds X \+\ Y c= A let X, A, Y be ManySortedSet of I; ::_thesis: ( X c= A & Y c= A implies X \+\ Y c= A ) assume A1: ( X c= A & Y c= A ) ; ::_thesis: X \+\ Y c= A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X \+\ Y) . i c= A . i ) assume A2: i in I ; ::_thesis: (X \+\ Y) . i c= A . i then ( X . i c= A . i & Y . i c= A . i ) by A1, PBOOLE:def_2; then (X . i) \+\ (Y . i) c= A . i by XBOOLE_1:110; then (X . i) \+\ (Y . i) in bool (A . i) ; then (X \+\ Y) . i in bool (A . i) by A2, PBOOLE:4; hence (X \+\ Y) . i c= A . i ; ::_thesis: verum end; theorem :: MBOOLEAN:17 for I being set for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X \/ Y)) proof let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X \/ Y)) let X, Y be ManySortedSet of I; ::_thesis: [|X,Y|] c= bool (bool (X \/ Y)) let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or [|X,Y|] . i c= (bool (bool (X \/ Y))) . i ) assume A1: i in I ; ::_thesis: [|X,Y|] . i c= (bool (bool (X \/ Y))) . i then A2: [|X,Y|] . i = [:(X . i),(Y . i):] by PBOOLE:def_16; (bool (bool (X \/ Y))) . i = bool ((bool (X \/ Y)) . i) by A1, Def1 .= bool (bool ((X . i) \/ (Y . i))) by A1, Lm2 ; hence [|X,Y|] . i c= (bool (bool (X \/ Y))) . i by A2, ZFMISC_1:86; ::_thesis: verum end; theorem :: MBOOLEAN:18 for I being set for X, A being ManySortedSet of I holds ( X c= A iff X in bool A ) proof let I be set ; ::_thesis: for X, A being ManySortedSet of I holds ( X c= A iff X in bool A ) let X, A be ManySortedSet of I; ::_thesis: ( X c= A iff X in bool A ) thus ( X c= A implies X in bool A ) ::_thesis: ( X in bool A implies X c= A ) proof assume A1: X c= A ; ::_thesis: X in bool A let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or X . i in (bool A) . i ) assume A2: i in I ; ::_thesis: X . i in (bool A) . i then X . i c= A . i by A1, PBOOLE:def_2; then X . i in bool (A . i) ; hence X . i in (bool A) . i by A2, Def1; ::_thesis: verum end; assume A3: X in bool A ; ::_thesis: X c= A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= A . i ) assume A4: i in I ; ::_thesis: X . i c= A . i then X . i in (bool A) . i by A3, PBOOLE:def_1; then X . i in bool (A . i) by A4, Def1; hence X . i c= A . i ; ::_thesis: verum end; theorem :: MBOOLEAN:19 for I being set for A, B being ManySortedSet of I holds (Funcs) (A,B) c= bool [|A,B|] proof let I be set ; ::_thesis: for A, B being ManySortedSet of I holds (Funcs) (A,B) c= bool [|A,B|] let A, B be ManySortedSet of I; ::_thesis: (Funcs) (A,B) c= bool [|A,B|] let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i ) assume A1: i in I ; ::_thesis: ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i then A2: ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def_17; (bool [|A,B|]) . i = bool ([|A,B|] . i) by A1, Def1 .= bool [:(A . i),(B . i):] by A1, PBOOLE:def_16 ; hence ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i by A2, FRAENKEL:2; ::_thesis: verum end; begin definition let I be set ; let A be ManySortedSet of I; func union A -> ManySortedSet of I means :Def2: :: MBOOLEAN:def 2 for i being set st i in I holds it . i = union (A . i); existence ex b1 being ManySortedSet of I st for i being set st i in I holds b1 . i = union (A . i) proof deffunc H1( set ) -> set = union (A . \$1); thus ex X being ManySortedSet of I st for i being set st i in I holds X . i = H1(i) from PBOOLE:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds b1 . i = union (A . i) ) & ( for i being set st i in I holds b2 . i = union (A . i) ) holds b1 = b2 proof let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds X . i = union (A . i) ) & ( for i being set st i in I holds Y . i = union (A . i) ) implies X = Y ) assume that A1: for i being set st i in I holds X . i = union (A . i) and A2: for i being set st i in I holds Y . i = union (A . i) ; ::_thesis: X = Y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_Y_._i let i be set ; ::_thesis: ( i in I implies X . i = Y . i ) assume A3: i in I ; ::_thesis: X . i = Y . i hence X . i = union (A . i) by A1 .= Y . i by A2, A3 ; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def2 defines union MBOOLEAN:def_2_:_ for I being set for A, b3 being ManySortedSet of I holds ( b3 = union A iff for i being set st i in I holds b3 . i = union (A . i) ); registration let I be set ; cluster union ([[0]] I) -> V3() ; coherence union ([[0]] I) is empty-yielding proof let i be set ; :: according to PBOOLE:def_12 ::_thesis: ( not i in I or (union ([[0]] I)) . i is empty ) A1: union (([[0]] I) . i) is empty by PBOOLE:5, ZFMISC_1:2; assume i in I ; ::_thesis: (union ([[0]] I)) . i is empty hence (union ([[0]] I)) . i is empty by A1, Def2; ::_thesis: verum end; end; Lm6: for I being set for A, B being ManySortedSet of I for i being set st i in I holds (union (A \/ B)) . i = union ((A . i) \/ (B . i)) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for i being set st i in I holds (union (A \/ B)) . i = union ((A . i) \/ (B . i)) let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds (union (A \/ B)) . i = union ((A . i) \/ (B . i)) let i be set ; ::_thesis: ( i in I implies (union (A \/ B)) . i = union ((A . i) \/ (B . i)) ) assume A1: i in I ; ::_thesis: (union (A \/ B)) . i = union ((A . i) \/ (B . i)) hence (union (A \/ B)) . i = union ((A \/ B) . i) by Def2 .= union ((A . i) \/ (B . i)) by A1, PBOOLE:def_4 ; ::_thesis: verum end; Lm7: for I being set for A, B being ManySortedSet of I for i being set st i in I holds (union (A /\ B)) . i = union ((A . i) /\ (B . i)) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for i being set st i in I holds (union (A /\ B)) . i = union ((A . i) /\ (B . i)) let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds (union (A /\ B)) . i = union ((A . i) /\ (B . i)) let i be set ; ::_thesis: ( i in I implies (union (A /\ B)) . i = union ((A . i) /\ (B . i)) ) assume A1: i in I ; ::_thesis: (union (A /\ B)) . i = union ((A . i) /\ (B . i)) hence (union (A /\ B)) . i = union ((A /\ B) . i) by Def2 .= union ((A . i) /\ (B . i)) by A1, PBOOLE:def_5 ; ::_thesis: verum end; theorem :: MBOOLEAN:20 for I being set for A, X being ManySortedSet of I holds ( A in union X iff ex Y being ManySortedSet of I st ( A in Y & Y in X ) ) proof let I be set ; ::_thesis: for A, X being ManySortedSet of I holds ( A in union X iff ex Y being ManySortedSet of I st ( A in Y & Y in X ) ) let A, X be ManySortedSet of I; ::_thesis: ( A in union X iff ex Y being ManySortedSet of I st ( A in Y & Y in X ) ) thus ( A in union X implies ex Y being ManySortedSet of I st ( A in Y & Y in X ) ) ::_thesis: ( ex Y being ManySortedSet of I st ( A in Y & Y in X ) implies A in union X ) proof defpred S1[ set , set ] means ( A . \$1 in \$2 & \$2 in X . \$1 ); assume A1: A in union X ; ::_thesis: ex Y being ManySortedSet of I st ( A in Y & Y in X ) A2: for i being set st i in I holds ex Y being set st S1[i,Y] proof let i be set ; ::_thesis: ( i in I implies ex Y being set st S1[i,Y] ) assume A3: i in I ; ::_thesis: ex Y being set st S1[i,Y] then A . i in (union X) . i by A1, PBOOLE:def_1; then A . i in union (X . i) by A3, Def2; hence ex Y being set st S1[i,Y] by TARSKI:def_4; ::_thesis: verum end; consider K being ManySortedSet of I such that A4: for i being set st i in I holds S1[i,K . i] from PBOOLE:sch_3(A2); take K ; ::_thesis: ( A in K & K in X ) thus A in K ::_thesis: K in X proof let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in K . i ) assume i in I ; ::_thesis: A . i in K . i hence A . i in K . i by A4; ::_thesis: verum end; thus K in X ::_thesis: verum proof let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or K . i in X . i ) assume i in I ; ::_thesis: K . i in X . i hence K . i in X . i by A4; ::_thesis: verum end; end; given Y being ManySortedSet of I such that A5: ( A in Y & Y in X ) ; ::_thesis: A in union X let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in (union X) . i ) assume A6: i in I ; ::_thesis: A . i in (union X) . i then ( A . i in Y . i & Y . i in X . i ) by A5, PBOOLE:def_1; then A . i in union (X . i) by TARSKI:def_4; hence A . i in (union X) . i by A6, Def2; ::_thesis: verum end; theorem :: MBOOLEAN:21 for I being set holds union ([[0]] I) = [[0]] I proof let I be set ; ::_thesis: union ([[0]] I) = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (union_([[0]]_I))_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies (union ([[0]] I)) . i = ([[0]] I) . i ) assume i in I ; ::_thesis: (union ([[0]] I)) . i = ([[0]] I) . i hence (union ([[0]] I)) . i = union (([[0]] I) . i) by Def2 .= {} by PBOOLE:5, ZFMISC_1:2 .= ([[0]] I) . i by PBOOLE:5 ; ::_thesis: verum end; hence union ([[0]] I) = [[0]] I by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:22 for I, x being set holds union (I --> x) = I --> (union x) proof let I, x be set ; ::_thesis: union (I --> x) = I --> (union x) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (union_(I_-->_x))_._i_=_(I_-->_(union_x))_._i let i be set ; ::_thesis: ( i in I implies (union (I --> x)) . i = (I --> (union x)) . i ) assume A1: i in I ; ::_thesis: (union (I --> x)) . i = (I --> (union x)) . i hence (union (I --> x)) . i = union ((I --> x) . i) by Def2 .= union x by A1, FUNCOP_1:7 .= (I --> (union x)) . i by A1, FUNCOP_1:7 ; ::_thesis: verum end; hence union (I --> x) = I --> (union x) by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:23 for I, x being set holds union (I --> {x}) = I --> x proof let I, x be set ; ::_thesis: union (I --> {x}) = I --> x now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (union_(I_-->_{x}))_._i_=_(I_-->_x)_._i let i be set ; ::_thesis: ( i in I implies (union (I --> {x})) . i = (I --> x) . i ) assume A1: i in I ; ::_thesis: (union (I --> {x})) . i = (I --> x) . i hence (union (I --> {x})) . i = union ((I --> {x}) . i) by Def2 .= union {x} by A1, FUNCOP_1:7 .= x by ZFMISC_1:25 .= (I --> x) . i by A1, FUNCOP_1:7 ; ::_thesis: verum end; hence union (I --> {x}) = I --> x by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:24 for I, x, y being set holds union (I --> {{x},{y}}) = I --> {x,y} proof let I, x, y be set ; ::_thesis: union (I --> {{x},{y}}) = I --> {x,y} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (union_(I_-->_{{x},{y}}))_._i_=_(I_-->_{x,y})_._i let i be set ; ::_thesis: ( i in I implies (union (I --> {{x},{y}})) . i = (I --> {x,y}) . i ) assume A1: i in I ; ::_thesis: (union (I --> {{x},{y}})) . i = (I --> {x,y}) . i hence (union (I --> {{x},{y}})) . i = union ((I --> {{x},{y}}) . i) by Def2 .= union {{x},{y}} by A1, FUNCOP_1:7 .= {x,y} by ZFMISC_1:26 .= (I --> {x,y}) . i by A1, FUNCOP_1:7 ; ::_thesis: verum end; hence union (I --> {{x},{y}}) = I --> {x,y} by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:25 for I being set for X, A being ManySortedSet of I st X in A holds X c= union A proof let I be set ; ::_thesis: for X, A being ManySortedSet of I st X in A holds X c= union A let X, A be ManySortedSet of I; ::_thesis: ( X in A implies X c= union A ) assume A1: X in A ; ::_thesis: X c= union A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (union A) . i ) assume A2: i in I ; ::_thesis: X . i c= (union A) . i then X . i in A . i by A1, PBOOLE:def_1; then X . i c= union (A . i) by ZFMISC_1:74; hence X . i c= (union A) . i by A2, Def2; ::_thesis: verum end; theorem :: MBOOLEAN:26 for I being set for A, B being ManySortedSet of I st A c= B holds union A c= union B proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A c= B holds union A c= union B let A, B be ManySortedSet of I; ::_thesis: ( A c= B implies union A c= union B ) assume A1: A c= B ; ::_thesis: union A c= union B let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (union A) . i c= (union B) . i ) assume A2: i in I ; ::_thesis: (union A) . i c= (union B) . i then A . i c= B . i by A1, PBOOLE:def_2; then union (A . i) c= union (B . i) by ZFMISC_1:77; then (union A) . i c= union (B . i) by A2, Def2; hence (union A) . i c= (union B) . i by A2, Def2; ::_thesis: verum end; theorem :: MBOOLEAN:27 for I being set for A, B being ManySortedSet of I holds union (A \/ B) = (union A) \/ (union B) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I holds union (A \/ B) = (union A) \/ (union B) let A, B be ManySortedSet of I; ::_thesis: union (A \/ B) = (union A) \/ (union B) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (union_(A_\/_B))_._i_=_((union_A)_\/_(union_B))_._i let i be set ; ::_thesis: ( i in I implies (union (A \/ B)) . i = ((union A) \/ (union B)) . i ) assume A1: i in I ; ::_thesis: (union (A \/ B)) . i = ((union A) \/ (union B)) . i hence (union (A \/ B)) . i = union ((A . i) \/ (B . i)) by Lm6 .= (union (A . i)) \/ (union (B . i)) by ZFMISC_1:78 .= ((union A) . i) \/ (union (B . i)) by A1, Def2 .= ((union A) . i) \/ ((union B) . i) by A1, Def2 .= ((union A) \/ (union B)) . i by A1, PBOOLE:def_4 ; ::_thesis: verum end; hence union (A \/ B) = (union A) \/ (union B) by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:28 for I being set for A, B being ManySortedSet of I holds union (A /\ B) c= (union A) /\ (union B) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I holds union (A /\ B) c= (union A) /\ (union B) let A, B be ManySortedSet of I; ::_thesis: union (A /\ B) c= (union A) /\ (union B) let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (union (A /\ B)) . i c= ((union A) /\ (union B)) . i ) assume A1: i in I ; ::_thesis: (union (A /\ B)) . i c= ((union A) /\ (union B)) . i then A2: (union (A /\ B)) . i = union ((A . i) /\ (B . i)) by Lm7; ((union A) /\ (union B)) . i = ((union A) . i) /\ ((union B) . i) by A1, PBOOLE:def_5 .= (union (A . i)) /\ ((union B) . i) by A1, Def2 .= (union (A . i)) /\ (union (B . i)) by A1, Def2 ; hence (union (A /\ B)) . i c= ((union A) /\ (union B)) . i by A2, ZFMISC_1:79; ::_thesis: verum end; theorem :: MBOOLEAN:29 for I being set for A being ManySortedSet of I holds union (bool A) = A proof let I be set ; ::_thesis: for A being ManySortedSet of I holds union (bool A) = A let A be ManySortedSet of I; ::_thesis: union (bool A) = A now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (union_(bool_A))_._i_=_A_._i let i be set ; ::_thesis: ( i in I implies (union (bool A)) . i = A . i ) assume A1: i in I ; ::_thesis: (union (bool A)) . i = A . i hence (union (bool A)) . i = union ((bool A) . i) by Def2 .= union (bool (A . i)) by A1, Def1 .= A . i by ZFMISC_1:81 ; ::_thesis: verum end; hence union (bool A) = A by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:30 for I being set for A being ManySortedSet of I holds A c= bool (union A) proof let I be set ; ::_thesis: for A being ManySortedSet of I holds A c= bool (union A) let A be ManySortedSet of I; ::_thesis: A c= bool (union A) let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= (bool (union A)) . i ) assume A1: i in I ; ::_thesis: A . i c= (bool (union A)) . i then (bool (union A)) . i = bool ((union A) . i) by Def1 .= bool (union (A . i)) by A1, Def2 ; hence A . i c= (bool (union A)) . i by ZFMISC_1:82; ::_thesis: verum end; theorem :: MBOOLEAN:31 for I being set for Y, A, X being ManySortedSet of I st union Y c= A & X in Y holds X c= A proof let I be set ; ::_thesis: for Y, A, X being ManySortedSet of I st union Y c= A & X in Y holds X c= A let Y, A, X be ManySortedSet of I; ::_thesis: ( union Y c= A & X in Y implies X c= A ) assume that A1: union Y c= A and A2: X in Y ; ::_thesis: X c= A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= A . i ) assume A3: i in I ; ::_thesis: X . i c= A . i then (union Y) . i c= A . i by A1, PBOOLE:def_2; then A4: union (Y . i) c= A . i by A3, Def2; X . i in Y . i by A2, A3, PBOOLE:def_1; hence X . i c= A . i by A4, SETFAM_1:41; ::_thesis: verum end; theorem :: MBOOLEAN:32 for I being set for Z being ManySortedSet of I for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds X c= Z ) holds union A c= Z proof let I be set ; ::_thesis: for Z being ManySortedSet of I for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds X c= Z ) holds union A c= Z let Z be ManySortedSet of I; ::_thesis: for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds X c= Z ) holds union A c= Z let A be V2() ManySortedSet of I; ::_thesis: ( ( for X being ManySortedSet of I st X in A holds X c= Z ) implies union A c= Z ) assume A1: for X being ManySortedSet of I st X in A holds X c= Z ; ::_thesis: union A c= Z let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (union A) . i c= Z . i ) assume A2: i in I ; ::_thesis: (union A) . i c= Z . i for X9 being set st X9 in A . i holds X9 c= Z . i proof consider M being ManySortedSet of I such that A3: M in A by PBOOLE:134; let X9 be set ; ::_thesis: ( X9 in A . i implies X9 c= Z . i ) assume A4: X9 in A . i ; ::_thesis: X9 c= Z . i dom (M +* (i .--> X9)) = I by A2, Lm1; then reconsider K = M +* (i .--> X9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; A5: dom (i .--> X9) = {i} by FUNCOP_1:13; i in {i} by TARSKI:def_1; then A6: K . i = (i .--> X9) . i by A5, FUNCT_4:13 .= X9 by FUNCOP_1:72 ; K in A proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in A . j ) assume A7: j in I ; ::_thesis: K . j in A . j now__::_thesis:_(_(_j_=_i_&_K_._j_in_A_._j_)_or_(_j_<>_i_&_K_._j_in_A_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: K . j in A . j hence K . j in A . j by A4, A6; ::_thesis: verum end; case j <> i ; ::_thesis: K . j in A . j then not j in dom (i .--> X9) by A5, TARSKI:def_1; then K . j = M . j by FUNCT_4:11; hence K . j in A . j by A3, A7, PBOOLE:def_1; ::_thesis: verum end; end; end; hence K . j in A . j ; ::_thesis: verum end; then K c= Z by A1; hence X9 c= Z . i by A2, A6, PBOOLE:def_2; ::_thesis: verum end; then union (A . i) c= Z . i by ZFMISC_1:76; hence (union A) . i c= Z . i by A2, Def2; ::_thesis: verum end; theorem :: MBOOLEAN:33 for I being set for B being ManySortedSet of I for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds X /\ B = [[0]] I ) holds (union A) /\ B = [[0]] I proof let I be set ; ::_thesis: for B being ManySortedSet of I for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds X /\ B = [[0]] I ) holds (union A) /\ B = [[0]] I let B be ManySortedSet of I; ::_thesis: for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds X /\ B = [[0]] I ) holds (union A) /\ B = [[0]] I let A be V2() ManySortedSet of I; ::_thesis: ( ( for X being ManySortedSet of I st X in A holds X /\ B = [[0]] I ) implies (union A) /\ B = [[0]] I ) assume A1: for X being ManySortedSet of I st X in A holds X /\ B = [[0]] I ; ::_thesis: (union A) /\ B = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ((union_A)_/\_B)_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies ((union A) /\ B) . i = ([[0]] I) . i ) assume A2: i in I ; ::_thesis: ((union A) /\ B) . i = ([[0]] I) . i for X9 being set st X9 in A . i holds X9 misses B . i proof consider M being ManySortedSet of I such that A3: M in A by PBOOLE:134; let X9 be set ; ::_thesis: ( X9 in A . i implies X9 misses B . i ) assume A4: X9 in A . i ; ::_thesis: X9 misses B . i dom (M +* (i .--> X9)) = I by A2, Lm1; then reconsider K = M +* (i .--> X9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; A5: dom (i .--> X9) = {i} by FUNCOP_1:13; i in {i} by TARSKI:def_1; then A6: K . i = (i .--> X9) . i by A5, FUNCT_4:13 .= X9 by FUNCOP_1:72 ; K in A proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in A . j ) assume A7: j in I ; ::_thesis: K . j in A . j now__::_thesis:_(_(_j_=_i_&_K_._j_in_A_._j_)_or_(_j_<>_i_&_K_._j_in_A_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: K . j in A . j hence K . j in A . j by A4, A6; ::_thesis: verum end; case j <> i ; ::_thesis: K . j in A . j then not j in dom (i .--> X9) by A5, TARSKI:def_1; then K . j = M . j by FUNCT_4:11; hence K . j in A . j by A3, A7, PBOOLE:def_1; ::_thesis: verum end; end; end; hence K . j in A . j ; ::_thesis: verum end; then K /\ B = [[0]] I by A1; then (K . i) /\ (B . i) = ([[0]] I) . i by A2, PBOOLE:def_5; then X9 /\ (B . i) = {} by A6, PBOOLE:5; hence X9 misses B . i by XBOOLE_0:def_7; ::_thesis: verum end; then union (A . i) misses B . i by ZFMISC_1:80; then (union (A . i)) /\ (B . i) = {} by XBOOLE_0:def_7; then ((union A) . i) /\ (B . i) = {} by A2, Def2; then ((union A) /\ B) . i = {} by A2, PBOOLE:def_5; hence ((union A) /\ B) . i = ([[0]] I) . i by PBOOLE:5; ::_thesis: verum end; hence (union A) /\ B = [[0]] I by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:34 for I being set for A, B being ManySortedSet of I st A \/ B is V2() & ( for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds X /\ Y = [[0]] I ) holds union (A /\ B) = (union A) /\ (union B) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A \/ B is V2() & ( for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds X /\ Y = [[0]] I ) holds union (A /\ B) = (union A) /\ (union B) let A, B be ManySortedSet of I; ::_thesis: ( A \/ B is V2() & ( for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds X /\ Y = [[0]] I ) implies union (A /\ B) = (union A) /\ (union B) ) assume A1: A \/ B is V2() ; ::_thesis: ( ex X, Y being ManySortedSet of I st ( X <> Y & X in A \/ B & Y in A \/ B & not X /\ Y = [[0]] I ) or union (A /\ B) = (union A) /\ (union B) ) assume A2: for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds X /\ Y = [[0]] I ; ::_thesis: union (A /\ B) = (union A) /\ (union B) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (union_(A_/\_B))_._i_=_((union_A)_/\_(union_B))_._i let i be set ; ::_thesis: ( i in I implies (union (A /\ B)) . i = ((union A) /\ (union B)) . i ) assume A3: i in I ; ::_thesis: (union (A /\ B)) . i = ((union A) /\ (union B)) . i for X9, Y9 being set st X9 <> Y9 & X9 in (A . i) \/ (B . i) & Y9 in (A . i) \/ (B . i) holds X9 misses Y9 proof consider M being ManySortedSet of I such that A4: M in A \/ B by A1, PBOOLE:134; A5: i in {i} by TARSKI:def_1; let X9, Y9 be set ; ::_thesis: ( X9 <> Y9 & X9 in (A . i) \/ (B . i) & Y9 in (A . i) \/ (B . i) implies X9 misses Y9 ) assume that A6: X9 <> Y9 and A7: X9 in (A . i) \/ (B . i) and A8: Y9 in (A . i) \/ (B . i) ; ::_thesis: X9 misses Y9 ( dom (M +* (i .--> X9)) = I & dom (M +* (i .--> Y9)) = I ) by A3, Lm1; then reconsider Kx = M +* (i .--> X9), Ky = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; A9: dom (i .--> Y9) = {i} by FUNCOP_1:13; then A10: Ky . i = (i .--> Y9) . i by A5, FUNCT_4:13 .= Y9 by FUNCOP_1:72 ; A11: Ky in A \/ B proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or Ky . j in (A \/ B) . j ) assume A12: j in I ; ::_thesis: Ky . j in (A \/ B) . j now__::_thesis:_Ky_._j_in_(A_\/_B)_._j percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: Ky . j in (A \/ B) . j hence Ky . j in (A \/ B) . j by A8, A10, A12, PBOOLE:def_4; ::_thesis: verum end; suppose j <> i ; ::_thesis: Ky . j in (A \/ B) . j then not j in dom (i .--> Y9) by A9, TARSKI:def_1; then Ky . j = M . j by FUNCT_4:11; hence Ky . j in (A \/ B) . j by A4, A12, PBOOLE:def_1; ::_thesis: verum end; end; end; hence Ky . j in (A \/ B) . j ; ::_thesis: verum end; A13: dom (i .--> X9) = {i} by FUNCOP_1:13; then A14: Kx . i = (i .--> X9) . i by A5, FUNCT_4:13 .= X9 by FUNCOP_1:72 ; Kx in A \/ B proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or Kx . j in (A \/ B) . j ) assume A15: j in I ; ::_thesis: Kx . j in (A \/ B) . j now__::_thesis:_(_(_j_=_i_&_Kx_._j_in_(A_\/_B)_._j_)_or_(_j_<>_i_&_Kx_._j_in_(A_\/_B)_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: Kx . j in (A \/ B) . j hence Kx . j in (A \/ B) . j by A7, A14, A15, PBOOLE:def_4; ::_thesis: verum end; case j <> i ; ::_thesis: Kx . j in (A \/ B) . j then not j in dom (i .--> X9) by A13, TARSKI:def_1; then Kx . j = M . j by FUNCT_4:11; hence Kx . j in (A \/ B) . j by A4, A15, PBOOLE:def_1; ::_thesis: verum end; end; end; hence Kx . j in (A \/ B) . j ; ::_thesis: verum end; then Kx /\ Ky = [[0]] I by A2, A6, A14, A10, A11; then (Kx /\ Ky) . i = {} by PBOOLE:5; then X9 /\ Y9 = {} by A3, A14, A10, PBOOLE:def_5; hence X9 misses Y9 by XBOOLE_0:def_7; ::_thesis: verum end; then union ((A . i) /\ (B . i)) = (union (A . i)) /\ (union (B . i)) by ZFMISC_1:83; then union ((A . i) /\ (B . i)) = ((union A) . i) /\ (union (B . i)) by A3, Def2; then union ((A . i) /\ (B . i)) = ((union A) . i) /\ ((union B) . i) by A3, Def2; then union ((A . i) /\ (B . i)) = ((union A) /\ (union B)) . i by A3, PBOOLE:def_5; hence (union (A /\ B)) . i = ((union A) /\ (union B)) . i by A3, Lm7; ::_thesis: verum end; hence union (A /\ B) = (union A) /\ (union B) by PBOOLE:3; ::_thesis: verum end; theorem :: MBOOLEAN:35 for I being set for A, X being ManySortedSet of I for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds Y /\ X = [[0]] I ) holds X c= union A proof let I be set ; ::_thesis: for A, X being ManySortedSet of I for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds Y /\ X = [[0]] I ) holds X c= union A let A, X be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds Y /\ X = [[0]] I ) holds X c= union A let B be V2() ManySortedSet of I; ::_thesis: ( X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds Y /\ X = [[0]] I ) implies X c= union A ) assume that A1: X c= union (A \/ B) and A2: for Y being ManySortedSet of I st Y in B holds Y /\ X = [[0]] I ; ::_thesis: X c= union A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (union A) . i ) assume A3: i in I ; ::_thesis: X . i c= (union A) . i A4: for Y9 being set st Y9 in B . i holds Y9 misses X . i proof consider M being ManySortedSet of I such that A5: M in B by PBOOLE:134; let Y9 be set ; ::_thesis: ( Y9 in B . i implies Y9 misses X . i ) assume A6: Y9 in B . i ; ::_thesis: Y9 misses X . i dom (M +* (i .--> Y9)) = I by A3, Lm1; then reconsider K = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; A7: dom (i .--> Y9) = {i} by FUNCOP_1:13; i in {i} by TARSKI:def_1; then A8: K . i = (i .--> Y9) . i by A7, FUNCT_4:13 .= Y9 by FUNCOP_1:72 ; K in B proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in B . j ) assume A9: j in I ; ::_thesis: K . j in B . j now__::_thesis:_(_(_j_=_i_&_K_._j_in_B_._j_)_or_(_j_<>_i_&_K_._j_in_B_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: K . j in B . j hence K . j in B . j by A6, A8; ::_thesis: verum end; case j <> i ; ::_thesis: K . j in B . j then not j in dom (i .--> Y9) by A7, TARSKI:def_1; then K . j = M . j by FUNCT_4:11; hence K . j in B . j by A5, A9, PBOOLE:def_1; ::_thesis: verum end; end; end; hence K . j in B . j ; ::_thesis: verum end; then K /\ X = [[0]] I by A2; then (K /\ X) . i = {} by PBOOLE:5; then Y9 /\ (X . i) = {} by A3, A8, PBOOLE:def_5; hence Y9 misses X . i by XBOOLE_0:def_7; ::_thesis: verum end; X . i c= (union (A \/ B)) . i by A1, A3, PBOOLE:def_2; then X . i c= union ((A . i) \/ (B . i)) by A3, Lm6; then X . i c= union (A . i) by A4, SETFAM_1:42; hence X . i c= (union A) . i by A3, Def2; ::_thesis: verum end; theorem :: MBOOLEAN:36 for I being set for A being V2() V26() ManySortedSet of I st ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds Y c= X ) holds union A in A proof let I be set ; ::_thesis: for A being V2() V26() ManySortedSet of I st ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds Y c= X ) holds union A in A let A be V2() V26() ManySortedSet of I; ::_thesis: ( ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds Y c= X ) implies union A in A ) assume A1: for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds Y c= X ; ::_thesis: union A in A let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or (union A) . i in A . i ) assume A2: i in I ; ::_thesis: (union A) . i in A . i then i in dom A by PARTFUN1:def_2; then A . i in rng A by FUNCT_1:3; then A3: A . i is finite by FINSET_1:def_2; A4: for X9, Y9 being set st X9 in A . i & Y9 in A . i & not X9 c= Y9 holds Y9 c= X9 proof let X9, Y9 be set ; ::_thesis: ( X9 in A . i & Y9 in A . i & not X9 c= Y9 implies Y9 c= X9 ) assume that A5: X9 in A . i and A6: Y9 in A . i ; ::_thesis: ( X9 c= Y9 or Y9 c= X9 ) consider M being ManySortedSet of I such that A7: M in A by PBOOLE:134; ( dom (M +* (i .--> Y9)) = I & dom (M +* (i .--> X9)) = I ) by A2, Lm1; then reconsider K1 = M +* (i .--> X9), K2 = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; assume A8: not X9 c= Y9 ; ::_thesis: Y9 c= X9 A9: i in {i} by TARSKI:def_1; A10: dom (i .--> Y9) = {i} by FUNCOP_1:13; then A11: K2 . i = (i .--> Y9) . i by A9, FUNCT_4:13 .= Y9 by FUNCOP_1:72 ; A12: K2 in A proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K2 . j in A . j ) assume A13: j in I ; ::_thesis: K2 . j in A . j now__::_thesis:_(_(_j_=_i_&_K2_._j_in_A_._j_)_or_(_j_<>_i_&_K2_._j_in_A_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: K2 . j in A . j hence K2 . j in A . j by A6, A11; ::_thesis: verum end; case j <> i ; ::_thesis: K2 . j in A . j then not j in dom (i .--> Y9) by A10, TARSKI:def_1; then K2 . j = M . j by FUNCT_4:11; hence K2 . j in A . j by A7, A13, PBOOLE:def_1; ::_thesis: verum end; end; end; hence K2 . j in A . j ; ::_thesis: verum end; A14: dom (i .--> X9) = {i} by FUNCOP_1:13; then A15: K1 . i = (i .--> X9) . i by A9, FUNCT_4:13 .= X9 by FUNCOP_1:72 ; K1 in A proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K1 . j in A . j ) assume A16: j in I ; ::_thesis: K1 . j in A . j now__::_thesis:_(_(_j_=_i_&_K1_._j_in_A_._j_)_or_(_j_<>_i_&_K1_._j_in_A_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: K1 . j in A . j hence K1 . j in A . j by A5, A15; ::_thesis: verum end; case j <> i ; ::_thesis: K1 . j in A . j then not j in dom (i .--> X9) by A14, TARSKI:def_1; then K1 . j = M . j by FUNCT_4:11; hence K1 . j in A . j by A7, A16, PBOOLE:def_1; ::_thesis: verum end; end; end; hence K1 . j in A . j ; ::_thesis: verum end; then ( K1 c= K2 or K2 c= K1 ) by A1, A12; hence Y9 c= X9 by A2, A8, A15, A11, PBOOLE:def_2; ::_thesis: verum end; A . i <> {} by A2, PBOOLE:def_13; then union (A . i) in A . i by A3, A4, CARD_2:62; hence (union A) . i in A . i by A2, Def2; ::_thesis: verum end;