:: Definitions and Basic Properties of Boolean & Union of Many :: Sorted Sets :: by Artur Korni{\l}owicz :: :: Received April 27, 1995 :: Copyright (c) 1995-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies PBOOLE, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_0, FUNCT_4, FUNCOP_1, TARSKI, FUNCT_2, FINSET_1, SETLIM_2; notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, FUNCT_4, FUNCOP_1, PBOOLE; constructors FUNCT_4, PBOOLE, FINSET_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, FUNCOP_1, PRE_CIRC; requirements SUBSET, BOOLE; definitions PBOOLE; equalities FUNCOP_1; expansions PBOOLE; theorems CARD_2, SETFAM_1, FUNCOP_1, FRAENKEL, FUNCT_4, PBOOLE, FINSET_1, TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, PARTFUN1, RELAT_1, FUNCT_1; schemes PBOOLE; begin :: Boolean of Many Sorted Sets reserve x, y for object, I for set, A, B, X, Y for ManySortedSet of I; definition let I, A; func bool A -> ManySortedSet of I means :Def1: for i be object st i in I holds it.i = bool (A.i); existence proof deffunc V(object) = bool (A.\$1); thus ex X being ManySortedSet of I st for i be object st i in I holds X.i = V(i) from PBOOLE:sch 4; end; uniqueness proof let X, Y be ManySortedSet of I such that A1: for i be object st i in I holds X.i = bool (A.i) and A2: for i be object st i in I holds Y.i = bool (A.i); now let i be object; assume A3: i in I; hence X.i = bool (A.i) by A1 .= Y.i by A2,A3; end; hence X = Y; end; end; registration let I, A; cluster bool A -> non-empty; coherence proof let i be object such that A1: i in I; bool (A.i) is non empty; hence thesis by A1,Def1; end; end; Lm1: for i, I, X be set for M be ManySortedSet of I st i in I holds dom (M +* (i .--> X)) = I proof let i, I, X be set, M be ManySortedSet of I such that A1: i in 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; end; Lm2: for i be set st i in I holds (bool (A (\/) B)).i = bool (A.i \/ B.i) proof let i be set; assume A1: i in I; hence (bool (A (\/) B)).i = bool ((A (\/) B).i) by Def1 .= bool (A.i \/ B.i) by A1,PBOOLE:def 4; end; Lm3: for i be set st i in I holds (bool (A (/\) B)).i = bool (A.i /\ B.i) proof let i be set; assume A1: i in I; hence (bool (A (/\) B)).i = bool ((A (/\) B).i) by Def1 .= bool (A.i /\ B.i) by A1,PBOOLE:def 5; end; Lm4: for i be set st i in I holds (bool (A (\) B)).i = bool (A.i \ B.i) proof let i be set; assume A1: i in I; hence (bool (A (\) B)).i = bool ((A (\) B).i) by Def1 .= bool (A.i \ B.i) by A1,PBOOLE:def 6; end; Lm5: for i be set st i in I holds (bool (A (\+\) B)).i = bool (A.i \+\ B.i) proof let i be set; assume A1: i in I; hence (bool (A (\+\) B)).i = bool ((A (\+\) B).i) by Def1 .= bool (A.i \+\ B.i) by A1,PBOOLE:4; end; theorem Th1: :: Tarski:6 X = bool Y iff for A holds A in X iff A c= Y proof thus X = bool Y implies for A holds A in X iff A c= Y proof assume A1: X = bool Y; let A; thus A in X implies A c= Y proof assume A2: A in X; let i be object; assume A3: i in I; then A4: A.i in X.i by A2; X.i = bool (Y.i) by A1,A3,Def1; hence thesis by A4; end; assume A5: A c= Y; let i be object; assume A6: i in I; then A7: A.i c= Y.i by A5; X.i = bool (Y.i) by A1,A6,Def1; hence thesis by A7; end; assume A8: for A holds A in X iff A c= Y; now let i be object such that A9: i in I; EmptyMS I c= Y by PBOOLE:43; then A10: EmptyMS I in X by A8; for A9 be set holds A9 in X.i iff A9 c= Y.i proof let A9 be set; A11: dom (i .--> A9) = {i} by FUNCOP_1:13; dom (EmptyMS I +* (i .--> A9)) = I by A9,Lm1; then reconsider K = EmptyMS 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 proof assume A13: A9 in X.i; K in X proof let j be object such that A14: j in I; now per cases; case j = i; hence thesis by A12,A13; end; case j <> i; then not j in dom (i .--> A9) by A11,TARSKI:def 1; then K.j = EmptyMS I.j by FUNCT_4:11; hence thesis by A10,A14; end; end; hence thesis; end; then K c= Y by A8; hence thesis by A9,A12; end; assume A15: A9 c= Y.i; K c= Y proof let j be object such that A16: j in I; now per cases; case j = i; hence thesis by A12,A15; end; case j <> i; then not j in dom (i .--> A9) by A11,TARSKI:def 1; then A17: K.j = EmptyMS I.j by FUNCT_4:11; EmptyMS I c= Y by PBOOLE:43; hence thesis by A16,A17; end; end; hence thesis; end; then K in X by A8; hence thesis by A9,A12; end; then X.i = bool (Y.i) by ZFMISC_1:def 1; hence X.i = (bool Y).i by A9,Def1; end; hence thesis; end; theorem :: ZFMISC_1:1 bool EmptyMS I = I --> {{}} proof now let i be object; assume A1: i in I; then (bool EmptyMS I).i = bool (EmptyMS I.i) by Def1 .= bool{} by PBOOLE:5 .= {{}} by ZFMISC_1:1; hence (bool EmptyMS I).i = (I --> {{}}).i by A1,FUNCOP_1:7; end; hence thesis; end; theorem for x being set holds bool (I --> x) = I --> bool x proof let x be set; now let i be object; assume A1: i in 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; end; hence thesis; end; theorem :: ZFMISC_1:30 bool (I --> {x}) = I --> { {} , {x} } proof now let i be object; assume A1: i in 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; end; hence thesis; end; theorem :: ZFMISC_1:76 EmptyMS I c= A proof let i be object; assume i in I; EmptyMS I.i = {} by PBOOLE:5; hence thesis by XBOOLE_1:2; end; theorem :: ZFMISC_1:79 A c= B implies bool A c= bool B proof assume A1: A c= B; let i be object; assume A2: i in I; then A3: A.i c= B.i by A1; (bool A).i = bool (A.i) & (bool B).i = bool (B.i) by A2,Def1; hence thesis by A3,ZFMISC_1:67; end; theorem :: ZFMISC_1:81 bool A (\/) bool B c= bool (A (\/) B) proof let i be object; assume A1: i in 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 thesis by A2,ZFMISC_1:69; end; theorem :: ZFMISC_1:82 bool A (\/) bool B = bool (A (\/) B) implies for i be set st i in I holds A.i,B.i are_c=-comparable proof assume A1: bool A (\/) bool B = bool (A (\/) B); let i be set such that A2: i in I; 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 thesis by ZFMISC_1:70; end; theorem :: ZFMISC_1:83 bool (A (/\) B) = bool A (/\) bool B proof now let i be object; assume A1: i in 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; end; hence thesis; end; theorem :: ZFMISC_1:84 bool (A (\) B) c= (I --> {{}}) (\/) (bool A (\) bool B) proof let i be object; assume A1: i in 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 thesis by A2,ZFMISC_1:72; end; theorem X c= A (\) B iff X c= A & X misses B proof thus X c= A (\) B implies X c= A & X misses B proof assume X c= A (\) B; then A1: X in bool (A (\) B) by Th1; thus X c= A proof let i be object; assume A2: i in I; then X.i in (bool (A (\) B)).i by A1; then X.i in bool (A.i \ B.i) by A2,Lm4; hence thesis by XBOOLE_1:106; end; let i be object; assume A3: i in I; then X.i in (bool (A (\) B)).i by A1; then X.i in bool (A.i \ B.i) by A3,Lm4; hence thesis by XBOOLE_1:106; end; assume A4: X c= A & X misses B; let i be object; assume A5: i in I; then X.i c= A.i & X.i misses B.i by A4; then X.i c= A.i \ B.i by XBOOLE_1:86; hence thesis by A5,PBOOLE:def 6; end; theorem :: ZFMISC_1:86 bool (A (\) B) (\/) bool (B (\) A) c= bool (A (\+\) B) proof let i be object; assume A1: i in 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 thesis by A2,ZFMISC_1:73; end; theorem :: ZFMISC_1:87 X c= A (\+\) B iff X c= A (\/) B & X misses A (/\) B proof thus X c= A (\+\) B implies X c= A (\/) B & X misses A (/\) B proof assume X c= A (\+\) B; then A1: X in bool (A (\+\) B) by Th1; thus X c= A (\/) B proof let i be object; assume A2: i in I; then X.i in (bool (A (\+\) B)).i by A1; 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 thesis by A2,PBOOLE:def 4; end; let i be object; assume A3: i in I; then X.i in (bool (A (\+\) B)).i by A1; 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 thesis by A3,PBOOLE:def 5; end; assume that A4: X c= A (\/) B and A5: X misses A (/\) B; let i be object; assume A6: i in I; then X.i misses (A (/\) B).i by A5; then A7: X.i misses A.i /\ B.i by A6,PBOOLE:def 5; X.i c= (A (\/) B).i by A4,A6; 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 thesis by A6,PBOOLE:4; end; theorem :: ZFMISC_1:89 X c= A or Y c= A implies X (/\) Y c= A proof assume A1: X c= A or Y c= A; per cases by A1; suppose A2: X c= A; let i be object; assume A3: i in I; then X.i c= A.i by A2; then X.i /\ Y.i c= A.i by XBOOLE_1:108; hence thesis by A3,PBOOLE:def 5; end; suppose A4: Y c= A; let i be object; assume A5: i in I; then Y.i c= A.i by A4; then X.i /\ Y.i c= A.i by XBOOLE_1:108; hence thesis by A5,PBOOLE:def 5; end; end; theorem :: ZFMISC_1:90 X c= A implies X (\) Y c= A proof assume A1: X c= A; let i be object; assume A2: i in I; then X.i c= A.i by A1; then X.i \ Y.i c= A.i by XBOOLE_1:109; hence thesis by A2,PBOOLE:def 6; end; theorem :: ZFMISC_1:91 X c= A & Y c= A implies X (\+\) Y c= A proof assume A1: X c= A & Y c= A; let i be object; assume A2: i in I; then X.i c= A.i & Y.i c= A.i by A1; 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 thesis; end; theorem :: ZFMISC_1:105 [|X, Y|] c= bool bool (X (\/) Y) proof let i be object; assume A1: i in 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 thesis by A2,ZFMISC_1:86; end; theorem :: FIN_TOPO:4 X c= A iff X in bool A proof thus X c= A implies X in bool A proof assume A1: X c= A; let i be object; assume A2: i in I; then X.i c= A.i by A1; then X.i in bool (A.i); hence thesis by A2,Def1; end; assume A3: X in bool A; let i be object; assume A4: i in I; then X.i in (bool A).i by A3; then X.i in bool (A.i) by A4,Def1; hence thesis; end; theorem :: FRAENKEL:5 (Funcs)(A,B) c= bool [|A, B|] proof let i be object; assume A1: i in 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 thesis by A2,FRAENKEL:2; end; begin :: Union of Many Sorted Sets definition let I, A; func union A -> ManySortedSet of I means :Def2: for i be object st i in I holds it.i = union (A.i); existence proof deffunc V(object) = union (A.\$1); thus ex X being ManySortedSet of I st for i be object st i in I holds X.i = V (i) from PBOOLE:sch 4; end; uniqueness proof let X, Y be ManySortedSet of I such that A1: for i be object st i in I holds X.i = union (A.i) and A2: for i be object st i in I holds Y.i = union (A.i); now let i be object; assume A3: i in I; hence X.i = union (A.i) by A1 .= Y.i by A2,A3; end; hence X = Y; end; end; registration let I; cluster union EmptyMS I -> empty-yielding; coherence proof let i be object; A1: union (EmptyMS I.i) is empty by PBOOLE:5,ZFMISC_1:2; assume i in I; hence thesis by A1,Def2; end; end; Lm6: for i be set st i in I holds (union (A (\/) B)).i = union (A.i \/ B.i) proof let i be set; assume A1: i in I; hence (union (A (\/) B)).i = union ((A (\/) B).i) by Def2 .= union (A.i \/ B.i) by A1,PBOOLE:def 4; end; Lm7: for i be set st i in I holds (union (A (/\) B)).i = union (A.i /\ B.i) proof let i be set; assume A1: i in I; hence (union (A (/\) B)).i = union ((A (/\) B).i) by Def2 .= union (A.i /\ B.i) by A1,PBOOLE:def 5; end; theorem :: Tarski:def 4 A in union X iff ex Y st A in Y & Y in X proof thus A in union X implies ex Y st A in Y & Y in X proof defpred P[object,object] means ex B being set st B = \$2 & A.\$1 in B & \$2 in X.\$1; assume A1: A in union X; A2: for i being object st i in I ex Y being object st P[i,Y] proof let i be object; assume A3: i in I; then A.i in (union X).i by A1; then A.i in union (X.i) by A3,Def2; then consider B being set such that A4: A.i in B & B in X.i by TARSKI:def 4; take B; thus thesis by A4; end; consider K be ManySortedSet of I such that A5: for i be object st i in I holds P[i,K.i] from PBOOLE:sch 3(A2); take K; thus A in K proof let i be object; assume i in I; then P[i,K.i] by A5; hence thesis; end; thus K in X proof let i be object; assume i in I; then P[i,K.i] by A5; hence thesis; end; end; given Y such that A6: A in Y & Y in X; let i be object; assume A7: i in I; then A.i in Y.i & Y.i in X.i by A6; then A.i in union (X.i) by TARSKI:def 4; hence thesis by A7,Def2; end; theorem :: ZFMISC_1:2 union EmptyMS I = EmptyMS I proof now let i be object; assume i in I; hence (union EmptyMS I).i = union (EmptyMS I.i) by Def2 .= {} by PBOOLE:5,ZFMISC_1:2 .= EmptyMS I.i by PBOOLE:5; end; hence thesis; end; theorem for x being set holds union (I --> x) = I --> union x proof let x be set; now let i be object; assume A1: i in 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; end; hence thesis; end; theorem :: ZFMISC_1:31 union (I --> {x}) = I --> x proof now let i be object; assume A1: i in 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; end; hence thesis; end; theorem :: ZFMISC_1:32 union (I --> { {x},{y} }) = I --> {x,y} proof now let i be object; assume A1: i in 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; end; hence thesis; end; theorem :: ZFMISC_1:92 X in A implies X c= union A proof assume A1: X in A; let i be object; assume A2: i in I; then X.i in A.i by A1; then X.i c= union (A.i) by ZFMISC_1:74; hence thesis by A2,Def2; end; theorem :: ZFMISC_1:95 A c= B implies union A c= union B proof assume A1: A c= B; let i be object; assume A2: i in I; then A.i c= B.i by A1; then union (A.i) c= union (B.i) by ZFMISC_1:77; then (union A).i c= union (B.i) by A2,Def2; hence thesis by A2,Def2; end; theorem :: ZFMISC_1:96 union (A (\/) B) = union A (\/) union B proof now let i be object; assume A1: i in 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; end; hence thesis; end; theorem :: ZFMISC_1:97 union (A (/\) B) c= union A (/\) union B proof let i be object; assume A1: i in 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 thesis by A2,ZFMISC_1:79; end; theorem :: ZFMISC_1:99 union bool A = A proof now let i be object; assume A1: i in 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; end; hence thesis; end; theorem :: ZFMISC_1:100 A c= bool union A proof let i be object; assume A1: i in I; then (bool union A).i = bool ((union A).i) by Def1 .= bool union (A.i) by A1,Def2; hence thesis by ZFMISC_1:82; end; theorem :: LATTICE4:1 union Y c= A & X in Y implies X c= A proof assume that A1: union Y c= A and A2: X in Y; let i be object; assume A3: i in I; then (union Y).i c= A.i by A1; then A4: union (Y.i) c= A.i by A3,Def2; X.i in Y.i by A2,A3; hence thesis by A4,SETFAM_1:41; end; theorem :: ZFMISC_1:94 for Z be ManySortedSet of I for A be non-empty ManySortedSet of I holds (for X be ManySortedSet of I st X in A holds X c= Z) implies union A c= Z proof let Z be ManySortedSet of I, A be non-empty ManySortedSet of I; assume A1: for X be ManySortedSet of I st X in A holds X c= Z; let i be object such that A2: i in I; for X9 be set st X9 in A.i holds X9 c= Z.i proof consider M be ManySortedSet of I such that A3: M in A by PBOOLE:134; let X9 be set such that A4: X9 in A.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 object such that A7: j in I; now per cases; case j = i; hence thesis by A4,A6; end; case j <> i; then not j in dom (i .--> X9) by A5,TARSKI:def 1; then K.j = M.j by FUNCT_4:11; hence thesis by A3,A7; end; end; hence thesis; end; then K c= Z by A1; hence thesis by A2,A6; end; then union (A.i) c= Z.i by ZFMISC_1:76; hence thesis by A2,Def2; end; theorem :: ZFMISC_1:98 for B be ManySortedSet of I for A be non-empty ManySortedSet of I st for X be ManySortedSet of I st X in A holds X (/\) B = EmptyMS I holds union(A) (/\) B = EmptyMS I proof let B be ManySortedSet of I, A be non-empty ManySortedSet of I; assume A1: for X be ManySortedSet of I st X in A holds X (/\) B = EmptyMS I; now let i be object such that A2: i in I; for X9 be set st X9 in A.i holds X9 misses (B.i) proof consider M be ManySortedSet of I such that A3: M in A by PBOOLE:134; let X9 be set such that A4: X9 in A.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 object such that A7: j in I; now per cases; case j = i; hence thesis by A4,A6; end; case j <> i; then not j in dom (i .--> X9) by A5,TARSKI:def 1; then K.j = M.j by FUNCT_4:11; hence thesis by A3,A7; end; end; hence thesis; end; then K (/\) B = EmptyMS I by A1; then K.i /\ B.i = EmptyMS I.i by A2,PBOOLE:def 5; then X9 /\ B.i = {} by A6,PBOOLE:5; hence thesis by XBOOLE_0:def 7; 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 = EmptyMS I.i by PBOOLE:5; end; hence thesis; end; theorem :: ZFMISC_1:101 for A, B be ManySortedSet of I st A (\/) B is non-empty & for X, Y be ManySortedSet of I st X <> Y & X in A (\/) B & Y in A (\/) B holds X (/\) Y = EmptyMS I holds union(A (/\) B) = union A (/\) union B proof let A, B be ManySortedSet of I such that A1: A (\/) B is non-empty; assume A2: for X, Y be ManySortedSet of I st X <> Y & X in A (\/) B & Y in A (\/) B holds X (/\) Y = EmptyMS I; now let i be object such that A3: i in I; for X9, Y9 be set st X9 <> Y9 & X9 in A.i \/ B.i & Y9 in A.i \/ B.i holds X9 misses Y9 proof consider M be 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 such that A6: X9 <> Y9 and A7: X9 in A.i \/ B.i and A8: Y9 in A.i \/ B.i; 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 object such that A12: j in I; now per cases; suppose j = i; hence thesis by A8,A10,A12,PBOOLE:def 4; end; suppose j <> i; then not j in dom (i .--> Y9) by A9,TARSKI:def 1; then Ky.j = M.j by FUNCT_4:11; hence thesis by A4,A12; end; end; hence thesis; 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 object such that A15: j in I; now per cases; case j = i; hence thesis by A7,A14,A15,PBOOLE:def 4; end; case j <> i; then not j in dom (i .--> X9) by A13,TARSKI:def 1; then Kx.j = M.j by FUNCT_4:11; hence thesis by A4,A15; end; end; hence thesis; end; then Kx (/\) Ky = EmptyMS 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 thesis by XBOOLE_0:def 7; 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; end; hence thesis; end; theorem :: LOPCLSET:31 for A, X be ManySortedSet of I for B be non-empty ManySortedSet of I holds (X c= union (A (\/) B) & for Y be ManySortedSet of I st Y in B holds Y (/\) X = EmptyMS I) implies X c= union A proof let A, X be ManySortedSet of I, B be non-empty ManySortedSet of I; assume that A1: X c= union (A (\/) B) and A2: for Y be ManySortedSet of I st Y in B holds Y (/\) X = EmptyMS I; let i be object; assume A3: i in I; A4: for Y9 be set st Y9 in B.i holds Y9 misses X.i proof consider M be ManySortedSet of I such that A5: M in B by PBOOLE:134; let Y9 be set such that A6: Y9 in B.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 object such that A9: j in I; now per cases; case j = i; hence thesis by A6,A8; end; case j <> i; then not j in dom (i .--> Y9) by A7,TARSKI:def 1; then K.j = M.j by FUNCT_4:11; hence thesis by A5,A9; end; end; hence thesis; end; then K (/\) X = EmptyMS I by A2; then (K (/\) X).i = {} by PBOOLE:5; then Y9 /\ X.i = {} by A3,A8,PBOOLE:def 5; hence thesis by XBOOLE_0:def 7; end; X.i c= (union (A (\/) B)).i by A1,A3; 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 thesis by A3,Def2; end; theorem :: RLVECT_3:34 for A be finite-yielding non-empty ManySortedSet of I st (for X, Y be ManySortedSet of I st X in A & Y in A holds X c= Y or Y c= X) holds union A in A proof let A be finite-yielding non-empty ManySortedSet of I such that A1: for X, Y be ManySortedSet of I st X in A & Y in A holds X c= Y or Y c= X; let i be object; assume A2: i in 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 be set st X9 in A.i & Y9 in A.i holds X9 c= Y9 or Y9 c= X9 proof let X9, Y9 be set such that A5: X9 in A.i and A6: Y9 in A.i; consider M be 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; 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 object such that A13: j in I; per cases; suppose j = i; hence thesis by A6,A11; end; suppose j <> i; then not j in dom (i .--> Y9) by A10,TARSKI:def 1; then K2.j = M.j by FUNCT_4:11; hence thesis by A7,A13; end; 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 object such that A16: j in I; per cases; suppose j = i; hence thesis by A5,A15; end; suppose j <> i; then not j in dom (i .--> X9) by A14,TARSKI:def 1; then K1.j = M.j by FUNCT_4:11; hence thesis by A7,A16; end; end; then K1 c= K2 or K2 c= K1 by A1,A12; hence thesis by A2,A8,A15,A11; end; A.i <> {} by A2,PBOOLE:def 13; then union (A.i) in A.i by A3,A4,CARD_2:62; hence thesis by A2,Def2; end;