let X be set ; :: thesis: for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X
for SM, T being FinSequence of S ex P being finite Subset of S st P is a_partition of (meet (rng SM)) \ (Union T)
let S be cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X; :: thesis: for SM, T being FinSequence of S ex P being finite Subset of S st P is a_partition of (meet (rng SM)) \ (Union T)
let SM, T be FinSequence of S; :: thesis: ex P being finite Subset of S st P is a_partition of (meet (rng SM)) \ (Union T)
defpred S1[ FinSequence] means ex pa being finite Subset of S st pa is a_partition of (meet (rng $1)) \ (union (rng T));
A1: 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 S1[p] ; :: thesis: S1[p ^ <*x*>]
then consider pa being finite Subset of S such that
A2: pa is a_partition of (meet (rng p)) \ (union (rng T)) ;
A3: (meet (rng (p ^ <*x*>))) \ (union (rng T)) = (meet ((rng p) \/ (rng <*x*>))) \ (union (rng T)) by FINSEQ_1:31
.= (meet ((rng p) \/ {x})) \ (union (rng T)) by FINSEQ_1:38 ;
A4: ( rng p <> {} implies (meet ((rng p) \/ {x})) \ (union (rng T)) = ((meet (rng p)) \ (union (rng T))) /\ x )
proof
assume rng p <> {} ; :: thesis: (meet ((rng p) \/ {x})) \ (union (rng T)) = ((meet (rng p)) \ (union (rng T))) /\ x
then (meet ((rng p) \/ {x})) \ (union (rng T)) = ((meet (rng p)) /\ (meet {x})) \ (union (rng T)) by SETFAM_1:9
.= ((meet (rng p)) /\ x) \ (union (rng T)) by SETFAM_1:10
.= ((meet (rng p)) \ (union (rng T))) /\ x by XBOOLE_1:49 ;
hence (meet ((rng p) \/ {x})) \ (union (rng T)) = ((meet (rng p)) \ (union (rng T))) /\ x ; :: thesis: verum
end;
ex pb being finite Subset of S st pb is a_partition of (meet (rng (p ^ <*x*>))) \ (union (rng T))
proof
defpred S2[ set ] means ( $1 is Element of S & not $1 /\ x is empty & $1 in pa );
defpred S3[ object , object ] means ex A1 being set st
( A1 = $1 & $1 is Element of S & $2 is finite Subset of S & not A1 /\ x is empty & $1 in pa & $2 is a_partition of A1 /\ x );
set XX1 = { s where s is Element of S : S2[s] } ;
set YY1 = { s where s is finite Subset of S : ex y being Element of S st
( S2[y] & s is a_partition of y /\ x ) } ;
A5: for a being object st a in { s where s is Element of S : S2[s] } holds
ex y being object st
( y in { s where s is finite Subset of S : ex y being Element of S st
( S2[y] & s is a_partition of y /\ x ) } & S3[a,y] )
proof
let a be object ; :: thesis: ( a in { s where s is Element of S : S2[s] } implies ex y being object st
( y in { s where s is finite Subset of S : ex y being Element of S st
( S2[y] & s is a_partition of y /\ x ) } & S3[a,y] ) )
assume a in { s where s is Element of S : S2[s] } ; :: thesis: ex y being object st
( y in { s where s is finite Subset of S : ex y being Element of S st
( S2[y] & s is a_partition of y /\ x ) } & S3[a,y] )
then consider s being Element of S such that
A6: ( a = s & S2[s] ) ;
reconsider a = a as set by TARSKI:1;
consider aa being finite Subset of S such that
A7: aa is a_partition of a /\ x by A6, Defcap;
( aa in { s where s is finite Subset of S : ex y being Element of S st
( S2[y] & s is a_partition of y /\ x ) } & S3[a,aa] ) by A6, A7;
hence ex y being object st
( y in { s where s is finite Subset of S : ex y being Element of S st
( S2[y] & s is a_partition of y /\ x ) } & S3[a,y] ) ; :: thesis: verum
end;
consider gg being Function such that
A8: ( dom gg = { s where s is Element of S : S2[s] } & rng gg c= { s where s is finite Subset of S : ex y being Element of S st
( S2[y] & s is a_partition of y /\ x ) } ) and
A9: for x being object st x in { s where s is Element of S : S2[s] } holds
S3[x,gg . x] from FUNCT_1:sch 6(A5);
 A10: { s where s is Element of S : S2[s] } is finite
proof
{ s where s is Element of S : S2[s] } c= pa
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { s where s is Element of S : S2[s] } or u in pa )
assume u in { s where s is Element of S : S2[s] } ; :: thesis: u in pa
then consider s being Element of S such that
A11: ( u = s & S2[s] ) ;
thus u in pa by A11; :: thesis: verum
end;
hence { s where s is Element of S : S2[s] } is finite ; :: thesis: verum
end;
A12: ( Union gg is finite Subset of S & Union gg is a_partition of ((meet (rng p)) \ (union (rng T))) /\ x )
proof
A13: Union gg is finite
proof
Union gg is finite
proof
for zz being set st zz in rng gg holds
zz is finite
proof
let zz be set ; :: thesis: ( zz in rng gg implies zz is finite )
assume zz in rng gg ; :: thesis: zz is finite
then consider z0 being object such that
A14: ( z0 in { s where s is Element of S : S2[s] } & zz = gg . z0 ) by FUNCT_1:def 3, A8;
S3[z0,gg . z0] by A9, A14;
hence zz is finite by A14; :: thesis: verum
end;
hence Union gg is finite by A10, A8, FINSET_1:8, FINSET_1:7; :: thesis: verum
end;
hence Union gg is finite ; :: thesis: verum
end;
A15: Union gg c= S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union gg or x in S )
assume x in Union gg ; :: thesis: x in S
then consider u being set such that
A16: x in u and
A17: u in rng gg by TARSKI:def 4;
consider u0 being object such that
A18: ( u0 in { s where s is Element of S : S2[s] } & u = gg . u0 ) by A8, A17, FUNCT_1:def 3;
S3[u0,gg . u0] by A9, A18;
hence x in S by A16, A18; :: thesis: verum
end;
Union gg is a_partition of ((meet (rng p)) \ (union (rng T))) /\ x
proof
A19: Union gg c= bool (((meet (rng p)) \ (union (rng T))) /\ x)
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Union gg or u in bool (((meet (rng p)) \ (union (rng T))) /\ x) )
assume A20: u in Union gg ; :: thesis: u in bool (((meet (rng p)) \ (union (rng T))) /\ x)
consider v being set such that
A21: ( u in v & v in rng gg ) by TARSKI:def 4, A20;
consider w being object such that
A22: w in dom gg and
A23: gg . w = v by FUNCT_1:def 3, A21;
reconsider u = u, w = w as set by TARSKI:1;
A24: S3[w,gg . w] by A22, A8, A9;
then w /\ x c= ((meet (rng p)) \ (union (rng T))) /\ x by A2, XBOOLE_1:26;
then u c= ((meet (rng p)) \ (union (rng T))) /\ x by A23, A21, A24, XBOOLE_1:1;
hence u in bool (((meet (rng p)) \ (union (rng T))) /\ x) ; :: thesis: verum
end;
A25: union (Union gg) = ((meet (rng p)) \ (union (rng T))) /\ x
proof
A26: union (Union gg) c= union (bool (((meet (rng p)) \ (union (rng T))) /\ x)) by A19, ZFMISC_1:77;
((meet (rng p)) \ (union (rng T))) /\ x c= union (Union gg)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((meet (rng p)) \ (union (rng T))) /\ x or a in union (Union gg) )
assume a in ((meet (rng p)) \ (union (rng T))) /\ x ; :: thesis: a in union (Union gg)
then a in (union pa) /\ x by A2, EQREL_1:def 4;
then A28: ( a in union pa & a in x ) by XBOOLE_0:def 4;
then consider p11 being set such that
A29: ( a in p11 & p11 in pa ) by TARSKI:def 4;
A30: ( not p11 /\ x is empty & p11 is Element of S & x is Element of S ) by A28, A29, XBOOLE_0:def 4;
A31: p11 in { s where s is Element of S : S2[s] } by A29, A30;
then S3[p11,gg . p11] by A9;
then union (gg . p11) = p11 /\ x by EQREL_1:def 4;
then a in union (gg . p11) by A28, A29, XBOOLE_0:def 4;
then consider d being set such that
A32: ( a in d & d in gg . p11 ) by TARSKI:def 4;
( a in d & d in gg . p11 & gg . p11 in rng gg ) by A32, A8, A31, FUNCT_1:3;
then ( a in d & d in union (rng gg) ) by TARSKI:def 4;
hence a in union (Union gg) by TARSKI:def 4; :: thesis: verum
end;
hence union (Union gg) = ((meet (rng p)) \ (union (rng T))) /\ x by A26, ZFMISC_1:81; :: thesis: verum
end;
for A being Subset of (((meet (rng p)) \ (union (rng T))) /\ x) st A in Union gg holds
( A <> {} & ( for B being Subset of (((meet (rng p)) \ (union (rng T))) /\ x) holds
( not B in Union gg or A = B or A misses B ) ) )
proof
let A be Subset of (((meet (rng p)) \ (union (rng T))) /\ x); :: thesis: ( A in Union gg implies ( A <> {} & ( for B being Subset of (((meet (rng p)) \ (union (rng T))) /\ x) holds
( not B in Union gg or A = B or A misses B ) ) ) )
assume A in Union gg ; :: thesis: ( A <> {} & ( for B being Subset of (((meet (rng p)) \ (union (rng T))) /\ x) holds
( not B in Union gg or A = B or A misses B ) ) )
then consider a0 being set such that
A33: ( A in a0 & a0 in rng gg ) by TARSKI:def 4;
consider a1 being object such that
A34: ( a1 in { s where s is Element of S : S2[s] } & a0 = gg . a1 ) by A33, A8, FUNCT_1:def 3;
reconsider a1 = a1 as set by TARSKI:1;
( A <> {} & ( for B being Subset of (((meet (rng p)) \ (union (rng T))) /\ x) holds
( not B in Union gg or A = B or A misses B ) ) )
proof
thus A <> {} :: thesis: for B being Subset of (((meet (rng p)) \ (union (rng T))) /\ x) holds
( not B in Union gg or A = B or A misses B )
proof
assume A35: A = {} ; :: thesis: contradiction
S3[a1,gg . a1] by A9, A34;
hence contradiction by A33, A34, A35; :: thesis: verum
end;
thus for B being Subset of (((meet (rng p)) \ (union (rng T))) /\ x) holds
( not B in Union gg or A = B or A misses B ) :: thesis: verum
proof
let B be Subset of (((meet (rng p)) \ (union (rng T))) /\ x); :: thesis: ( not B in Union gg or A = B or A misses B )
assume B in Union gg ; :: thesis: ( A = B or A misses B )
then consider x0 being set such that
A36: ( B in x0 & x0 in rng gg ) by TARSKI:def 4;
consider y0 being object such that
A37: ( y0 in { s where s is Element of S : S2[s] } & gg . y0 = x0 ) by A8, A36, FUNCT_1:def 3;
reconsider y0 = y0 as set by TARSKI:1;
( A = B or A misses B )
proof
per cases ( a1 = y0 or not a1 = y0 ) ;
suppose A38: a1 = y0 ; :: thesis: ( A = B or A misses B )
then S3[a1,gg . a1] by A9, A37;
hence ( A = B or A misses B ) by EQREL_1:def 4, A36, A37, A33, A34, A38; :: thesis: verum
end;
suppose A39: not a1 = y0 ; :: thesis: ( A = B or A misses B )
consider sx being Element of S such that
A40: ( a1 = sx & S2[sx] ) by A34;
consider sd being Element of S such that
A41: ( y0 = sd & S2[sd] ) by A37;
( a1 misses y0 & a1 /\ x c= a1 & y0 /\ x c= y0 ) by A40, A41, XBOOLE_1:17, A39, A2, EQREL_1:def 4;
then A42: a1 /\ x misses y0 /\ x by XBOOLE_1:64;
A43: S3[y0,gg . y0] by A9, A37;
S3[a1,gg . a1] by A9, A34;
hence ( A = B or A misses B ) by A43, A36, A37, A33, A34, A42, XBOOLE_1:64; :: thesis: verum
end;
end;
end;
hence ( A = B or A misses B ) ; :: thesis: verum
end;
end;
hence ( A <> {} & ( for B being Subset of (((meet (rng p)) \ (union (rng T))) /\ x) holds
( not B in Union gg or A = B or A misses B ) ) ) ; :: thesis: verum
end;
hence Union gg is a_partition of ((meet (rng p)) \ (union (rng T))) /\ x by EQREL_1:def 4, A19, A25; :: thesis: verum
end;
hence ( Union gg is finite Subset of S & Union gg is a_partition of ((meet (rng p)) \ (union (rng T))) /\ x ) by A13, A15; :: thesis: verum
end;
( rng p = {} implies ex ZZ being finite Subset of S st ZZ is a_partition of (meet (rng (p ^ <*x*>))) \ (union (rng T)) )
proof
assume rng p = {} ; :: thesis: ex ZZ being finite Subset of S st ZZ is a_partition of (meet (rng (p ^ <*x*>))) \ (union (rng T))
then p = {} ;
then p ^ <*x*> = <*x*> by FINSEQ_1:34;
then rng (p ^ <*x*>) = {x} by FINSEQ_1:39;
then A44: (meet (rng (p ^ <*x*>))) \ (union (rng T)) = x \ (union (rng T)) by SETFAM_1:10;
thus ex ZZ being finite Subset of S st ZZ is a_partition of (meet (rng (p ^ <*x*>))) \ (union (rng T)) by A44, Thm1; :: thesis: verum
end;
hence ex pb being finite Subset of S st pb is a_partition of (meet (rng (p ^ <*x*>))) \ (union (rng T)) by A4, A12, A3; :: thesis: verum
end;
hence S1[p ^ <*x*>] ; :: thesis: verum
end;
A45: S1[ <*> S]
proof
( {} is finite Subset of S & {} is a_partition of {} ) by SUBSET_1:1, EQREL_1:45;
hence S1[ <*> S] by SETFAM_1:1; :: thesis: verum
end;
for p being FinSequence of S holds S1[p] from FINSEQ_2:sch 2(A45, A1);
 hence ex P being finite Subset of S st P is a_partition of (meet (rng SM)) \ (Union T) ; :: thesis: verum