let X be set ; :: thesis: for S being cap-finite-partition-closed Subset-Family of X
for SM being FinSequence of S ex P being finite Subset of S st P is a_partition of meet (rng SM)
let S be cap-finite-partition-closed Subset-Family of X; :: thesis: for SM being FinSequence of S ex P being finite Subset of S st P is a_partition of meet (rng SM)
let SM be FinSequence of S; :: thesis: ex P being finite Subset of S st P is a_partition of meet (rng SM)
per cases ( S is empty or not S is empty ) ;
suppose A1: S is empty ; :: thesis: ex P being finite Subset of S st P is a_partition of meet (rng SM)
then meet (rng SM) = {} by SETFAM_1:1;
hence ex P being finite Subset of S st P is a_partition of meet (rng SM) by A1, EQREL_1:45; :: thesis: verum
end;
suppose A3: not S is empty ; :: thesis: ex P being finite Subset of S st P is a_partition of meet (rng SM)
defpred S1[ FinSequence] means ex p being finite Subset of S st p is a_partition of meet (rng $1);
A4: for p being FinSequence of S
for x being Element of S st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of S; :: thesis: for x being Element of S st S1[p] holds
S1[p ^ <*x*>]
let x be Element of S; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A5: S1[p] ; :: thesis: S1[p ^ <*x*>]
per cases ( rng p = {} or rng p <> {} ) ;
suppose A10: rng p <> {} ; :: thesis: S1[p ^ <*x*>]
consider pp being finite Subset of S such that
A11: pp is a_partition of meet (rng p) by A5;
defpred S2[ object , object ] means ex A1 being set st
( A1 = $1 & $1 is Element of S & $2 is finite Subset of S & $2 is a_partition of A1 /\ x );
set XIN = { s where s is Element of S : s in pp } ;
A15: { s where s is Element of S : s in pp } c= pp
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { s where s is Element of S : s in pp } or a in pp )
assume a in { s where s is Element of S : s in pp } ; :: thesis: a in pp
then ex a0 being Element of S st
( a = a0 & a0 in pp ) ;
hence a in pp ; :: thesis: verum
end;
set XOUT = { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } ;
A17: for a being object st a in { s where s is Element of S : s in pp } holds
ex b being object st
( b in { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } & S2[a,b] )
proof
let a be object ; :: thesis: ( a in { s where s is Element of S : s in pp } implies ex b being object st
( b in { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } & S2[a,b] ) )
assume a in { s where s is Element of S : s in pp } ; :: thesis: ex b being object st
( b in { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } & S2[a,b] )
then consider s0 being Element of S such that
A18: a = s0 and
A19: s0 in pp ;
per cases ( s0 /\ x <> {} or s0 /\ x = {} ) ;
suppose s0 /\ x <> {} ; :: thesis: ex b being object st
( b in { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } & S2[a,b] )
then consider ps being finite Subset of S such that
A20: ps is a_partition of s0 /\ x by Defcap;
( ps in { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } & S2[a,ps] ) by A18, A19, A20;
hence ex b being object st
( b in { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } & S2[a,b] ) ; :: thesis: verum
end;
suppose A21: s0 /\ x = {} ; :: thesis: ex b being object st
( b in { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } & S2[a,b] )
( {} is finite Subset of S & {} is a_partition of {} ) by SUBSET_1:1, EQREL_1:45;
then ( {} in { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } & S2[a, {} ] ) by A18, A19, A21;
hence ex b being object st
( b in { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } & S2[a,b] ) ; :: thesis: verum
end;
end;
end;
consider f being Function such that
A22: ( dom f = { s where s is Element of S : s in pp } & rng f c= { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } ) and
A23: for x being object st x in { s where s is Element of S : s in pp } holds
S2[x,f . x] from FUNCT_1:sch 6(A17);
 ( Union f is finite Subset of S & Union f is a_partition of meet (rng (p ^ <*x*>)) )
proof
A24: Union f is finite
proof
for z being set st z in rng f holds
z is finite
proof
let z be set ; :: thesis: ( z in rng f implies z is finite )
assume z in rng f ; :: thesis: z is finite
then consider z0 being object such that
A25: ( z0 in { s where s is Element of S : s in pp } & z = f . z0 ) by A22, FUNCT_1:def 3;
S2[z0,f . z0] by A23, A25;
hence z is finite by A25; :: thesis: verum
end;
hence Union f is finite by A22, A15, FINSET_1:7, FINSET_1:8; :: thesis: verum
end;
A26: Union f c= S
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Union f or a in S )
assume a in Union f ; :: thesis: a in S
then consider b being set such that
A27: a in b and
A28: b in rng f by TARSKI:def 4;
consider c being object such that
A29: ( c in { s where s is Element of S : s in pp } & b = f . c ) by A22, A28, FUNCT_1:def 3;
S2[c,f . c] by A23, A29;
hence a in S by A27, A29; :: thesis: verum
end;
A30: Union f c= bool (meet (rng (p ^ <*x*>)))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Union f or a in bool (meet (rng (p ^ <*x*>))) )
assume a in Union f ; :: thesis: a in bool (meet (rng (p ^ <*x*>)))
then consider b being set such that
A31: a in b and
A32: b in rng f by TARSKI:def 4;
reconsider a = a as set by TARSKI:1;
b in { s where s is finite Subset of S : ex y being set st
( y in pp & s is a_partition of y /\ x ) } by A22, A32;
then consider b0 being finite Subset of S such that
A33: b = b0 and
A34: ex y being set st
( y in pp & b0 is a_partition of y /\ x ) ;
consider y0 being set such that
A35: y0 in pp and
A36: b0 is a_partition of y0 /\ x by A34;
y0 /\ x c= (meet (rng p)) /\ x by A35, A11, XBOOLE_1:26;
then A37: y0 /\ x c= (meet (rng p)) /\ (meet {x}) by SETFAM_1:10;
A38: a c= (meet (rng p)) /\ (meet {x}) by A31, A33, A36, A37, XBOOLE_1:1;
a c= meet ((rng p) \/ {x}) by A10, A38, SETFAM_1:9;
then a c= meet ((rng p) \/ (rng <*x*>)) by FINSEQ_1:38;
then a c= meet (rng (p ^ <*x*>)) by FINSEQ_1:31;
hence a in bool (meet (rng (p ^ <*x*>))) ; :: thesis: verum
end;
A39: union (Union f) = meet (rng (p ^ <*x*>))
proof
A40: union (Union f) c= meet (rng (p ^ <*x*>))
proof
union (Union f) c= union (bool (meet (rng (p ^ <*x*>)))) by A30, ZFMISC_1:77;
hence union (Union f) c= meet (rng (p ^ <*x*>)) by ZFMISC_1:81; :: thesis: verum
end;
meet (rng (p ^ <*x*>)) c= union (Union f)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in meet (rng (p ^ <*x*>)) or a in union (Union f) )
assume A41: a in meet (rng (p ^ <*x*>)) ; :: thesis: a in union (Union f)
rng (p ^ <*x*>) = (rng p) \/ (rng <*x*>) by FINSEQ_1:31;
then A42: meet (rng (p ^ <*x*>)) = meet ((rng p) \/ {x}) by FINSEQ_1:38;
meet (rng (p ^ <*x*>)) = (meet (rng p)) /\ (meet {x}) by A10, A42, SETFAM_1:9;
then meet (rng (p ^ <*x*>)) = (meet (rng p)) /\ x by SETFAM_1:10;
then a in (union pp) /\ x by A11, EQREL_1:def 4, A41;
then A43: ( a in union pp & a in x ) by XBOOLE_0:def 4;
then consider a0 being set such that
A44: ( a in a0 & a0 in pp ) by TARSKI:def 4;
A45: a0 in { s where s is Element of S : s in pp } by A44;
then S2[a0,f . a0] by A23;
then A46: union (f . a0) = a0 /\ x by EQREL_1:def 4;
a in a0 /\ x by A44, A43, XBOOLE_0:def 4;
then consider c0 being set such that
A47: a in c0 and
A48: c0 in f . a0 by A46, TARSKI:def 4;
A49: a in union (f . a0) by A47, A48, TARSKI:def 4;
f . a0 c= Union f
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in f . a0 or b in Union f )
assume b in f . a0 ; :: thesis: b in Union f
then ( b in f . a0 & f . a0 in rng f ) by A22, A45, FUNCT_1:def 3;
hence b in Union f by TARSKI:def 4; :: thesis: verum
end;
then union (f . a0) c= union (Union f) by ZFMISC_1:77;
hence a in union (Union f) by A49; :: thesis: verum
end;
hence union (Union f) = meet (rng (p ^ <*x*>)) by A40; :: thesis: verum
end;
for A being Subset of (meet (rng (p ^ <*x*>))) st A in Union f holds
( A <> {} & ( for B being Subset of (meet (rng (p ^ <*x*>))) holds
( not B in Union f or A = B or A misses B ) ) )
proof
let A be Subset of (meet (rng (p ^ <*x*>))); :: thesis: ( A in Union f implies ( A <> {} & ( for B being Subset of (meet (rng (p ^ <*x*>))) holds
( not B in Union f or A = B or A misses B ) ) ) )
assume A51: A in Union f ; :: thesis: ( A <> {} & ( for B being Subset of (meet (rng (p ^ <*x*>))) holds
( not B in Union f or A = B or A misses B ) ) )
consider a0 being set such that
A52: ( A in a0 & a0 in rng f ) by A51, TARSKI:def 4;
consider b0 being object such that
A53: b0 in { s where s is Element of S : s in pp } and
A54: a0 = f . b0 by A52, A22, FUNCT_1:def 3;
reconsider b0 = b0 as set by TARSKI:1;
A55: S2[b0,f . b0] by A23, A53;
hence A <> {} by A52, A54; :: thesis: for B being Subset of (meet (rng (p ^ <*x*>))) holds
( not B in Union f or A = B or A misses B )
thus for B being Subset of (meet (rng (p ^ <*x*>))) holds
( not B in Union f or A = B or A misses B ) :: thesis: verum
proof
let B be Subset of (meet (rng (p ^ <*x*>))); :: thesis: ( not B in Union f or A = B or A misses B )
assume B in Union f ; :: thesis: ( A = B or A misses B )
then consider d0 being set such that
A56: ( B in d0 & d0 in rng f ) by TARSKI:def 4;
consider e0 being object such that
A57: e0 in { s where s is Element of S : s in pp } and
A58: d0 = f . e0 by A56, A22, FUNCT_1:def 3;
reconsider e0 = e0 as set by TARSKI:1;
B02: S2[e0,f . e0] by A23, A57;
consider b00 being Element of S such that
A59: b0 = b00 and
A60: b00 in pp by A53;
consider e00 being Element of S such that
A61: e0 = e00 and
A62: e00 in pp by A57;
per cases ( e00 = b00 or not e00 = b00 ) ;
suppose e00 = b00 ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A52, A54, A56, A58, A59, A61, A55, EQREL_1:def 4; :: thesis: verum
end;
suppose A63: not e00 = b00 ; :: thesis: ( A = B or A misses B )
( union (f . b0) = b0 /\ x & union (f . e0) = e0 /\ x ) by EQREL_1:def 4, A55, B02;
then ( union (f . b0) c= b0 & union (f . e0) c= e0 ) by XBOOLE_1:17;
then A64: union (f . b0) misses union (f . e0) by A63, A59, A61, A60, A62, A11, EQREL_1:def 4, XBOOLE_1:64;
A /\ B c= {}
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in A /\ B or t in {} )
assume t in A /\ B ; :: thesis: t in {}
then ( t in A & t in B ) by XBOOLE_0:def 4;
then ( t in union (f . b0) & t in union (f . e0) ) by A52, A54, A56, A58, TARSKI:def 4;
hence t in {} by A64, XBOOLE_0:def 4; :: thesis: verum
end;
hence ( A = B or A misses B ) ; :: thesis: verum
end;
end;
end;
end;
hence ( Union f is finite Subset of S & Union f is a_partition of meet (rng (p ^ <*x*>)) ) by A24, A26, A30, A39, EQREL_1:def 4; :: thesis: verum
end;
hence S1[p ^ <*x*>] ; :: thesis: verum
end;
end;
end;
A65: S1[ <*> S] for p being FinSequence of S holds S1[p] from FINSEQ_2:sch 2(A65, A4);
then consider P being finite Subset of S such that
A66: P is a_partition of meet (rng SM) ;
thus ex P being finite Subset of S st P is a_partition of meet (rng SM) by A66; :: thesis: verum
end;
end;