:: 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;