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