:: MSSUBFAM semantic presentation begin registration let I be set ; let F be ManySortedFunction of I; cluster doms F -> I -defined ; coherence doms F is I -defined proof dom (doms F) = dom F by FUNCT_6:59 .= I by PARTFUN1:def_2 ; hence doms F is I -defined by RELAT_1:def_18; ::_thesis: verum end; cluster rngs F -> I -defined ; coherence rngs F is I -defined proof dom (rngs F) = dom F by FUNCT_6:60 .= I by PARTFUN1:def_2 ; hence rngs F is I -defined by RELAT_1:def_18; ::_thesis: verum end; end; registration let I be set ; let F be ManySortedFunction of I; cluster doms F -> I -defined total for I -defined Function; coherence for b1 being I -defined Function st b1 = doms F holds b1 is total proof dom (doms F) = dom F by FUNCT_6:59 .= I by PARTFUN1:def_2 ; hence for b1 being I -defined Function st b1 = doms F holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; cluster rngs F -> I -defined total for I -defined Function; coherence for b1 being I -defined Function st b1 = rngs F holds b1 is total proof dom (rngs F) = dom F by FUNCT_6:60 .= I by PARTFUN1:def_2 ; hence for b1 being I -defined Function st b1 = rngs F holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; end; scheme :: MSSUBFAM:sch 1 MSFExFunc{ F1() -> set , F2() -> ManySortedSet of F1(), F3() -> ManySortedSet of F1(), P1[ set , set , set ] } : ex F being ManySortedFunction of F2(),F3() st for i being set st i in F1() holds ex f being Function of (F2() . i),(F3() . i) st ( f = F . i & ( for x being set st x in F2() . i holds P1[f . x,x,i] ) ) provided A1: for i being set st i in F1() holds for x being set st x in F2() . i holds ex y being set st ( y in F3() . i & P1[y,x,i] ) proof defpred S1[ set , set ] means ex f1 being Function of (F2() . $1),(F3() . $1) st ( f1 = $2 & ( for x being set st x in F2() . $1 holds P1[f1 . x,x,$1] ) ); A2: now__::_thesis:_for_i_being_set_st_i_in_F1()_holds_ ex_j_being_set_st_S1[i,j] let i be set ; ::_thesis: ( i in F1() implies ex j being set st S1[j,b2] ) assume A3: i in F1() ; ::_thesis: ex j being set st S1[j,b2] percases ( not F3() . i is empty or F3() . i is empty ) ; suppose not F3() . i is empty ; ::_thesis: ex j being set st S1[j,b2] then reconsider bb = F3() . i as non empty set ; defpred S2[ set , set ] means P1[$2,$1,i]; A4: for e being set st e in F2() . i holds ex u being set st ( u in bb & S2[e,u] ) by A1, A3; consider ff being Function of (F2() . i),bb such that A5: for e being set st e in F2() . i holds S2[e,ff . e] from FUNCT_2:sch_1(A4); reconsider fff = ff as Function of (F2() . i),(F3() . i) ; reconsider j = fff as set ; take j = j; ::_thesis: S1[i,j] thus S1[i,j] by A5; ::_thesis: verum end; supposeA6: F3() . i is empty ; ::_thesis: ex j being set st S1[j,b2] A7: now__::_thesis:_for_x_being_set_holds_not_x_in_F2()_._i let x be set ; ::_thesis: not x in F2() . i for y being set holds ( not y in F3() . i or not P1[y,x,i] ) by A6; hence not x in F2() . i by A1, A3; ::_thesis: verum end; then F2() . i = {} by XBOOLE_0:def_1; then reconsider fff = {} as Function of (F2() . i),(F3() . i) by RELSET_1:12; reconsider j = fff as set ; take j = j; ::_thesis: S1[i,j] thus S1[i,j] ::_thesis: verum proof take fff ; ::_thesis: ( fff = j & ( for x being set st x in F2() . i holds P1[fff . x,x,i] ) ) thus fff = j ; ::_thesis: for x being set st x in F2() . i holds P1[fff . x,x,i] thus for x being set st x in F2() . i holds P1[fff . x,x,i] by A7; ::_thesis: verum end; end; end; end; consider F being ManySortedSet of F1() such that A8: for i being set st i in F1() holds S1[i,F . i] from PBOOLE:sch_3(A2); F is ManySortedFunction of F2(),F3() proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in F1() or F . i is Element of bool [:(F2() . i),(F3() . i):] ) assume i in F1() ; ::_thesis: F . i is Element of bool [:(F2() . i),(F3() . i):] then ex f being Function of (F2() . i),(F3() . i) st ( f = F . i & ( for x being set st x in F2() . i holds P1[f . x,x,i] ) ) by A8; hence F . i is Element of bool [:(F2() . i),(F3() . i):] ; ::_thesis: verum end; then reconsider F = F as ManySortedFunction of F2(),F3() ; take F ; ::_thesis: for i being set st i in F1() holds ex f being Function of (F2() . i),(F3() . i) st ( f = F . i & ( for x being set st x in F2() . i holds P1[f . x,x,i] ) ) thus for i being set st i in F1() holds ex f being Function of (F2() . i),(F3() . i) st ( f = F . i & ( for x being set st x in F2() . i holds P1[f . x,x,i] ) ) by A8; ::_thesis: verum end; theorem :: MSSUBFAM:1 for I being set for sf being Subset-Family of I st sf <> {} holds Intersect sf c= union sf proof let I be set ; ::_thesis: for sf being Subset-Family of I st sf <> {} holds Intersect sf c= union sf let sf be Subset-Family of I; ::_thesis: ( sf <> {} implies Intersect sf c= union sf ) assume sf <> {} ; ::_thesis: Intersect sf c= union sf then Intersect sf = meet sf by SETFAM_1:def_9; hence Intersect sf c= union sf by SETFAM_1:2; ::_thesis: verum end; theorem :: MSSUBFAM:2 for I, G being set for sf being Subset-Family of I st G in sf holds Intersect sf c= G proof let I, G be set ; ::_thesis: for sf being Subset-Family of I st G in sf holds Intersect sf c= G let sf be Subset-Family of I; ::_thesis: ( G in sf implies Intersect sf c= G ) assume A1: G in sf ; ::_thesis: Intersect sf c= G then meet sf = Intersect sf by SETFAM_1:def_9; hence Intersect sf c= G by A1, SETFAM_1:3; ::_thesis: verum end; theorem :: MSSUBFAM:3 for I being set for sf being Subset-Family of I st {} in sf holds Intersect sf = {} proof let I be set ; ::_thesis: for sf being Subset-Family of I st {} in sf holds Intersect sf = {} let sf be Subset-Family of I; ::_thesis: ( {} in sf implies Intersect sf = {} ) assume A1: {} in sf ; ::_thesis: Intersect sf = {} then Intersect sf = meet sf by SETFAM_1:def_9; hence Intersect sf = {} by A1, SETFAM_1:4; ::_thesis: verum end; theorem :: MSSUBFAM:4 for I being set for sf being Subset-Family of I for Z being Subset of I st ( for Z1 being set st Z1 in sf holds Z c= Z1 ) holds Z c= Intersect sf proof let I be set ; ::_thesis: for sf being Subset-Family of I for Z being Subset of I st ( for Z1 being set st Z1 in sf holds Z c= Z1 ) holds Z c= Intersect sf let sf be Subset-Family of I; ::_thesis: for Z being Subset of I st ( for Z1 being set st Z1 in sf holds Z c= Z1 ) holds Z c= Intersect sf let Z be Subset of I; ::_thesis: ( ( for Z1 being set st Z1 in sf holds Z c= Z1 ) implies Z c= Intersect sf ) assume A1: for Z1 being set st Z1 in sf holds Z c= Z1 ; ::_thesis: Z c= Intersect sf percases ( sf <> {} or sf = {} ) ; supposeA2: sf <> {} ; ::_thesis: Z c= Intersect sf then Intersect sf = meet sf by SETFAM_1:def_9; hence Z c= Intersect sf by A1, A2, SETFAM_1:5; ::_thesis: verum end; suppose sf = {} ; ::_thesis: Z c= Intersect sf then Intersect sf = I by SETFAM_1:def_9; hence Z c= Intersect sf ; ::_thesis: verum end; end; end; theorem :: MSSUBFAM:5 for I, G being set for sf being Subset-Family of I st sf <> {} & ( for Z1 being set st Z1 in sf holds G c= Z1 ) holds G c= Intersect sf proof let I, G be set ; ::_thesis: for sf being Subset-Family of I st sf <> {} & ( for Z1 being set st Z1 in sf holds G c= Z1 ) holds G c= Intersect sf let sf be Subset-Family of I; ::_thesis: ( sf <> {} & ( for Z1 being set st Z1 in sf holds G c= Z1 ) implies G c= Intersect sf ) assume that A1: sf <> {} and A2: for Z1 being set st Z1 in sf holds G c= Z1 ; ::_thesis: G c= Intersect sf Intersect sf = meet sf by A1, SETFAM_1:def_9; hence G c= Intersect sf by A1, A2, SETFAM_1:5; ::_thesis: verum end; theorem :: MSSUBFAM:6 for I, G, H being set for sf being Subset-Family of I st G in sf & G c= H holds Intersect sf c= H proof let I, G, H be set ; ::_thesis: for sf being Subset-Family of I st G in sf & G c= H holds Intersect sf c= H let sf be Subset-Family of I; ::_thesis: ( G in sf & G c= H implies Intersect sf c= H ) assume that A1: G in sf and A2: G c= H ; ::_thesis: Intersect sf c= H Intersect sf = meet sf by A1, SETFAM_1:def_9; hence Intersect sf c= H by A1, A2, SETFAM_1:7; ::_thesis: verum end; theorem :: MSSUBFAM:7 for I, G, H being set for sf being Subset-Family of I st G in sf & G misses H holds Intersect sf misses H proof let I, G, H be set ; ::_thesis: for sf being Subset-Family of I st G in sf & G misses H holds Intersect sf misses H let sf be Subset-Family of I; ::_thesis: ( G in sf & G misses H implies Intersect sf misses H ) assume that A1: G in sf and A2: G misses H ; ::_thesis: Intersect sf misses H Intersect sf = meet sf by A1, SETFAM_1:def_9; hence Intersect sf misses H by A1, A2, SETFAM_1:8; ::_thesis: verum end; theorem :: MSSUBFAM:8 for I being set for sh, sf, sg being Subset-Family of I st sh = sf \/ sg holds Intersect sh = (Intersect sf) /\ (Intersect sg) proof let I be set ; ::_thesis: for sh, sf, sg being Subset-Family of I st sh = sf \/ sg holds Intersect sh = (Intersect sf) /\ (Intersect sg) let sh, sf, sg be Subset-Family of I; ::_thesis: ( sh = sf \/ sg implies Intersect sh = (Intersect sf) /\ (Intersect sg) ) assume A1: sh = sf \/ sg ; ::_thesis: Intersect sh = (Intersect sf) /\ (Intersect sg) percases ( ( sf = {} & sg = {} ) or ( sf <> {} & sg = {} ) or ( sf = {} & sg <> {} ) or ( sf <> {} & sg <> {} ) ) ; suppose ( sf = {} & sg = {} ) ; ::_thesis: Intersect sh = (Intersect sf) /\ (Intersect sg) hence Intersect sh = (Intersect sf) /\ (Intersect sg) by A1; ::_thesis: verum end; supposeA2: ( sf <> {} & sg = {} ) ; ::_thesis: Intersect sh = (Intersect sf) /\ (Intersect sg) hence Intersect sh = meet sf by A1, SETFAM_1:def_9 .= (meet sf) /\ I by XBOOLE_1:28 .= (Intersect sf) /\ I by A2, SETFAM_1:def_9 .= (Intersect sf) /\ (Intersect sg) by A2, SETFAM_1:def_9 ; ::_thesis: verum end; supposeA3: ( sf = {} & sg <> {} ) ; ::_thesis: Intersect sh = (Intersect sf) /\ (Intersect sg) hence Intersect sh = meet sg by A1, SETFAM_1:def_9 .= I /\ (meet sg) by XBOOLE_1:28 .= I /\ (Intersect sg) by A3, SETFAM_1:def_9 .= (Intersect sf) /\ (Intersect sg) by A3, SETFAM_1:def_9 ; ::_thesis: verum end; supposeA4: ( sf <> {} & sg <> {} ) ; ::_thesis: Intersect sh = (Intersect sf) /\ (Intersect sg) then A5: Intersect sg = meet sg by SETFAM_1:def_9; ( Intersect sh = meet sh & Intersect sf = meet sf ) by A1, A4, SETFAM_1:def_9; hence Intersect sh = (Intersect sf) /\ (Intersect sg) by A1, A4, A5, SETFAM_1:9; ::_thesis: verum end; end; end; theorem :: MSSUBFAM:9 for I being set for sf being Subset-Family of I for v being Subset of I st sf = {v} holds Intersect sf = v proof let I be set ; ::_thesis: for sf being Subset-Family of I for v being Subset of I st sf = {v} holds Intersect sf = v let sf be Subset-Family of I; ::_thesis: for v being Subset of I st sf = {v} holds Intersect sf = v let v be Subset of I; ::_thesis: ( sf = {v} implies Intersect sf = v ) assume A1: sf = {v} ; ::_thesis: Intersect sf = v then Intersect sf = meet sf by SETFAM_1:def_9; hence Intersect sf = v by A1, SETFAM_1:10; ::_thesis: verum end; theorem :: MSSUBFAM:10 for I being set for sf being Subset-Family of I for v, w being Subset of I st sf = {v,w} holds Intersect sf = v /\ w proof let I be set ; ::_thesis: for sf being Subset-Family of I for v, w being Subset of I st sf = {v,w} holds Intersect sf = v /\ w let sf be Subset-Family of I; ::_thesis: for v, w being Subset of I st sf = {v,w} holds Intersect sf = v /\ w let v, w be Subset of I; ::_thesis: ( sf = {v,w} implies Intersect sf = v /\ w ) assume A1: sf = {v,w} ; ::_thesis: Intersect sf = v /\ w then Intersect sf = meet sf by SETFAM_1:def_9; hence Intersect sf = v /\ w by A1, SETFAM_1:11; ::_thesis: verum end; theorem :: MSSUBFAM:11 for I being set for A, B being ManySortedSet of I st A in B holds A is Element of B proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A in B holds A is Element of B let A, B be ManySortedSet of I; ::_thesis: ( A in B implies A is Element of B ) assume A1: A in B ; ::_thesis: A is Element of B let i be set ; :: according to PBOOLE:def_14 ::_thesis: ( not i in I or A . i is Element of B . i ) assume i in I ; ::_thesis: A . i is Element of B . i hence A . i is Element of B . i by A1, PBOOLE:def_1; ::_thesis: verum end; theorem :: MSSUBFAM:12 for I being set for A being ManySortedSet of I for B being V8() ManySortedSet of I st A is Element of B holds A in B proof let I be set ; ::_thesis: for A being ManySortedSet of I for B being V8() ManySortedSet of I st A is Element of B holds A in B let A be ManySortedSet of I; ::_thesis: for B being V8() ManySortedSet of I st A is Element of B holds A in B let B be V8() ManySortedSet of I; ::_thesis: ( A is Element of B implies A in B ) assume A1: A is Element of B ; ::_thesis: A in B let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in B . i ) assume A2: i in I ; ::_thesis: A . i in B . i then A3: B . i <> {} ; A . i is Element of B . i by A1, A2, PBOOLE:def_14; hence A . i in B . i by A3; ::_thesis: verum end; theorem Th13: :: MSSUBFAM:13 for i, I being set for F being ManySortedFunction of I for f being Function st i in I & f = F . i holds (rngs F) . i = rng f proof let i, I be set ; ::_thesis: for F being ManySortedFunction of I for f being Function st i in I & f = F . i holds (rngs F) . i = rng f let F be ManySortedFunction of I; ::_thesis: for f being Function st i in I & f = F . i holds (rngs F) . i = rng f A1: dom F = I by PARTFUN1:def_2; let f be Function; ::_thesis: ( i in I & f = F . i implies (rngs F) . i = rng f ) assume ( i in I & f = F . i ) ; ::_thesis: (rngs F) . i = rng f hence (rngs F) . i = rng f by A1, FUNCT_6:22; ::_thesis: verum end; theorem Th14: :: MSSUBFAM:14 for i, I being set for F being ManySortedFunction of I for f being Function st i in I & f = F . i holds (doms F) . i = dom f proof let i, I be set ; ::_thesis: for F being ManySortedFunction of I for f being Function st i in I & f = F . i holds (doms F) . i = dom f let F be ManySortedFunction of I; ::_thesis: for f being Function st i in I & f = F . i holds (doms F) . i = dom f A1: dom F = I by PARTFUN1:def_2; let f be Function; ::_thesis: ( i in I & f = F . i implies (doms F) . i = dom f ) assume ( i in I & f = F . i ) ; ::_thesis: (doms F) . i = dom f hence (doms F) . i = dom f by A1, FUNCT_6:22; ::_thesis: verum end; theorem :: MSSUBFAM:15 for I being set for F, G being ManySortedFunction of I holds G ** F is ManySortedFunction of I proof let I be set ; ::_thesis: for F, G being ManySortedFunction of I holds G ** F is ManySortedFunction of I let F, G be ManySortedFunction of I; ::_thesis: G ** F is ManySortedFunction of I dom (G ** F) = (dom F) /\ (dom G) by PBOOLE:def_19 .= I /\ (dom G) by PARTFUN1:def_2 .= I /\ I by PARTFUN1:def_2 .= I ; hence G ** F is ManySortedFunction of I by PARTFUN1:def_2, RELAT_1:def_18; ::_thesis: verum end; theorem :: MSSUBFAM:16 for I being set for A being V8() ManySortedSet of I for F being ManySortedFunction of A, [[0]] I holds F = [[0]] I proof let I be set ; ::_thesis: for A being V8() ManySortedSet of I for F being ManySortedFunction of A, [[0]] I holds F = [[0]] I let A be V8() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A, [[0]] I holds F = [[0]] I let F be ManySortedFunction of A, [[0]] I; ::_thesis: F = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ F_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies F . i = ([[0]] I) . i ) assume i in I ; ::_thesis: F . i = ([[0]] I) . i then reconsider f = F . i as Function of (A . i),(([[0]] I) . i) by PBOOLE:def_15; f = {} ; hence F . i = ([[0]] I) . i ; ::_thesis: verum end; hence F = [[0]] I by PBOOLE:3; ::_thesis: verum end; theorem :: MSSUBFAM:17 for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of I st A is_transformable_to B & F is ManySortedFunction of A,B holds ( doms F = A & rngs F c= B ) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for F being ManySortedFunction of I st A is_transformable_to B & F is ManySortedFunction of A,B holds ( doms F = A & rngs F c= B ) let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of I st A is_transformable_to B & F is ManySortedFunction of A,B holds ( doms F = A & rngs F c= B ) let F be ManySortedFunction of I; ::_thesis: ( A is_transformable_to B & F is ManySortedFunction of A,B implies ( doms F = A & rngs F c= B ) ) assume that A1: A is_transformable_to B and A2: F is ManySortedFunction of A,B ; ::_thesis: ( doms F = A & rngs F c= B ) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (doms_F)_._i_=_A_._i let i be set ; ::_thesis: ( i in I implies (doms F) . i = A . i ) assume A3: i in I ; ::_thesis: (doms F) . i = A . i then reconsider f = F . i as Function of (A . i),(B . i) by A2, PBOOLE:def_15; A4: ( B . i = {} implies A . i = {} ) by A1, A3, PZFMISC1:def_3; thus (doms F) . i = dom f by A3, Th14 .= A . i by A4, FUNCT_2:def_1 ; ::_thesis: verum end; hence doms F = A by PBOOLE:3; ::_thesis: rngs F c= B let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (rngs F) . i c= B . i ) assume A5: i in I ; ::_thesis: (rngs F) . i c= B . i then reconsider f = F . i as Function of (A . i),(B . i) by A2, PBOOLE:def_15; rng f c= B . i by RELAT_1:def_19; hence (rngs F) . i c= B . i by A5, Th13; ::_thesis: verum end; begin registration let I be set ; cluster Relation-like V9() I -defined Function-like total -> V36() for set ; coherence for b1 being ManySortedSet of I st b1 is V9() holds b1 is V36() proof let A be ManySortedSet of I; ::_thesis: ( A is V9() implies A is V36() ) assume A1: A is V9() ; ::_thesis: A is V36() let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or A . i is finite ) assume i in I ; ::_thesis: A . i is finite reconsider B = A . i as empty set by A1; B is finite ; hence A . i is finite ; ::_thesis: verum end; end; registration let I be set ; cluster [[0]] I -> V9() V36() ; coherence ( [[0]] I is empty-yielding & [[0]] I is finite-yielding ) ; end; registration let I be set ; let A be ManySortedSet of I; cluster Relation-like V9() I -defined Function-like total V36() for ManySortedSubset of A; existence ex b1 being ManySortedSubset of A st ( b1 is V9() & b1 is V36() ) proof set x = [[0]] I; [[0]] I c= A by PBOOLE:43; then reconsider x = [[0]] I as ManySortedSubset of A by PBOOLE:def_18; take x ; ::_thesis: ( x is V9() & x is V36() ) thus ( x is V9() & x is V36() ) ; ::_thesis: verum end; end; theorem Th18: :: MSSUBFAM:18 for I being set for A, B being ManySortedSet of I st A c= B & B is V36() holds A is V36() proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A c= B & B is V36() holds A is V36() let A, B be ManySortedSet of I; ::_thesis: ( A c= B & B is V36() implies A is V36() ) assume A1: ( A c= B & B is V36() ) ; ::_thesis: A is V36() let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or A . i is finite ) assume i in I ; ::_thesis: A . i is finite then ( A . i c= B . i & B . i is finite ) by A1, PBOOLE:def_2; hence A . i is finite ; ::_thesis: verum end; registration let I be set ; let A be V36() ManySortedSet of I; cluster -> V36() for ManySortedSubset of A; coherence for b1 being ManySortedSubset of A holds b1 is V36() proof let x be ManySortedSubset of A; ::_thesis: x is V36() reconsider x9 = x as ManySortedSet of I ; x9 c= A by PBOOLE:def_18; hence x is V36() by Th18; ::_thesis: verum end; end; registration let I be set ; let A, B be V36() ManySortedSet of I; clusterA \/ B -> V36() ; coherence A \/ B is finite-yielding proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or (A \/ B) . i is finite ) assume A1: i in I ; ::_thesis: (A \/ B) . i is finite (A . i) \/ (B . i) is finite ; hence (A \/ B) . i is finite by A1, PBOOLE:def_4; ::_thesis: verum end; end; registration let I be set ; let A be ManySortedSet of I; let B be V36() ManySortedSet of I; clusterA /\ B -> V36() ; coherence A /\ B is finite-yielding proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or (A /\ B) . i is finite ) assume A1: i in I ; ::_thesis: (A /\ B) . i is finite (A . i) /\ (B . i) is finite ; hence (A /\ B) . i is finite by A1, PBOOLE:def_5; ::_thesis: verum end; end; registration let I be set ; let B be ManySortedSet of I; let A be V36() ManySortedSet of I; clusterA /\ B -> V36() ; coherence A /\ B is finite-yielding ; end; registration let I be set ; let B be ManySortedSet of I; let A be V36() ManySortedSet of I; clusterA \ B -> V36() ; coherence A \ B is finite-yielding proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or (A \ B) . i is finite ) assume A1: i in I ; ::_thesis: (A \ B) . i is finite (A . i) \ (B . i) is finite ; hence (A \ B) . i is finite by A1, PBOOLE:def_6; ::_thesis: verum end; end; registration let I be set ; let F be ManySortedFunction of I; let A be V36() ManySortedSet of I; clusterF .:.: A -> V36() ; coherence F .:.: A is finite-yielding proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or (F .:.: A) . i is finite ) assume A1: i in I ; ::_thesis: (F .:.: A) . i is finite reconsider f = F . i as Function ; f .: (A . i) is finite ; hence (F .:.: A) . i is finite by A1, PBOOLE:def_20; ::_thesis: verum end; end; registration let I be set ; let A, B be V36() ManySortedSet of I; cluster[|A,B|] -> V36() ; coherence [|A,B|] is finite-yielding proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or [|A,B|] . i is finite ) assume A1: i in I ; ::_thesis: [|A,B|] . i is finite [:(A . i),(B . i):] is finite ; hence [|A,B|] . i is finite by A1, PBOOLE:def_16; ::_thesis: verum end; end; theorem :: MSSUBFAM:19 for I being set for B, A being ManySortedSet of I st B is V8() & [|A,B|] is V36() holds A is V36() proof let I be set ; ::_thesis: for B, A being ManySortedSet of I st B is V8() & [|A,B|] is V36() holds A is V36() let B, A be ManySortedSet of I; ::_thesis: ( B is V8() & [|A,B|] is V36() implies A is V36() ) assume that A1: B is V8() and A2: [|A,B|] is V36() ; ::_thesis: A is V36() let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or A . i is finite ) assume A3: i in I ; ::_thesis: A . i is finite [|A,B|] . i is finite by A2; then [:(A . i),(B . i):] is finite by A3, PBOOLE:def_16; hence A . i is finite by A1, A3; ::_thesis: verum end; theorem :: MSSUBFAM:20 for I being set for A, B being ManySortedSet of I st A is V8() & [|A,B|] is V36() holds B is V36() proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is V8() & [|A,B|] is V36() holds B is V36() let A, B be ManySortedSet of I; ::_thesis: ( A is V8() & [|A,B|] is V36() implies B is V36() ) assume that A1: A is V8() and A2: [|A,B|] is V36() ; ::_thesis: B is V36() let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or B . i is finite ) assume A3: i in I ; ::_thesis: B . i is finite [|A,B|] . i is finite by A2; then [:(A . i),(B . i):] is finite by A3, PBOOLE:def_16; hence B . i is finite by A1, A3; ::_thesis: verum end; theorem Th21: :: MSSUBFAM:21 for I being set for A being ManySortedSet of I holds ( A is V36() iff bool A is V36() ) proof let I be set ; ::_thesis: for A being ManySortedSet of I holds ( A is V36() iff bool A is V36() ) let A be ManySortedSet of I; ::_thesis: ( A is V36() iff bool A is V36() ) thus ( A is V36() implies bool A is V36() ) ::_thesis: ( bool A is V36() implies A is V36() ) proof assume A1: A is V36() ; ::_thesis: bool A is V36() let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or (bool A) . i is finite ) assume A2: i in I ; ::_thesis: (bool A) . i is finite A . i is finite by A1; then bool (A . i) is finite ; hence (bool A) . i is finite by A2, MBOOLEAN:def_1; ::_thesis: verum end; assume A3: bool A is V36() ; ::_thesis: A is V36() let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or A . i is finite ) assume A4: i in I ; ::_thesis: A . i is finite (bool A) . i is finite by A3; then bool (A . i) is finite by A4, MBOOLEAN:def_1; hence A . i is finite ; ::_thesis: verum end; registration let I be set ; let M be V36() ManySortedSet of I; cluster bool M -> V36() ; coherence bool M is finite-yielding by Th21; end; theorem :: MSSUBFAM:22 for I being set for A being V8() ManySortedSet of I st A is V36() & ( for M being ManySortedSet of I st M in A holds M is V36() ) holds union A is V36() proof let I be set ; ::_thesis: for A being V8() ManySortedSet of I st A is V36() & ( for M being ManySortedSet of I st M in A holds M is V36() ) holds union A is V36() let A be V8() ManySortedSet of I; ::_thesis: ( A is V36() & ( for M being ManySortedSet of I st M in A holds M is V36() ) implies union A is V36() ) assume that A1: A is V36() and A2: for M being ManySortedSet of I st M in A holds M is V36() ; ::_thesis: union A is V36() let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or (union A) . i is finite ) assume A3: i in I ; ::_thesis: (union A) . i is finite A4: for X9 being set st X9 in A . i holds X9 is finite proof consider M being ManySortedSet of I such that A5: M in A by PBOOLE:134; let X9 be set ; ::_thesis: ( X9 in A . i implies X9 is finite ) assume A6: X9 in A . i ; ::_thesis: X9 is finite dom (M +* (i .--> X9)) = I by A3, PZFMISC1:1; then reconsider K = M +* (i .--> X9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; A7: dom (i .--> X9) = {i} by FUNCOP_1:13; i in {i} by TARSKI:def_1; then A8: K . i = (i .--> X9) . i by A7, 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 A9: 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 A6, A8; ::_thesis: verum end; case j <> i ; ::_thesis: K . j in A . j then not j in dom (i .--> X9) by A7, TARSKI:def_1; then K . j = M . j by FUNCT_4:11; hence K . j in A . j by A5, A9, PBOOLE:def_1; ::_thesis: verum end; end; end; hence K . j in A . j ; ::_thesis: verum end; then K is V36() by A2; hence X9 is finite by A8; ::_thesis: verum end; A . i is finite by A1; then union (A . i) is finite by A4, FINSET_1:7; hence (union A) . i is finite by A3, MBOOLEAN:def_2; ::_thesis: verum end; theorem :: MSSUBFAM:23 for I being set for A being ManySortedSet of I st union A is V36() holds ( A is V36() & ( for M being ManySortedSet of I st M in A holds M is V36() ) ) proof let I be set ; ::_thesis: for A being ManySortedSet of I st union A is V36() holds ( A is V36() & ( for M being ManySortedSet of I st M in A holds M is V36() ) ) let A be ManySortedSet of I; ::_thesis: ( union A is V36() implies ( A is V36() & ( for M being ManySortedSet of I st M in A holds M is V36() ) ) ) assume A1: union A is V36() ; ::_thesis: ( A is V36() & ( for M being ManySortedSet of I st M in A holds M is V36() ) ) thus A is V36() ::_thesis: for M being ManySortedSet of I st M in A holds M is V36() proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or A . i is finite ) assume A2: i in I ; ::_thesis: A . i is finite (union A) . i is finite by A1; then union (A . i) is finite by A2, MBOOLEAN:def_2; hence A . i is finite by FINSET_1:7; ::_thesis: verum end; let M be ManySortedSet of I; ::_thesis: ( M in A implies M is V36() ) assume A3: M in A ; ::_thesis: M is V36() let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or M . i is finite ) assume A4: i in I ; ::_thesis: M . i is finite (union A) . i is finite by A1; then A5: union (A . i) is finite by A4, MBOOLEAN:def_2; M . i in A . i by A3, A4, PBOOLE:def_1; hence M . i is finite by A5, FINSET_1:7; ::_thesis: verum end; theorem :: MSSUBFAM:24 for I being set for F being ManySortedFunction of I st doms F is V36() holds rngs F is V36() proof let I be set ; ::_thesis: for F being ManySortedFunction of I st doms F is V36() holds rngs F is V36() let F be ManySortedFunction of I; ::_thesis: ( doms F is V36() implies rngs F is V36() ) assume A1: doms F is V36() ; ::_thesis: rngs F is V36() let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or (rngs F) . i is finite ) assume A2: i in I ; ::_thesis: (rngs F) . i is finite reconsider f = F . i as Function ; (doms F) . i is finite by A1; then dom f is finite by A2, Th14; then rng f is finite by FINSET_1:8; hence (rngs F) . i is finite by A2, Th13; ::_thesis: verum end; theorem :: MSSUBFAM:25 for I being set for A being ManySortedSet of I for F being ManySortedFunction of I st A c= rngs F & ( for i being set for f being Function st i in I & f = F . i holds f " (A . i) is finite ) holds A is V36() proof let I be set ; ::_thesis: for A being ManySortedSet of I for F being ManySortedFunction of I st A c= rngs F & ( for i being set for f being Function st i in I & f = F . i holds f " (A . i) is finite ) holds A is V36() let A be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of I st A c= rngs F & ( for i being set for f being Function st i in I & f = F . i holds f " (A . i) is finite ) holds A is V36() let F be ManySortedFunction of I; ::_thesis: ( A c= rngs F & ( for i being set for f being Function st i in I & f = F . i holds f " (A . i) is finite ) implies A is V36() ) assume that A1: A c= rngs F and A2: for i being set for f being Function st i in I & f = F . i holds f " (A . i) is finite ; ::_thesis: A is V36() let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or A . i is finite ) assume A3: i in I ; ::_thesis: A . i is finite reconsider f = F . i as Function ; (rngs F) . i = rng f by A3, Th13; then A4: A . i c= rng f by A1, A3, PBOOLE:def_2; f " (A . i) is finite by A2, A3; hence A . i is finite by A4, FINSET_1:9; ::_thesis: verum end; registration let I be set ; let A, B be V36() ManySortedSet of I; cluster (Funcs) (A,B) -> V36() ; coherence (Funcs) (A,B) is finite-yielding proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or ((Funcs) (A,B)) . i is finite ) assume i in I ; ::_thesis: ((Funcs) (A,B)) . i is finite then ( ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) & A . i is finite ) by PBOOLE:def_17; hence ((Funcs) (A,B)) . i is finite by FRAENKEL:6; ::_thesis: verum end; end; registration let I be set ; let A, B be V36() ManySortedSet of I; clusterA \+\ B -> V36() ; coherence A \+\ B is finite-yielding ; end; theorem :: MSSUBFAM:26 for I being set for X, Y, Z being ManySortedSet of I st X is V36() & X c= [|Y,Z|] holds ex A, B being ManySortedSet of I st ( A is V36() & A c= Y & B is V36() & B c= Z & X c= [|A,B|] ) proof let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X is V36() & X c= [|Y,Z|] holds ex A, B being ManySortedSet of I st ( A is V36() & A c= Y & B is V36() & B c= Z & X c= [|A,B|] ) let X, Y, Z be ManySortedSet of I; ::_thesis: ( X is V36() & X c= [|Y,Z|] implies ex A, B being ManySortedSet of I st ( A is V36() & A c= Y & B is V36() & B c= Z & X c= [|A,B|] ) ) assume that A1: X is V36() and A2: X c= [|Y,Z|] ; ::_thesis: ex A, B being ManySortedSet of I st ( A is V36() & A c= Y & B is V36() & B c= Z & X c= [|A,B|] ) defpred S1[ set , set ] means ex b being set st ( $2 is finite & $2 c= Y . $1 & b is finite & b c= Z . $1 & X . $1 c= [:$2,b:] ); A3: for i being set st i in I holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume A4: i in I ; ::_thesis: ex j being set st S1[i,j] then X . i c= [|Y,Z|] . i by A2, PBOOLE:def_2; then A5: X . i c= [:(Y . i),(Z . i):] by A4, PBOOLE:def_16; X . i is finite by A1; hence ex j being set st S1[i,j] by A5, FINSET_1:13; ::_thesis: verum end; consider A being ManySortedSet of I such that A6: for i being set st i in I holds S1[i,A . i] from PBOOLE:sch_3(A3); defpred S2[ set , set ] means ( A . $1 is finite & A . $1 c= Y . $1 & $2 is finite & $2 c= Z . $1 & X . $1 c= [:(A . $1),$2:] ); A7: for i being set st i in I holds ex j being set st S2[i,j] by A6; consider B being ManySortedSet of I such that A8: for i being set st i in I holds S2[i,B . i] from PBOOLE:sch_3(A7); take A ; ::_thesis: ex B being ManySortedSet of I st ( A is V36() & A c= Y & B is V36() & B c= Z & X c= [|A,B|] ) take B ; ::_thesis: ( A is V36() & A c= Y & B is V36() & B c= Z & X c= [|A,B|] ) thus A is V36() ::_thesis: ( A c= Y & B is V36() & B c= Z & X c= [|A,B|] ) proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or A . i is finite ) assume i in I ; ::_thesis: A . i is finite hence A . i is finite by A8; ::_thesis: verum end; thus A c= Y ::_thesis: ( B is V36() & B c= Z & X c= [|A,B|] ) proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= Y . i ) assume i in I ; ::_thesis: A . i c= Y . i hence A . i c= Y . i by A8; ::_thesis: verum end; thus B is V36() ::_thesis: ( B c= Z & X c= [|A,B|] ) proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or B . i is finite ) assume i in I ; ::_thesis: B . i is finite hence B . i is finite by A8; ::_thesis: verum end; thus B c= Z ::_thesis: X c= [|A,B|] proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or B . i c= Z . i ) assume i in I ; ::_thesis: B . i c= Z . i hence B . i c= Z . i by A8; ::_thesis: verum end; thus X c= [|A,B|] ::_thesis: verum proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= [|A,B|] . i ) assume A9: i in I ; ::_thesis: X . i c= [|A,B|] . i then X . i c= [:(A . i),(B . i):] by A8; hence X . i c= [|A,B|] . i by A9, PBOOLE:def_16; ::_thesis: verum end; end; theorem :: MSSUBFAM:27 for I being set for X, Y, Z being ManySortedSet of I st X is V36() & X c= [|Y,Z|] holds ex A being ManySortedSet of I st ( A is V36() & A c= Y & X c= [|A,Z|] ) proof let I be set ; ::_thesis: for X, Y, Z being ManySortedSet of I st X is V36() & X c= [|Y,Z|] holds ex A being ManySortedSet of I st ( A is V36() & A c= Y & X c= [|A,Z|] ) let X, Y, Z be ManySortedSet of I; ::_thesis: ( X is V36() & X c= [|Y,Z|] implies ex A being ManySortedSet of I st ( A is V36() & A c= Y & X c= [|A,Z|] ) ) assume that A1: X is V36() and A2: X c= [|Y,Z|] ; ::_thesis: ex A being ManySortedSet of I st ( A is V36() & A c= Y & X c= [|A,Z|] ) defpred S1[ set , set ] means ( $2 is finite & $2 c= Y . $1 & X . $1 c= [:$2,(Z . $1):] ); A3: for i being set st i in I holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume A4: i in I ; ::_thesis: ex j being set st S1[i,j] then X . i c= [|Y,Z|] . i by A2, PBOOLE:def_2; then A5: X . i c= [:(Y . i),(Z . i):] by A4, PBOOLE:def_16; X . i is finite by A1; then consider A9 being set such that A6: ( A9 is finite & A9 c= Y . i & X . i c= [:A9,(Z . i):] ) by A5, FINSET_1:14; take A9 ; ::_thesis: S1[i,A9] thus S1[i,A9] by A6; ::_thesis: verum end; consider A being ManySortedSet of I such that A7: for i being set st i in I holds S1[i,A . i] from PBOOLE:sch_3(A3); take A ; ::_thesis: ( A is V36() & A c= Y & X c= [|A,Z|] ) thus A is V36() ::_thesis: ( A c= Y & X c= [|A,Z|] ) proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or A . i is finite ) assume i in I ; ::_thesis: A . i is finite hence A . i is finite by A7; ::_thesis: verum end; thus A c= Y ::_thesis: X c= [|A,Z|] proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= Y . i ) assume i in I ; ::_thesis: A . i c= Y . i hence A . i c= Y . i by A7; ::_thesis: verum end; thus X c= [|A,Z|] ::_thesis: verum proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= [|A,Z|] . i ) assume A8: i in I ; ::_thesis: X . i c= [|A,Z|] . i then X . i c= [:(A . i),(Z . i):] by A7; hence X . i c= [|A,Z|] . i by A8, PBOOLE:def_16; ::_thesis: verum end; end; theorem :: MSSUBFAM:28 for I being set for M being V8() V36() ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds B c= A ) holds ex m being ManySortedSet of I st ( m in M & ( for K being ManySortedSet of I st K in M holds m c= K ) ) proof let I be set ; ::_thesis: for M being V8() V36() ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds B c= A ) holds ex m being ManySortedSet of I st ( m in M & ( for K being ManySortedSet of I st K in M holds m c= K ) ) let M be V8() V36() ManySortedSet of I; ::_thesis: ( ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds B c= A ) implies ex m being ManySortedSet of I st ( m in M & ( for K being ManySortedSet of I st K in M holds m c= K ) ) ) assume A1: for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds B c= A ; ::_thesis: ex m being ManySortedSet of I st ( m in M & ( for K being ManySortedSet of I st K in M holds m c= K ) ) defpred S1[ set , set ] means ( $2 in M . $1 & ( for D9 being set st D9 in M . $1 holds $2 c= D9 ) ); A2: for i being set st i in I holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume A3: i in I ; ::_thesis: ex j being set st S1[i,j] M . i is c=-linear proof consider c9 being ManySortedSet of I such that A4: c9 in M by PBOOLE:134; consider b9 being ManySortedSet of I such that A5: b9 in M by PBOOLE:134; let B9, C9 be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not B9 in M . i or not C9 in M . i or B9,C9 are_c=-comparable ) assume that A6: B9 in M . i and A7: C9 in M . i ; ::_thesis: B9,C9 are_c=-comparable A8: dom (i .--> B9) = {i} by FUNCOP_1:13; set qc = c9 +* (i .--> C9); dom (c9 +* (i .--> C9)) = I by A3, PZFMISC1:1; then reconsider qc = c9 +* (i .--> C9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; A9: dom (i .--> C9) = {i} by FUNCOP_1:13; i in {i} by TARSKI:def_1; then A10: qc . i = (i .--> C9) . i by A9, FUNCT_4:13 .= C9 by FUNCOP_1:72 ; A11: qc in M proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or qc . j in M . j ) assume A12: j in I ; ::_thesis: qc . j in M . j now__::_thesis:_(_(_j_=_i_&_qc_._j_in_M_._j_)_or_(_j_<>_i_&_qc_._j_in_M_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: qc . j in M . j hence qc . j in M . j by A7, A10; ::_thesis: verum end; case j <> i ; ::_thesis: qc . j in M . j then not j in dom (i .--> C9) by A9, TARSKI:def_1; then qc . j = c9 . j by FUNCT_4:11; hence qc . j in M . j by A4, A12, PBOOLE:def_1; ::_thesis: verum end; end; end; hence qc . j in M . j ; ::_thesis: verum end; set qb = b9 +* (i .--> B9); dom (b9 +* (i .--> B9)) = I by A3, PZFMISC1:1; then reconsider qb = b9 +* (i .--> B9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; assume A13: not B9 c= C9 ; :: according to XBOOLE_0:def_9 ::_thesis: C9 c= B9 i in {i} by TARSKI:def_1; then A14: qb . i = (i .--> B9) . i by A8, FUNCT_4:13 .= B9 by FUNCOP_1:72 ; qb in M proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or qb . j in M . j ) assume A15: j in I ; ::_thesis: qb . j in M . j now__::_thesis:_(_(_j_=_i_&_qb_._j_in_M_._j_)_or_(_j_<>_i_&_qb_._j_in_M_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: qb . j in M . j hence qb . j in M . j by A6, A14; ::_thesis: verum end; case j <> i ; ::_thesis: qb . j in M . j then not j in dom (i .--> B9) by A8, TARSKI:def_1; then qb . j = b9 . j by FUNCT_4:11; hence qb . j in M . j by A5, A15, PBOOLE:def_1; ::_thesis: verum end; end; end; hence qb . j in M . j ; ::_thesis: verum end; then ( qb c= qc or qc c= qb ) by A1, A11; hence C9 c= B9 by A3, A13, A14, A10, PBOOLE:def_2; ::_thesis: verum end; then consider m9 being set such that A16: ( m9 in M . i & ( for D9 being set st D9 in M . i holds m9 c= D9 ) ) by A3, FINSET_1:11; take m9 ; ::_thesis: S1[i,m9] thus S1[i,m9] by A16; ::_thesis: verum end; consider m being ManySortedSet of I such that A17: for i being set st i in I holds S1[i,m . i] from PBOOLE:sch_3(A2); take m ; ::_thesis: ( m in M & ( for K being ManySortedSet of I st K in M holds m c= K ) ) thus m in M ::_thesis: for K being ManySortedSet of I st K in M holds m c= K proof let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or m . i in M . i ) assume i in I ; ::_thesis: m . i in M . i hence m . i in M . i by A17; ::_thesis: verum end; thus for C being ManySortedSet of I st C in M holds m c= C ::_thesis: verum proof let C be ManySortedSet of I; ::_thesis: ( C in M implies m c= C ) assume A18: C in M ; ::_thesis: m c= C let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or m . i c= C . i ) assume A19: i in I ; ::_thesis: m . i c= C . i then C . i in M . i by A18, PBOOLE:def_1; hence m . i c= C . i by A17, A19; ::_thesis: verum end; end; theorem :: MSSUBFAM:29 for I being set for M being V8() V36() ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds B c= A ) holds ex m being ManySortedSet of I st ( m in M & ( for K being ManySortedSet of I st K in M holds K c= m ) ) proof let I be set ; ::_thesis: for M being V8() V36() ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds B c= A ) holds ex m being ManySortedSet of I st ( m in M & ( for K being ManySortedSet of I st K in M holds K c= m ) ) let M be V8() V36() ManySortedSet of I; ::_thesis: ( ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds B c= A ) implies ex m being ManySortedSet of I st ( m in M & ( for K being ManySortedSet of I st K in M holds K c= m ) ) ) assume A1: for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds B c= A ; ::_thesis: ex m being ManySortedSet of I st ( m in M & ( for K being ManySortedSet of I st K in M holds K c= m ) ) defpred S1[ set , set ] means ( $2 in M . $1 & ( for D9 being set st D9 in M . $1 holds D9 c= $2 ) ); A2: for i being set st i in I holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume A3: i in I ; ::_thesis: ex j being set st S1[i,j] M . i is c=-linear proof consider c9 being ManySortedSet of I such that A4: c9 in M by PBOOLE:134; consider b9 being ManySortedSet of I such that A5: b9 in M by PBOOLE:134; let B9, C9 be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not B9 in M . i or not C9 in M . i or B9,C9 are_c=-comparable ) assume that A6: B9 in M . i and A7: C9 in M . i ; ::_thesis: B9,C9 are_c=-comparable A8: dom (i .--> B9) = {i} by FUNCOP_1:13; set qc = c9 +* (i .--> C9); dom (c9 +* (i .--> C9)) = I by A3, PZFMISC1:1; then reconsider qc = c9 +* (i .--> C9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; A9: dom (i .--> C9) = {i} by FUNCOP_1:13; i in {i} by TARSKI:def_1; then A10: qc . i = (i .--> C9) . i by A9, FUNCT_4:13 .= C9 by FUNCOP_1:72 ; A11: qc in M proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or qc . j in M . j ) assume A12: j in I ; ::_thesis: qc . j in M . j now__::_thesis:_(_(_j_=_i_&_qc_._j_in_M_._j_)_or_(_j_<>_i_&_qc_._j_in_M_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: qc . j in M . j hence qc . j in M . j by A7, A10; ::_thesis: verum end; case j <> i ; ::_thesis: qc . j in M . j then not j in dom (i .--> C9) by A9, TARSKI:def_1; then qc . j = c9 . j by FUNCT_4:11; hence qc . j in M . j by A4, A12, PBOOLE:def_1; ::_thesis: verum end; end; end; hence qc . j in M . j ; ::_thesis: verum end; set qb = b9 +* (i .--> B9); dom (b9 +* (i .--> B9)) = I by A3, PZFMISC1:1; then reconsider qb = b9 +* (i .--> B9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; assume A13: not B9 c= C9 ; :: according to XBOOLE_0:def_9 ::_thesis: C9 c= B9 i in {i} by TARSKI:def_1; then A14: qb . i = (i .--> B9) . i by A8, FUNCT_4:13 .= B9 by FUNCOP_1:72 ; qb in M proof let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or qb . j in M . j ) assume A15: j in I ; ::_thesis: qb . j in M . j now__::_thesis:_(_(_j_=_i_&_qb_._j_in_M_._j_)_or_(_j_<>_i_&_qb_._j_in_M_._j_)_) percases ( j = i or j <> i ) ; case j = i ; ::_thesis: qb . j in M . j hence qb . j in M . j by A6, A14; ::_thesis: verum end; case j <> i ; ::_thesis: qb . j in M . j then not j in dom (i .--> B9) by A8, TARSKI:def_1; then qb . j = b9 . j by FUNCT_4:11; hence qb . j in M . j by A5, A15, PBOOLE:def_1; ::_thesis: verum end; end; end; hence qb . j in M . j ; ::_thesis: verum end; then ( qb c= qc or qc c= qb ) by A1, A11; hence C9 c= B9 by A3, A13, A14, A10, PBOOLE:def_2; ::_thesis: verum end; then consider m9 being set such that A16: ( m9 in M . i & ( for D9 being set st D9 in M . i holds D9 c= m9 ) ) by A3, FINSET_1:12; take m9 ; ::_thesis: S1[i,m9] thus S1[i,m9] by A16; ::_thesis: verum end; consider m being ManySortedSet of I such that A17: for i being set st i in I holds S1[i,m . i] from PBOOLE:sch_3(A2); take m ; ::_thesis: ( m in M & ( for K being ManySortedSet of I st K in M holds K c= m ) ) thus m in M ::_thesis: for K being ManySortedSet of I st K in M holds K c= m proof let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or m . i in M . i ) assume i in I ; ::_thesis: m . i in M . i hence m . i in M . i by A17; ::_thesis: verum end; thus for K being ManySortedSet of I st K in M holds K c= m ::_thesis: verum proof let K be ManySortedSet of I; ::_thesis: ( K in M implies K c= m ) assume A18: K in M ; ::_thesis: K c= m let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or K . i c= m . i ) assume A19: i in I ; ::_thesis: K . i c= m . i then K . i in M . i by A18, PBOOLE:def_1; hence K . i c= m . i by A17, A19; ::_thesis: verum end; end; theorem :: MSSUBFAM:30 for I being set for F being ManySortedFunction of I for Z being ManySortedSet of I st Z is V36() & Z c= rngs F holds ex Y being ManySortedSet of I st ( Y c= doms F & Y is V36() & F .:.: Y = Z ) proof let I be set ; ::_thesis: for F being ManySortedFunction of I for Z being ManySortedSet of I st Z is V36() & Z c= rngs F holds ex Y being ManySortedSet of I st ( Y c= doms F & Y is V36() & F .:.: Y = Z ) let F be ManySortedFunction of I; ::_thesis: for Z being ManySortedSet of I st Z is V36() & Z c= rngs F holds ex Y being ManySortedSet of I st ( Y c= doms F & Y is V36() & F .:.: Y = Z ) let Z be ManySortedSet of I; ::_thesis: ( Z is V36() & Z c= rngs F implies ex Y being ManySortedSet of I st ( Y c= doms F & Y is V36() & F .:.: Y = Z ) ) assume that A1: Z is V36() and A2: Z c= rngs F ; ::_thesis: ex Y being ManySortedSet of I st ( Y c= doms F & Y is V36() & F .:.: Y = Z ) defpred S1[ set , set ] means ex f being Function st ( f = F . $1 & $2 c= (doms F) . $1 & $2 is finite & f .: $2 = Z . $1 ); A3: for i being set st i in I holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) reconsider f = F . i as Function ; assume A4: i in I ; ::_thesis: ex j being set st S1[i,j] then rng f = (rngs F) . i by Th13; then A5: Z . i c= rng f by A2, A4, PBOOLE:def_2; Z . i is finite by A1; then consider y being set such that A6: ( y c= dom f & y is finite & f .: y = Z . i ) by A5, ORDERS_1:85; take y ; ::_thesis: S1[i,y] take f ; ::_thesis: ( f = F . i & y c= (doms F) . i & y is finite & f .: y = Z . i ) thus f = F . i ; ::_thesis: ( y c= (doms F) . i & y is finite & f .: y = Z . i ) thus ( y c= (doms F) . i & y is finite & f .: y = Z . i ) by A4, A6, Th14; ::_thesis: verum end; consider Y being ManySortedSet of I such that A7: for i being set st i in I holds S1[i,Y . i] from PBOOLE:sch_3(A3); take Y ; ::_thesis: ( Y c= doms F & Y is V36() & F .:.: Y = Z ) thus Y c= doms F ::_thesis: ( Y is V36() & F .:.: Y = Z ) proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or Y . i c= (doms F) . i ) assume i in I ; ::_thesis: Y . i c= (doms F) . i then ex f being Function st ( f = F . i & Y . i c= (doms F) . i & Y . i is finite & f .: (Y . i) = Z . i ) by A7; hence Y . i c= (doms F) . i ; ::_thesis: verum end; thus Y is V36() ::_thesis: F .:.: Y = Z proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or Y . i is finite ) assume i in I ; ::_thesis: Y . i is finite then ex f being Function st ( f = F . i & Y . i c= (doms F) . i & Y . i is finite & f .: (Y . i) = Z . i ) by A7; hence Y . i is finite ; ::_thesis: verum end; now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (F_.:.:_Y)_._i_=_Z_._i let i be set ; ::_thesis: ( i in I implies (F .:.: Y) . i = Z . i ) assume A8: i in I ; ::_thesis: (F .:.: Y) . i = Z . i then ex f being Function st ( f = F . i & Y . i c= (doms F) . i & Y . i is finite & f .: (Y . i) = Z . i ) by A7; hence (F .:.: Y) . i = Z . i by A8, PBOOLE:def_20; ::_thesis: verum end; hence F .:.: Y = Z by PBOOLE:3; ::_thesis: verum end; begin definition let I be set ; let M be ManySortedSet of I; mode MSSubsetFamily of M is ManySortedSubset of bool M; end; registration let I be set ; let M be ManySortedSet of I; cluster Relation-like V8() I -defined Function-like total for ManySortedSubset of bool M; existence not for b1 being MSSubsetFamily of M holds b1 is V8() proof bool M is ManySortedSubset of bool M by PBOOLE:def_18; hence not for b1 being MSSubsetFamily of M holds b1 is V8() ; ::_thesis: verum end; end; definition let I be set ; let M be ManySortedSet of I; :: original: bool redefine func bool M -> MSSubsetFamily of M; coherence bool M is MSSubsetFamily of M by PBOOLE:def_18; end; registration let I be set ; let M be ManySortedSet of I; cluster Relation-like V9() I -defined Function-like total V36() for ManySortedSubset of bool M; existence ex b1 being MSSubsetFamily of M st ( b1 is V9() & b1 is V36() ) proof [[0]] I c= bool M by PBOOLE:43; then [[0]] I is ManySortedSubset of bool M by PBOOLE:def_18; hence ex b1 being MSSubsetFamily of M st ( b1 is V9() & b1 is V36() ) ; ::_thesis: verum end; end; theorem :: MSSUBFAM:31 for I being set for M being ManySortedSet of I holds [[0]] I is V9() V36() MSSubsetFamily of M proof let I be set ; ::_thesis: for M being ManySortedSet of I holds [[0]] I is V9() V36() MSSubsetFamily of M let M be ManySortedSet of I; ::_thesis: [[0]] I is V9() V36() MSSubsetFamily of M [[0]] I c= bool M by PBOOLE:43; hence [[0]] I is V9() V36() MSSubsetFamily of M by PBOOLE:def_18; ::_thesis: verum end; registration let I be set ; let M be V36() ManySortedSet of I; cluster Relation-like V8() I -defined Function-like total V36() for ManySortedSubset of bool M; existence ex b1 being MSSubsetFamily of M st ( b1 is V8() & b1 is V36() ) proof bool M is MSSubsetFamily of M ; hence ex b1 being MSSubsetFamily of M st ( b1 is V8() & b1 is V36() ) ; ::_thesis: verum end; end; definition let I be non empty set ; let M be ManySortedSet of I; let SF be MSSubsetFamily of M; let i be Element of I; :: original: . redefine funcSF . i -> Subset-Family of (M . i); coherence SF . i is Subset-Family of (M . i) proof SF c= bool M by PBOOLE:def_18; then SF . i c= (bool M) . i by PBOOLE:def_2; hence SF . i is Subset-Family of (M . i) by MBOOLEAN:def_1; ::_thesis: verum end; end; theorem Th32: :: MSSUBFAM:32 for i, I being set for M being ManySortedSet of I for SF being MSSubsetFamily of M st i in I holds SF . i is Subset-Family of (M . i) proof let i, I be set ; ::_thesis: for M being ManySortedSet of I for SF being MSSubsetFamily of M st i in I holds SF . i is Subset-Family of (M . i) let M be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M st i in I holds SF . i is Subset-Family of (M . i) let SF be MSSubsetFamily of M; ::_thesis: ( i in I implies SF . i is Subset-Family of (M . i) ) assume A1: i in I ; ::_thesis: SF . i is Subset-Family of (M . i) SF c= bool M by PBOOLE:def_18; then SF . i c= (bool M) . i by A1, PBOOLE:def_2; hence SF . i is Subset-Family of (M . i) by A1, MBOOLEAN:def_1; ::_thesis: verum end; theorem Th33: :: MSSUBFAM:33 for I being set for A, M being ManySortedSet of I for SF being MSSubsetFamily of M st A in SF holds A is ManySortedSubset of M proof let I be set ; ::_thesis: for A, M being ManySortedSet of I for SF being MSSubsetFamily of M st A in SF holds A is ManySortedSubset of M let A, M be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M st A in SF holds A is ManySortedSubset of M let SF be MSSubsetFamily of M; ::_thesis: ( A in SF implies A is ManySortedSubset of M ) A1: SF c= bool M by PBOOLE:def_18; assume A in SF ; ::_thesis: A is ManySortedSubset of M then A in bool M by A1, PBOOLE:9; then A c= M by MBOOLEAN:18; hence A is ManySortedSubset of M by PBOOLE:def_18; ::_thesis: verum end; theorem Th34: :: MSSUBFAM:34 for I being set for M being ManySortedSet of I for SF, SG being MSSubsetFamily of M holds SF \/ SG is MSSubsetFamily of M proof let I be set ; ::_thesis: for M being ManySortedSet of I for SF, SG being MSSubsetFamily of M holds SF \/ SG is MSSubsetFamily of M let M be ManySortedSet of I; ::_thesis: for SF, SG being MSSubsetFamily of M holds SF \/ SG is MSSubsetFamily of M let SF, SG be MSSubsetFamily of M; ::_thesis: SF \/ SG is MSSubsetFamily of M ( SF c= bool M & SG c= bool M ) by PBOOLE:def_18; then SF \/ SG c= bool M by PBOOLE:16; hence SF \/ SG is MSSubsetFamily of M by PBOOLE:def_18; ::_thesis: verum end; theorem :: MSSUBFAM:35 for I being set for M being ManySortedSet of I for SF, SG being MSSubsetFamily of M holds SF /\ SG is MSSubsetFamily of M proof let I be set ; ::_thesis: for M being ManySortedSet of I for SF, SG being MSSubsetFamily of M holds SF /\ SG is MSSubsetFamily of M let M be ManySortedSet of I; ::_thesis: for SF, SG being MSSubsetFamily of M holds SF /\ SG is MSSubsetFamily of M let SF, SG be MSSubsetFamily of M; ::_thesis: SF /\ SG is MSSubsetFamily of M ( SF c= bool M & SG c= bool M ) by PBOOLE:def_18; then SF /\ SG c= (bool M) /\ (bool M) by PBOOLE:21; hence SF /\ SG is MSSubsetFamily of M by PBOOLE:def_18; ::_thesis: verum end; theorem Th36: :: MSSUBFAM:36 for I being set for A, M being ManySortedSet of I for SF being MSSubsetFamily of M holds SF \ A is MSSubsetFamily of M proof let I be set ; ::_thesis: for A, M being ManySortedSet of I for SF being MSSubsetFamily of M holds SF \ A is MSSubsetFamily of M let A, M be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M holds SF \ A is MSSubsetFamily of M let SF be MSSubsetFamily of M; ::_thesis: SF \ A is MSSubsetFamily of M SF c= bool M by PBOOLE:def_18; then A1: SF \ A c= (bool M) \ A by PBOOLE:53; (bool M) \ A c= bool M by PBOOLE:56; then SF \ A c= bool M by A1, PBOOLE:13; hence SF \ A is MSSubsetFamily of M by PBOOLE:def_18; ::_thesis: verum end; theorem :: MSSUBFAM:37 for I being set for M being ManySortedSet of I for SF, SG being MSSubsetFamily of M holds SF \+\ SG is MSSubsetFamily of M proof let I be set ; ::_thesis: for M being ManySortedSet of I for SF, SG being MSSubsetFamily of M holds SF \+\ SG is MSSubsetFamily of M let M be ManySortedSet of I; ::_thesis: for SF, SG being MSSubsetFamily of M holds SF \+\ SG is MSSubsetFamily of M let SF, SG be MSSubsetFamily of M; ::_thesis: SF \+\ SG is MSSubsetFamily of M ( SF \ SG is MSSubsetFamily of M & SG \ SF is MSSubsetFamily of M ) by Th36; hence SF \+\ SG is MSSubsetFamily of M by Th34; ::_thesis: verum end; theorem Th38: :: MSSUBFAM:38 for I being set for A, M being ManySortedSet of I st A c= M holds {A} is MSSubsetFamily of M proof let I be set ; ::_thesis: for A, M being ManySortedSet of I st A c= M holds {A} is MSSubsetFamily of M let A, M be ManySortedSet of I; ::_thesis: ( A c= M implies {A} is MSSubsetFamily of M ) assume A c= M ; ::_thesis: {A} is MSSubsetFamily of M then A in bool M by MBOOLEAN:18; then {A} c= bool M by PZFMISC1:33; hence {A} is MSSubsetFamily of M by PBOOLE:def_18; ::_thesis: verum end; theorem Th39: :: MSSUBFAM:39 for I being set for A, M, B being ManySortedSet of I st A c= M & B c= M holds {A,B} is MSSubsetFamily of M proof let I be set ; ::_thesis: for A, M, B being ManySortedSet of I st A c= M & B c= M holds {A,B} is MSSubsetFamily of M let A, M, B be ManySortedSet of I; ::_thesis: ( A c= M & B c= M implies {A,B} is MSSubsetFamily of M ) assume ( A c= M & B c= M ) ; ::_thesis: {A,B} is MSSubsetFamily of M then ( {A} is MSSubsetFamily of M & {B} is MSSubsetFamily of M ) by Th38; then {A} \/ {B} is MSSubsetFamily of M by Th34; hence {A,B} is MSSubsetFamily of M by PZFMISC1:10; ::_thesis: verum end; theorem Th40: :: MSSUBFAM:40 for I being set for M being ManySortedSet of I for SF being MSSubsetFamily of M holds union SF c= M proof let I be set ; ::_thesis: for M being ManySortedSet of I for SF being MSSubsetFamily of M holds union SF c= M let M be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M holds union SF c= M let SF be MSSubsetFamily of M; ::_thesis: union SF c= M A1: for x being set for F being Subset-Family of x holds union F is Subset of x ; let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (union SF) . i c= M . i ) assume A2: i in I ; ::_thesis: (union SF) . i c= M . i SF . i is Subset-Family of (M . i) by A2, Th32; then union (SF . i) is Subset of (M . i) by A1; then union (SF . i) c= M . i ; hence (union SF) . i c= M . i by A2, MBOOLEAN:def_2; ::_thesis: verum end; begin definition let I be set ; let M be ManySortedSet of I; let SF be MSSubsetFamily of M; func meet SF -> ManySortedSet of I means :Def1: :: MSSUBFAM:def 1 for i being set st i in I holds ex Q being Subset-Family of (M . i) st ( Q = SF . i & it . i = Intersect Q ); existence ex b1 being ManySortedSet of I st for i being set st i in I holds ex Q being Subset-Family of (M . i) st ( Q = SF . i & b1 . i = Intersect Q ) proof defpred S1[ set , set ] means ex Q being Subset-Family of (M . $1) st ( Q = SF . $1 & $2 = Intersect Q ); A1: for i being set st i in I holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume A2: i in I ; ::_thesis: ex j being set st S1[i,j] then reconsider Q = SF . i as Subset-Family of (M . i) by Th32; reconsider a = I --> (Intersect Q) as ManySortedSet of I ; take a . i ; ::_thesis: S1[i,a . i] take Q ; ::_thesis: ( Q = SF . i & a . i = Intersect Q ) thus ( Q = SF . i & a . i = Intersect Q ) by A2, FUNCOP_1:7; ::_thesis: verum end; ex X being ManySortedSet of I st for i being set st i in I holds S1[i,X . i] from PBOOLE:sch_3(A1); hence ex b1 being ManySortedSet of I st for i being set st i in I holds ex Q being Subset-Family of (M . i) st ( Q = SF . i & b1 . i = Intersect Q ) ; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds ex Q being Subset-Family of (M . i) st ( Q = SF . i & b1 . i = Intersect Q ) ) & ( for i being set st i in I holds ex Q being Subset-Family of (M . i) st ( Q = SF . i & b2 . i = Intersect Q ) ) holds b1 = b2 proof let X1, X2 be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds ex Q being Subset-Family of (M . i) st ( Q = SF . i & X1 . i = Intersect Q ) ) & ( for i being set st i in I holds ex Q being Subset-Family of (M . i) st ( Q = SF . i & X2 . i = Intersect Q ) ) implies X1 = X2 ) assume A3: ( ( for i being set st i in I holds ex Q1 being Subset-Family of (M . i) st ( Q1 = SF . i & X1 . i = Intersect Q1 ) ) & ( for i being set st i in I holds ex Q2 being Subset-Family of (M . i) st ( Q2 = SF . i & X2 . i = Intersect Q2 ) ) ) ; ::_thesis: X1 = X2 now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X1_._i_=_X2_._i let i be set ; ::_thesis: ( i in I implies X1 . i = X2 . i ) assume i in I ; ::_thesis: X1 . i = X2 . i then ( ex Q1 being Subset-Family of (M . i) st ( Q1 = SF . i & X1 . i = Intersect Q1 ) & ex Q2 being Subset-Family of (M . i) st ( Q2 = SF . i & X2 . i = Intersect Q2 ) ) by A3; hence X1 . i = X2 . i ; ::_thesis: verum end; hence X1 = X2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def1 defines meet MSSUBFAM:def_1_:_ for I being set for M being ManySortedSet of I for SF being MSSubsetFamily of M for b4 being ManySortedSet of I holds ( b4 = meet SF iff for i being set st i in I holds ex Q being Subset-Family of (M . i) st ( Q = SF . i & b4 . i = Intersect Q ) ); definition let I be set ; let M be ManySortedSet of I; let SF be MSSubsetFamily of M; :: original: meet redefine func meet SF -> ManySortedSubset of M; coherence meet SF is ManySortedSubset of M proof let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or (meet SF) . i c= M . i ) assume i in I ; ::_thesis: (meet SF) . i c= M . i then ex Q being Subset-Family of (M . i) st ( Q = SF . i & (meet SF) . i = Intersect Q ) by Def1; hence (meet SF) . i c= M . i ; ::_thesis: verum end; end; theorem Th41: :: MSSUBFAM:41 for I being set for M being ManySortedSet of I for SF being MSSubsetFamily of M st SF = [[0]] I holds meet SF = M proof let I be set ; ::_thesis: for M being ManySortedSet of I for SF being MSSubsetFamily of M st SF = [[0]] I holds meet SF = M let M be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M st SF = [[0]] I holds meet SF = M let SF be MSSubsetFamily of M; ::_thesis: ( SF = [[0]] I implies meet SF = M ) assume A1: SF = [[0]] I ; ::_thesis: meet SF = M now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (meet_SF)_._i_=_M_._i let i be set ; ::_thesis: ( i in I implies (meet SF) . i = M . i ) assume i in I ; ::_thesis: (meet SF) . i = M . i then consider Q being Subset-Family of (M . i) such that A2: Q = SF . i and A3: (meet SF) . i = Intersect Q by Def1; Q = {} by A1, A2; hence (meet SF) . i = M . i by A3, SETFAM_1:def_9; ::_thesis: verum end; hence meet SF = M by PBOOLE:3; ::_thesis: verum end; theorem :: MSSUBFAM:42 for I being set for M being ManySortedSet of I for SFe being V8() MSSubsetFamily of M holds meet SFe c= union SFe proof let I be set ; ::_thesis: for M being ManySortedSet of I for SFe being V8() MSSubsetFamily of M holds meet SFe c= union SFe let M be ManySortedSet of I; ::_thesis: for SFe being V8() MSSubsetFamily of M holds meet SFe c= union SFe let SFe be V8() MSSubsetFamily of M; ::_thesis: meet SFe c= union SFe let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (meet SFe) . i c= (union SFe) . i ) assume A1: i in I ; ::_thesis: (meet SFe) . i c= (union SFe) . i then consider Q being Subset-Family of (M . i) such that A2: Q = SFe . i and A3: (meet SFe) . i = Intersect Q by Def1; ( meet Q c= union Q & Intersect Q = meet Q ) by A1, A2, SETFAM_1:2, SETFAM_1:def_9; hence (meet SFe) . i c= (union SFe) . i by A1, A2, A3, MBOOLEAN:def_2; ::_thesis: verum end; theorem :: MSSUBFAM:43 for I being set for M, A being ManySortedSet of I for SF being MSSubsetFamily of M st A in SF holds meet SF c= A proof let I be set ; ::_thesis: for M, A being ManySortedSet of I for SF being MSSubsetFamily of M st A in SF holds meet SF c= A let M, A be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M st A in SF holds meet SF c= A let SF be MSSubsetFamily of M; ::_thesis: ( A in SF implies meet SF c= A ) assume A1: A in SF ; ::_thesis: meet SF c= A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (meet SF) . i c= A . i ) assume A2: i in I ; ::_thesis: (meet SF) . i c= A . i then consider Q being Subset-Family of (M . i) such that A3: Q = SF . i and A4: (meet SF) . i = Intersect Q by Def1; A5: A . i in SF . i by A1, A2, PBOOLE:def_1; then Intersect Q = meet Q by A3, SETFAM_1:def_9; hence (meet SF) . i c= A . i by A3, A4, A5, SETFAM_1:3; ::_thesis: verum end; theorem :: MSSUBFAM:44 for I being set for M being ManySortedSet of I for SF being MSSubsetFamily of M st [[0]] I in SF holds meet SF = [[0]] I proof let I be set ; ::_thesis: for M being ManySortedSet of I for SF being MSSubsetFamily of M st [[0]] I in SF holds meet SF = [[0]] I let M be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M st [[0]] I in SF holds meet SF = [[0]] I let SF be MSSubsetFamily of M; ::_thesis: ( [[0]] I in SF implies meet SF = [[0]] I ) assume A1: [[0]] I in SF ; ::_thesis: meet SF = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (meet_SF)_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies (meet SF) . i = ([[0]] I) . i ) assume A2: i in I ; ::_thesis: (meet SF) . i = ([[0]] I) . i then consider Q being Subset-Family of (M . i) such that A3: Q = SF . i and A4: (meet SF) . i = Intersect Q by Def1; ([[0]] I) . i in Q by A1, A2, A3, PBOOLE:def_1; then A5: {} in Q ; ([[0]] I) . i in SF . i by A1, A2, PBOOLE:def_1; then Intersect Q = meet Q by A3, SETFAM_1:def_9; then Intersect Q = {} by A5, SETFAM_1:4; hence (meet SF) . i = ([[0]] I) . i by A4; ::_thesis: verum end; hence meet SF = [[0]] I by PBOOLE:3; ::_thesis: verum end; theorem :: MSSUBFAM:45 for I being set for Z, M being ManySortedSet of I for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds Z c= Z1 ) holds Z c= meet SF proof let I be set ; ::_thesis: for Z, M being ManySortedSet of I for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds Z c= Z1 ) holds Z c= meet SF let Z, M be ManySortedSet of I; ::_thesis: for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds Z c= Z1 ) holds Z c= meet SF let SF be V8() MSSubsetFamily of M; ::_thesis: ( ( for Z1 being ManySortedSet of I st Z1 in SF holds Z c= Z1 ) implies Z c= meet SF ) assume A1: for Z1 being ManySortedSet of I st Z1 in SF holds Z c= Z1 ; ::_thesis: Z c= meet SF let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or Z . i c= (meet SF) . i ) consider T being ManySortedSet of I such that A2: T in SF by PBOOLE:134; assume A3: i in I ; ::_thesis: Z . i c= (meet SF) . i then consider Q being Subset-Family of (M . i) such that A4: Q = SF . i and A5: (meet SF) . i = Intersect Q by Def1; A6: for Z9 being set st Z9 in Q holds Z . i c= Z9 proof let Z9 be set ; ::_thesis: ( Z9 in Q implies Z . i c= Z9 ) assume A7: Z9 in Q ; ::_thesis: Z . i c= Z9 dom (T +* (i .--> Z9)) = I by A3, PZFMISC1:1; then reconsider K = T +* (i .--> Z9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; A8: dom (i .--> Z9) = {i} by FUNCOP_1:13; i in {i} by TARSKI:def_1; then A9: K . i = (i .--> Z9) . i by A8, FUNCT_4:13 .= Z9 by FUNCOP_1:72 ; K in SF proof let q be set ; :: according to PBOOLE:def_1 ::_thesis: ( not q in I or K . q in SF . q ) assume A10: q in I ; ::_thesis: K . q in SF . q percases ( q = i or q <> i ) ; suppose q = i ; ::_thesis: K . q in SF . q hence K . q in SF . q by A4, A7, A9; ::_thesis: verum end; suppose q <> i ; ::_thesis: K . q in SF . q then not q in dom (i .--> Z9) by A8, TARSKI:def_1; then K . q = T . q by FUNCT_4:11; hence K . q in SF . q by A2, A10, PBOOLE:def_1; ::_thesis: verum end; end; end; then Z c= K by A1; hence Z . i c= Z9 by A3, A9, PBOOLE:def_2; ::_thesis: verum end; Intersect Q = meet Q by A3, A4, SETFAM_1:def_9; hence Z . i c= (meet SF) . i by A3, A4, A5, A6, SETFAM_1:5; ::_thesis: verum end; theorem :: MSSUBFAM:46 for I being set for M being ManySortedSet of I for SF, SG being MSSubsetFamily of M st SF c= SG holds meet SG c= meet SF proof let I be set ; ::_thesis: for M being ManySortedSet of I for SF, SG being MSSubsetFamily of M st SF c= SG holds meet SG c= meet SF let M be ManySortedSet of I; ::_thesis: for SF, SG being MSSubsetFamily of M st SF c= SG holds meet SG c= meet SF let SF, SG be MSSubsetFamily of M; ::_thesis: ( SF c= SG implies meet SG c= meet SF ) assume A1: SF c= SG ; ::_thesis: meet SG c= meet SF let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (meet SG) . i c= (meet SF) . i ) assume A2: i in I ; ::_thesis: (meet SG) . i c= (meet SF) . i then consider Qf being Subset-Family of (M . i) such that A3: Qf = SF . i and A4: (meet SF) . i = Intersect Qf by Def1; consider Qg being Subset-Family of (M . i) such that A5: Qg = SG . i and A6: (meet SG) . i = Intersect Qg by A2, Def1; Qf c= Qg by A1, A2, A3, A5, PBOOLE:def_2; hence (meet SG) . i c= (meet SF) . i by A4, A6, SETFAM_1:44; ::_thesis: verum end; theorem :: MSSUBFAM:47 for I being set for M, A, B being ManySortedSet of I for SF being MSSubsetFamily of M st A in SF & A c= B holds meet SF c= B proof let I be set ; ::_thesis: for M, A, B being ManySortedSet of I for SF being MSSubsetFamily of M st A in SF & A c= B holds meet SF c= B let M, A, B be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M st A in SF & A c= B holds meet SF c= B let SF be MSSubsetFamily of M; ::_thesis: ( A in SF & A c= B implies meet SF c= B ) assume that A1: A in SF and A2: A c= B ; ::_thesis: meet SF c= B let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (meet SF) . i c= B . i ) assume A3: i in I ; ::_thesis: (meet SF) . i c= B . i then A4: A . i c= B . i by A2, PBOOLE:def_2; consider Q being Subset-Family of (M . i) such that A5: Q = SF . i and A6: (meet SF) . i = Intersect Q by A3, Def1; A7: A . i in SF . i by A1, A3, PBOOLE:def_1; then Intersect Q = meet Q by A5, SETFAM_1:def_9; hence (meet SF) . i c= B . i by A5, A6, A7, A4, SETFAM_1:7; ::_thesis: verum end; theorem :: MSSUBFAM:48 for I being set for M, A, B being ManySortedSet of I for SF being MSSubsetFamily of M st A in SF & A /\ B = [[0]] I holds (meet SF) /\ B = [[0]] I proof let I be set ; ::_thesis: for M, A, B being ManySortedSet of I for SF being MSSubsetFamily of M st A in SF & A /\ B = [[0]] I holds (meet SF) /\ B = [[0]] I let M, A, B be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M st A in SF & A /\ B = [[0]] I holds (meet SF) /\ B = [[0]] I let SF be MSSubsetFamily of M; ::_thesis: ( A in SF & A /\ B = [[0]] I implies (meet SF) /\ B = [[0]] I ) assume that A1: A in SF and A2: A /\ B = [[0]] I ; ::_thesis: (meet SF) /\ B = [[0]] I now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ((meet_SF)_/\_B)_._i_=_([[0]]_I)_._i let i be set ; ::_thesis: ( i in I implies ((meet SF) /\ B) . i = ([[0]] I) . i ) assume A3: i in I ; ::_thesis: ((meet SF) /\ B) . i = ([[0]] I) . i then consider Q being Subset-Family of (M . i) such that A4: Q = SF . i and A5: (meet SF) . i = Intersect Q by Def1; A6: A . i in SF . i by A1, A3, PBOOLE:def_1; (A . i) /\ (B . i) = ([[0]] I) . i by A2, A3, PBOOLE:def_5; then (A . i) /\ (B . i) = {} ; then A . i misses B . i by XBOOLE_0:def_7; then meet Q misses B . i by A4, A6, SETFAM_1:8; then (meet Q) /\ (B . i) = {} by XBOOLE_0:def_7; then A7: (meet Q) /\ (B . i) = ([[0]] I) . i ; Intersect Q = meet Q by A4, A6, SETFAM_1:def_9; hence ((meet SF) /\ B) . i = ([[0]] I) . i by A3, A5, A7, PBOOLE:def_5; ::_thesis: verum end; hence (meet SF) /\ B = [[0]] I by PBOOLE:3; ::_thesis: verum end; theorem :: MSSUBFAM:49 for I being set for M being ManySortedSet of I for SH, SF, SG being MSSubsetFamily of M st SH = SF \/ SG holds meet SH = (meet SF) /\ (meet SG) proof let I be set ; ::_thesis: for M being ManySortedSet of I for SH, SF, SG being MSSubsetFamily of M st SH = SF \/ SG holds meet SH = (meet SF) /\ (meet SG) let M be ManySortedSet of I; ::_thesis: for SH, SF, SG being MSSubsetFamily of M st SH = SF \/ SG holds meet SH = (meet SF) /\ (meet SG) let SH, SF, SG be MSSubsetFamily of M; ::_thesis: ( SH = SF \/ SG implies meet SH = (meet SF) /\ (meet SG) ) assume A1: SH = SF \/ SG ; ::_thesis: meet SH = (meet SF) /\ (meet SG) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (meet_SH)_._i_=_((meet_SF)_/\_(meet_SG))_._i let i be set ; ::_thesis: ( i in I implies (meet SH) . i = ((meet SF) /\ (meet SG)) . i ) assume A2: i in I ; ::_thesis: (meet SH) . i = ((meet SF) /\ (meet SG)) . i then consider Qf being Subset-Family of (M . i) such that A3: Qf = SF . i and A4: (meet SF) . i = Intersect Qf by Def1; consider Qh being Subset-Family of (M . i) such that A5: Qh = SH . i and A6: (meet SH) . i = Intersect Qh by A2, Def1; consider Qg being Subset-Family of (M . i) such that A7: Qg = SG . i and A8: (meet SG) . i = Intersect Qg by A2, Def1; A9: Qh = Qf \/ Qg by A1, A2, A3, A7, A5, PBOOLE:def_4; now__::_thesis:_(_(_Qf_<>_{}_&_Qg_<>_{}_&_(meet_SH)_._i_=_((meet_SF)_/\_(meet_SG))_._i_)_or_(_Qf_<>_{}_&_Qg_=_{}_&_(meet_SH)_._i_=_((meet_SF)_/\_(meet_SG))_._i_)_or_(_Qf_=_{}_&_Qg_<>_{}_&_(meet_SH)_._i_=_((meet_SF)_/\_(meet_SG))_._i_)_or_(_Qf_=_{}_&_Qg_=_{}_&_(meet_SH)_._i_=_((meet_SF)_/\_(meet_SG))_._i_)_) percases ( ( Qf <> {} & Qg <> {} ) or ( Qf <> {} & Qg = {} ) or ( Qf = {} & Qg <> {} ) or ( Qf = {} & Qg = {} ) ) ; caseA10: ( Qf <> {} & Qg <> {} ) ; ::_thesis: (meet SH) . i = ((meet SF) /\ (meet SG)) . i hence (meet SH) . i = meet Qh by A6, A9, SETFAM_1:def_9 .= (meet Qf) /\ (meet Qg) by A9, A10, SETFAM_1:9 .= ((meet SF) . i) /\ (meet Qg) by A4, A10, SETFAM_1:def_9 .= ((meet SF) . i) /\ ((meet SG) . i) by A8, A10, SETFAM_1:def_9 .= ((meet SF) /\ (meet SG)) . i by A2, PBOOLE:def_5 ; ::_thesis: verum end; caseA11: ( Qf <> {} & Qg = {} ) ; ::_thesis: (meet SH) . i = ((meet SF) /\ (meet SG)) . i hence (meet SH) . i = ((meet SF) . i) /\ (M . i) by A4, A6, A9, XBOOLE_1:28 .= ((meet SF) . i) /\ ((meet SG) . i) by A8, A11, SETFAM_1:def_9 .= ((meet SF) /\ (meet SG)) . i by A2, PBOOLE:def_5 ; ::_thesis: verum end; caseA12: ( Qf = {} & Qg <> {} ) ; ::_thesis: (meet SH) . i = ((meet SF) /\ (meet SG)) . i hence (meet SH) . i = (M . i) /\ ((meet SG) . i) by A8, A6, A9, XBOOLE_1:28 .= ((meet SF) . i) /\ ((meet SG) . i) by A4, A12, SETFAM_1:def_9 .= ((meet SF) /\ (meet SG)) . i by A2, PBOOLE:def_5 ; ::_thesis: verum end; case ( Qf = {} & Qg = {} ) ; ::_thesis: (meet SH) . i = ((meet SF) /\ (meet SG)) . i hence (meet SH) . i = (Intersect Qf) /\ (Intersect Qg) by A6, A9 .= ((meet SF) /\ (meet SG)) . i by A2, A4, A8, PBOOLE:def_5 ; ::_thesis: verum end; end; end; hence (meet SH) . i = ((meet SF) /\ (meet SG)) . i ; ::_thesis: verum end; hence meet SH = (meet SF) /\ (meet SG) by PBOOLE:3; ::_thesis: verum end; theorem :: MSSUBFAM:50 for I being set for M being ManySortedSet of I for SF being MSSubsetFamily of M for V being ManySortedSubset of M st SF = {V} holds meet SF = V proof let I be set ; ::_thesis: for M being ManySortedSet of I for SF being MSSubsetFamily of M for V being ManySortedSubset of M st SF = {V} holds meet SF = V let M be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M for V being ManySortedSubset of M st SF = {V} holds meet SF = V let SF be MSSubsetFamily of M; ::_thesis: for V being ManySortedSubset of M st SF = {V} holds meet SF = V let V be ManySortedSubset of M; ::_thesis: ( SF = {V} implies meet SF = V ) assume A1: SF = {V} ; ::_thesis: meet SF = V now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (meet_SF)_._i_=_V_._i let i be set ; ::_thesis: ( i in I implies (meet SF) . i = V . i ) assume A2: i in I ; ::_thesis: (meet SF) . i = V . i then consider Q being Subset-Family of (M . i) such that A3: Q = SF . i and A4: (meet SF) . i = Intersect Q by Def1; thus (meet SF) . i = meet Q by A1, A2, A3, A4, SETFAM_1:def_9 .= meet {(V . i)} by A1, A2, A3, PZFMISC1:def_1 .= V . i by SETFAM_1:10 ; ::_thesis: verum end; hence meet SF = V by PBOOLE:3; ::_thesis: verum end; theorem Th51: :: MSSUBFAM:51 for I being set for M being ManySortedSet of I for SF being MSSubsetFamily of M for V, W being ManySortedSubset of M st SF = {V,W} holds meet SF = V /\ W proof let I be set ; ::_thesis: for M being ManySortedSet of I for SF being MSSubsetFamily of M for V, W being ManySortedSubset of M st SF = {V,W} holds meet SF = V /\ W let M be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M for V, W being ManySortedSubset of M st SF = {V,W} holds meet SF = V /\ W let SF be MSSubsetFamily of M; ::_thesis: for V, W being ManySortedSubset of M st SF = {V,W} holds meet SF = V /\ W let V, W be ManySortedSubset of M; ::_thesis: ( SF = {V,W} implies meet SF = V /\ W ) assume A1: SF = {V,W} ; ::_thesis: meet SF = V /\ W now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (meet_SF)_._i_=_(V_/\_W)_._i let i be set ; ::_thesis: ( i in I implies (meet SF) . i = (V /\ W) . i ) assume A2: i in I ; ::_thesis: (meet SF) . i = (V /\ W) . i then ex Q being Subset-Family of (M . i) st ( Q = SF . i & (meet SF) . i = Intersect Q ) by Def1; hence (meet SF) . i = meet ({V,W} . i) by A1, A2, SETFAM_1:def_9 .= meet {(V . i),(W . i)} by A2, PZFMISC1:def_2 .= (V . i) /\ (W . i) by SETFAM_1:11 .= (V /\ W) . i by A2, PBOOLE:def_5 ; ::_thesis: verum end; hence meet SF = V /\ W by PBOOLE:3; ::_thesis: verum end; theorem :: MSSUBFAM:52 for I being set for M, A being ManySortedSet of I for SF being MSSubsetFamily of M st A in meet SF holds for B being ManySortedSet of I st B in SF holds A in B proof let I be set ; ::_thesis: for M, A being ManySortedSet of I for SF being MSSubsetFamily of M st A in meet SF holds for B being ManySortedSet of I st B in SF holds A in B let M, A be ManySortedSet of I; ::_thesis: for SF being MSSubsetFamily of M st A in meet SF holds for B being ManySortedSet of I st B in SF holds A in B let SF be MSSubsetFamily of M; ::_thesis: ( A in meet SF implies for B being ManySortedSet of I st B in SF holds A in B ) assume A1: A in meet SF ; ::_thesis: for B being ManySortedSet of I st B in SF holds A in B let B be ManySortedSet of I; ::_thesis: ( B in SF implies A in B ) assume A2: B in SF ; ::_thesis: A in B let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in B . i ) assume A3: i in I ; ::_thesis: A . i in B . i then A4: A . i in (meet SF) . i by A1, PBOOLE:def_1; A5: B . i in SF . i by A2, A3, PBOOLE:def_1; ex Q being Subset-Family of (M . i) st ( Q = SF . i & (meet SF) . i = Intersect Q ) by A3, Def1; hence A . i in B . i by A4, A5, SETFAM_1:43; ::_thesis: verum end; theorem :: MSSUBFAM:53 for I being set for A, M being ManySortedSet of I for SF being V8() MSSubsetFamily of M st A in M & ( for B being ManySortedSet of I st B in SF holds A in B ) holds A in meet SF proof let I be set ; ::_thesis: for A, M being ManySortedSet of I for SF being V8() MSSubsetFamily of M st A in M & ( for B being ManySortedSet of I st B in SF holds A in B ) holds A in meet SF let A, M be ManySortedSet of I; ::_thesis: for SF being V8() MSSubsetFamily of M st A in M & ( for B being ManySortedSet of I st B in SF holds A in B ) holds A in meet SF let SF be V8() MSSubsetFamily of M; ::_thesis: ( A in M & ( for B being ManySortedSet of I st B in SF holds A in B ) implies A in meet SF ) assume that A1: A in M and A2: for B being ManySortedSet of I st B in SF holds A in B ; ::_thesis: A in meet SF let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in (meet SF) . i ) consider T being ManySortedSet of I such that A3: T in SF by PBOOLE:134; assume A4: i in I ; ::_thesis: A . i in (meet SF) . i then consider Q being Subset-Family of (M . i) such that A5: Q = SF . i and A6: (meet SF) . i = Intersect Q by Def1; A7: for B9 being set st B9 in Q holds A . i in B9 proof let B9 be set ; ::_thesis: ( B9 in Q implies A . i in B9 ) assume A8: B9 in Q ; ::_thesis: A . i in B9 dom (T +* (i .--> B9)) = I by A4, PZFMISC1:1; then reconsider K = T +* (i .--> B9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; A9: dom (i .--> B9) = {i} by FUNCOP_1:13; i in {i} by TARSKI:def_1; then A10: K . i = (i .--> B9) . i by A9, FUNCT_4:13 .= B9 by FUNCOP_1:72 ; K in SF proof let q be set ; :: according to PBOOLE:def_1 ::_thesis: ( not q in I or K . q in SF . q ) assume A11: q in I ; ::_thesis: K . q in SF . q percases ( q = i or q <> i ) ; suppose q = i ; ::_thesis: K . q in SF . q hence K . q in SF . q by A5, A8, A10; ::_thesis: verum end; suppose q <> i ; ::_thesis: K . q in SF . q then not q in dom (i .--> B9) by A9, TARSKI:def_1; then K . q = T . q by FUNCT_4:11; hence K . q in SF . q by A3, A11, PBOOLE:def_1; ::_thesis: verum end; end; end; then A in K by A2; hence A . i in B9 by A4, A10, PBOOLE:def_1; ::_thesis: verum end; A . i in M . i by A1, A4, PBOOLE:def_1; hence A . i in (meet SF) . i by A6, A7, SETFAM_1:43; ::_thesis: verum end; definition let I be set ; let M be ManySortedSet of I; let IT be MSSubsetFamily of M; attrIT is additive means :: MSSUBFAM:def 2 for A, B being ManySortedSet of I st A in IT & B in IT holds A \/ B in IT; attrIT is absolutely-additive means :Def3: :: MSSUBFAM:def 3 for F being MSSubsetFamily of M st F c= IT holds union F in IT; attrIT is multiplicative means :: MSSUBFAM:def 4 for A, B being ManySortedSet of I st A in IT & B in IT holds A /\ B in IT; attrIT is absolutely-multiplicative means :Def5: :: MSSUBFAM:def 5 for F being MSSubsetFamily of M st F c= IT holds meet F in IT; attrIT is properly-upper-bound means :Def6: :: MSSUBFAM:def 6 M in IT; attrIT is properly-lower-bound means :Def7: :: MSSUBFAM:def 7 [[0]] I in IT; end; :: deftheorem defines additive MSSUBFAM:def_2_:_ for I being set for M being ManySortedSet of I for IT being MSSubsetFamily of M holds ( IT is additive iff for A, B being ManySortedSet of I st A in IT & B in IT holds A \/ B in IT ); :: deftheorem Def3 defines absolutely-additive MSSUBFAM:def_3_:_ for I being set for M being ManySortedSet of I for IT being MSSubsetFamily of M holds ( IT is absolutely-additive iff for F being MSSubsetFamily of M st F c= IT holds union F in IT ); :: deftheorem defines multiplicative MSSUBFAM:def_4_:_ for I being set for M being ManySortedSet of I for IT being MSSubsetFamily of M holds ( IT is multiplicative iff for A, B being ManySortedSet of I st A in IT & B in IT holds A /\ B in IT ); :: deftheorem Def5 defines absolutely-multiplicative MSSUBFAM:def_5_:_ for I being set for M being ManySortedSet of I for IT being MSSubsetFamily of M holds ( IT is absolutely-multiplicative iff for F being MSSubsetFamily of M st F c= IT holds meet F in IT ); :: deftheorem Def6 defines properly-upper-bound MSSUBFAM:def_6_:_ for I being set for M being ManySortedSet of I for IT being MSSubsetFamily of M holds ( IT is properly-upper-bound iff M in IT ); :: deftheorem Def7 defines properly-lower-bound MSSUBFAM:def_7_:_ for I being set for M being ManySortedSet of I for IT being MSSubsetFamily of M holds ( IT is properly-lower-bound iff [[0]] I in IT ); Lm1: for I being set for M being ManySortedSet of I holds ( bool M is additive & bool M is absolutely-additive & bool M is multiplicative & bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound ) proof let I be set ; ::_thesis: for M being ManySortedSet of I holds ( bool M is additive & bool M is absolutely-additive & bool M is multiplicative & bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound ) let M be ManySortedSet of I; ::_thesis: ( bool M is additive & bool M is absolutely-additive & bool M is multiplicative & bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound ) thus bool M is additive ::_thesis: ( bool M is absolutely-additive & bool M is multiplicative & bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound ) proof let A be ManySortedSet of I; :: according to MSSUBFAM:def_2 ::_thesis: for B being ManySortedSet of I st A in bool M & B in bool M holds A \/ B in bool M let B be ManySortedSet of I; ::_thesis: ( A in bool M & B in bool M implies A \/ B in bool M ) assume ( A in bool M & B in bool M ) ; ::_thesis: A \/ B in bool M then ( A c= M & B c= M ) by MBOOLEAN:1; then A \/ B c= M by PBOOLE:16; hence A \/ B in bool M by MBOOLEAN:1; ::_thesis: verum end; thus bool M is absolutely-additive ::_thesis: ( bool M is multiplicative & bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound ) proof let F be MSSubsetFamily of M; :: according to MSSUBFAM:def_3 ::_thesis: ( F c= bool M implies union F in bool M ) assume F c= bool M ; ::_thesis: union F in bool M union F c= M by Th40; hence union F in bool M by MBOOLEAN:18; ::_thesis: verum end; thus bool M is multiplicative ::_thesis: ( bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound ) proof let A be ManySortedSet of I; :: according to MSSUBFAM:def_4 ::_thesis: for B being ManySortedSet of I st A in bool M & B in bool M holds A /\ B in bool M let B be ManySortedSet of I; ::_thesis: ( A in bool M & B in bool M implies A /\ B in bool M ) assume that A1: A in bool M and B in bool M ; ::_thesis: A /\ B in bool M A c= M by A1, MBOOLEAN:1; then A /\ B c= M by MBOOLEAN:14; hence A /\ B in bool M by MBOOLEAN:1; ::_thesis: verum end; thus bool M is absolutely-multiplicative ::_thesis: ( bool M is properly-upper-bound & bool M is properly-lower-bound ) proof let F be MSSubsetFamily of M; :: according to MSSUBFAM:def_5 ::_thesis: ( F c= bool M implies meet F in bool M ) assume F c= bool M ; ::_thesis: meet F in bool M meet F c= M by PBOOLE:def_18; hence meet F in bool M by MBOOLEAN:18; ::_thesis: verum end; M in bool M by MBOOLEAN:18; hence bool M is properly-upper-bound by Def6; ::_thesis: bool M is properly-lower-bound [[0]] I c= M by MBOOLEAN:5; then [[0]] I in bool M by MBOOLEAN:1; hence bool M is properly-lower-bound by Def7; ::_thesis: verum end; registration let I be set ; let M be ManySortedSet of I; cluster Relation-like V8() I -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ManySortedSubset of bool M; existence ex b1 being MSSubsetFamily of M st ( b1 is V8() & b1 is additive & b1 is absolutely-additive & b1 is multiplicative & b1 is absolutely-multiplicative & b1 is properly-upper-bound & b1 is properly-lower-bound ) proof take bool M ; ::_thesis: ( bool M is V8() & bool M is additive & bool M is absolutely-additive & bool M is multiplicative & bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound ) thus ( bool M is V8() & bool M is additive & bool M is absolutely-additive & bool M is multiplicative & bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound ) by Lm1; ::_thesis: verum end; end; definition let I be set ; let M be ManySortedSet of I; :: original: bool redefine func bool M -> additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSSubsetFamily of M; coherence bool M is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSSubsetFamily of M by Lm1; end; registration let I be set ; let M be ManySortedSet of I; cluster absolutely-additive -> additive for ManySortedSubset of bool M; coherence for b1 being MSSubsetFamily of M st b1 is absolutely-additive holds b1 is additive proof let SF be MSSubsetFamily of M; ::_thesis: ( SF is absolutely-additive implies SF is additive ) assume A1: SF is absolutely-additive ; ::_thesis: SF is additive let A be ManySortedSet of I; :: according to MSSUBFAM:def_2 ::_thesis: for B being ManySortedSet of I st A in SF & B in SF holds A \/ B in SF let B be ManySortedSet of I; ::_thesis: ( A in SF & B in SF implies A \/ B in SF ) assume that A2: A in SF and A3: B in SF ; ::_thesis: A \/ B in SF ( {A} c= SF & {B} c= SF ) by A2, A3, PZFMISC1:33; then {A} \/ {B} c= SF by PBOOLE:16; then A4: {A,B} c= SF by PZFMISC1:10; B is ManySortedSubset of M by A3, Th33; then A5: B c= M by PBOOLE:def_18; A is ManySortedSubset of M by A2, Th33; then A c= M by PBOOLE:def_18; then {A,B} is MSSubsetFamily of M by A5, Th39; then union {A,B} in SF by A1, A4, Def3; hence A \/ B in SF by PZFMISC1:32; ::_thesis: verum end; end; registration let I be set ; let M be ManySortedSet of I; cluster absolutely-multiplicative -> multiplicative for ManySortedSubset of bool M; coherence for b1 being MSSubsetFamily of M st b1 is absolutely-multiplicative holds b1 is multiplicative proof let SF be MSSubsetFamily of M; ::_thesis: ( SF is absolutely-multiplicative implies SF is multiplicative ) assume A1: SF is absolutely-multiplicative ; ::_thesis: SF is multiplicative let A be ManySortedSet of I; :: according to MSSUBFAM:def_4 ::_thesis: for B being ManySortedSet of I st A in SF & B in SF holds A /\ B in SF let B be ManySortedSet of I; ::_thesis: ( A in SF & B in SF implies A /\ B in SF ) assume that A2: A in SF and A3: B in SF ; ::_thesis: A /\ B in SF A4: B is ManySortedSubset of M by A3, Th33; then A5: B c= M by PBOOLE:def_18; A6: A is ManySortedSubset of M by A2, Th33; then A c= M by PBOOLE:def_18; then reconsider ab = {A,B} as MSSubsetFamily of M by A5, Th39; ( {A} c= SF & {B} c= SF ) by A2, A3, PZFMISC1:33; then {A} \/ {B} c= SF by PBOOLE:16; then {A,B} c= SF by PZFMISC1:10; then meet ab in SF by A1, Def5; hence A /\ B in SF by A6, A4, Th51; ::_thesis: verum end; end; registration let I be set ; let M be ManySortedSet of I; cluster absolutely-multiplicative -> properly-upper-bound for ManySortedSubset of bool M; coherence for b1 being MSSubsetFamily of M st b1 is absolutely-multiplicative holds b1 is properly-upper-bound proof [[0]] I c= bool M by PBOOLE:43; then reconsider a = [[0]] I as MSSubsetFamily of M by PBOOLE:def_18; let SF be MSSubsetFamily of M; ::_thesis: ( SF is absolutely-multiplicative implies SF is properly-upper-bound ) assume A1: SF is absolutely-multiplicative ; ::_thesis: SF is properly-upper-bound ( meet a = M & [[0]] I c= SF ) by Th41, PBOOLE:43; hence M in SF by A1, Def5; :: according to MSSUBFAM:def_6 ::_thesis: verum end; end; registration let I be set ; let M be ManySortedSet of I; cluster properly-upper-bound -> V8() for ManySortedSubset of bool M; coherence for b1 being MSSubsetFamily of M st b1 is properly-upper-bound holds b1 is V8() proof let SF be MSSubsetFamily of M; ::_thesis: ( SF is properly-upper-bound implies SF is V8() ) assume SF is properly-upper-bound ; ::_thesis: SF is V8() then A1: M in SF by Def6; let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not SF . i is empty ) assume i in I ; ::_thesis: not SF . i is empty hence not SF . i is empty by A1, PBOOLE:def_1; ::_thesis: verum end; end; registration let I be set ; let M be ManySortedSet of I; cluster absolutely-additive -> properly-lower-bound for ManySortedSubset of bool M; coherence for b1 being MSSubsetFamily of M st b1 is absolutely-additive holds b1 is properly-lower-bound proof [[0]] I c= bool M by PBOOLE:43; then reconsider a = [[0]] I as MSSubsetFamily of M by PBOOLE:def_18; let SF be MSSubsetFamily of M; ::_thesis: ( SF is absolutely-additive implies SF is properly-lower-bound ) assume A1: SF is absolutely-additive ; ::_thesis: SF is properly-lower-bound ( union a = [[0]] I & [[0]] I c= SF ) by MBOOLEAN:21, PBOOLE:43; hence [[0]] I in SF by A1, Def3; :: according to MSSUBFAM:def_7 ::_thesis: verum end; end; registration let I be set ; let M be ManySortedSet of I; cluster properly-lower-bound -> V8() for ManySortedSubset of bool M; coherence for b1 being MSSubsetFamily of M st b1 is properly-lower-bound holds b1 is V8() proof let SF be MSSubsetFamily of M; ::_thesis: ( SF is properly-lower-bound implies SF is V8() ) assume SF is properly-lower-bound ; ::_thesis: SF is V8() then A1: [[0]] I in SF by Def7; let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not SF . i is empty ) assume i in I ; ::_thesis: not SF . i is empty hence not SF . i is empty by A1, PBOOLE:def_1; ::_thesis: verum end; end;