let X be set ; :: thesis: for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X st S is with_countable_Cover holds
ex P being countable Subset of S st P is a_partition of X
let S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X; :: thesis: ( S is with_countable_Cover implies ex P being countable Subset of S st P is a_partition of X )
assume S is with_countable_Cover ; :: thesis: ex P being countable Subset of S st P is a_partition of X
then consider XX being countable Subset of S such that
A1: XX is Cover of X ;
per cases ( S is empty or not S is empty ) ;
suppose C1: S is empty ; :: thesis: ex P being countable Subset of S st P is a_partition of X
X c= union XX by A1, SETFAM_1:def 11;
then C2: X is empty by C1, ZFMISC_1:2;
set P = {} ;
{} is countable Subset of S by SUBSET_1:1;
hence ex P being countable Subset of S st P is a_partition of X by C2, EQREL_1:45; :: thesis: verum
end;
suppose B0: not S is empty ; :: thesis: ex P being countable Subset of S st P is a_partition of X
A2: X c= union XX by A1, SETFAM_1:def 11;
per cases ( X is empty or not X is empty ) ;
suppose A5: not X is empty ; :: thesis: ex P being countable Subset of S st P is a_partition of X
A6: ex g being Function of NATPLUS,S st rng g = XX
proof
consider f being Function of omega,XX such that
A7: rng f = XX by A5, A2, ZFMISC_1:2, CARD_3:96;
reconsider f = f as Function of NAT,XX ;
defpred S1[ object , object ] means ( $1 in NATPLUS & ex xx being Nat st
( xx + 1 = $1 & $2 = f . xx ) );
A8: for x, y1, y2 being object st x in NATPLUS & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
A9: for x being object st x in NATPLUS holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in NATPLUS implies ex y being object st S1[x,y] )
assume A10: x in NATPLUS ; :: thesis: ex y being object st S1[x,y]
then reconsider x = x as Nat ;
A11: x - 1 is Nat by A10, CHORD:1;
(x - 1) + 1 = x ;
then consider xx being Nat such that
A12: xx + 1 = x by A11;
set y = f . xx;
( x in NATPLUS & ex xx being Nat st
( xx + 1 = x & f . xx = f . xx ) ) by A10, A12;
hence ex y being object st S1[x,y] ; :: thesis: verum
end;
consider g being Function such that
A13: ( dom g = NATPLUS & ( for a being object st a in NATPLUS holds
S1[a,g . a] ) ) from FUNCT_1:sch 2(A8, A9);
 A14: rng g = XX
proof
A15: rng g c= XX
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in XX )
assume x in rng g ; :: thesis: x in XX
then consider y being object such that
A16: ( y in dom g & x = g . y ) by FUNCT_1:def 3;
consider xx being Nat such that
A17: ( xx + 1 = y & g . y = f . xx ) by A13, A16;
( xx is Nat & dom f = NAT ) by A5, A2, ZFMISC_1:2, FUNCT_2:def 1;
then xx in dom f by ORDINAL1:def 12;
then x in rng f by A16, A17, FUNCT_1:def 3;
hence x in XX ; :: thesis: verum
end;
XX c= rng g
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in XX or x in rng g )
assume x in XX ; :: thesis: x in rng g
then consider y being object such that
A18: ( y in dom f & x = f . y ) by A7, FUNCT_1:def 3;
reconsider y = y as Nat by A18;
A19: ( y + 1 in dom g & x = f . y ) by A13, A18, NAT_LAT:def 6;
g . (y + 1) = f . y
proof
consider xx being Nat such that
A20: ( xx + 1 = y + 1 & g . (y + 1) = f . xx ) by A13, A19;
thus g . (y + 1) = f . y by A20; :: thesis: verum
end;
hence x in rng g by A19, FUNCT_1:def 3; :: thesis: verum
end;
hence rng g = XX by A15; :: thesis: verum
end;
g is Function of NATPLUS,S by B0, A13, A14, FUNCT_2:def 1, RELSET_1:4;
hence ex g being Function of NATPLUS,S st rng g = XX by A14; :: thesis: verum
end;
ex P being countable Subset of S st P is a_partition of X
proof
consider g being Function of NATPLUS,S such that
A21: rng g = XX by A6;
consider P being countable Subset of S such that
A22: ( P is a_partition of Union g & ( for n being NatPlus holds Union (g | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (g | (Seg n)) ) } ) ) by Thm4;
Union g c= X
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union g or y in X )
assume y in Union g ; :: thesis: y in X
then consider z being set such that
A24: ( y in z & z in rng g ) by TARSKI:def 4;
y in union S by A24, TARSKI:def 4;
hence y in X ; :: thesis: verum
end;
then X = Union g by A1, A21, SETFAM_1:def 11;
hence ex P being countable Subset of S st P is a_partition of X by A22; :: thesis: verum
end;
hence ex P being countable Subset of S st P is a_partition of X ; :: thesis: verum
end;
end;
end;
end;