let C be Cardinal; :: thesis: for T being TopSpace st ( for F being Subset-Family of T st F is open & F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & card G c= C ) ) holds
for A being Subset of T st A is closed & A is discrete holds
card A c= C
let T be TopSpace; :: thesis: ( ( for F being Subset-Family of T st F is open & F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & card G c= C ) ) implies for A being Subset of T st A is closed & A is discrete holds
card A c= C )
assume A1: for F being Subset-Family of T st F is open & F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & card G c= C ) ; :: thesis: for A being Subset of T st A is closed & A is discrete holds
card A c= C
set TOP = the topology of T;
let A be Subset of T; :: thesis: ( A is closed & A is discrete implies card A c= C )
assume that
A2: A is closed and
A3: A is discrete ; :: thesis: card A c= C
A ` in the topology of T by A2, PRE_TOPC:def 2;
then A4: {(A `)} c= the topology of T by ZFMISC_1:31;
defpred S₁[ object , object ] means ex D1 being set st
( D1 = $1 & {$2} = D1 /\ A );
defpred S₂[ object , object ] means ex D2 being set st
( D2 = $2 & A /\ D2 = {$1} );
A5: for x being object st x in A holds
ex y being object st
( y in the topology of T & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in A implies ex y being object st
( y in the topology of T & S₂[x,y] ) )
assume x in A ; :: thesis: ex y being object st
( y in the topology of T & S₂[x,y] )
then consider G being Subset of T such that
A6: ( G is open & A /\ G = {x} ) by A3, TEX_2:26;
take G ; :: thesis: ( G in the topology of T & S₂[x,G] )
thus ( G in the topology of T & S₂[x,G] ) by A6; :: thesis: verum

end;

consider p being Function of A, the topology of T such that
A7: for x being object st x in A holds
S₂[x,p . x] from FUNCT_2:sch 1(A5);
reconsider RNG = rng p, AA = {(A `)} as open Subset-Family of T by A4, TOPS_2:11, XBOOLE_1:1;
reconsider RngA = RNG \/ AA as open Subset-Family of T by TOPS_2:13;
[#] T c= union RngA

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] T or x in union RngA )
assume A8: x in [#] T ; :: thesis: x in union RngA

per cases ( x in A or not x in A ) ;

suppose A9: x in A ; :: thesis: x in union RngA

dom p = A by FUNCT_2:def 1;
then p . x in rng p by A9, FUNCT_1:def 3;
then A10: p . x in RngA by XBOOLE_0:def 3;
S₂[x,p . x] by A7, A9;
then ( x in {x} & A /\ (p . x) = {x} ) by TARSKI:def 1;
then x in p . x by XBOOLE_0:def 4;
hence x in union RngA by A10, TARSKI:def 4; :: thesis: verum

end;

suppose A11: not x in A ; :: thesis: x in union RngA

A ` in AA by TARSKI:def 1;
then A12: A ` in RngA by XBOOLE_0:def 3;
x in A ` by A8, A11, XBOOLE_0:def 5;
hence x in union RngA by A12, TARSKI:def 4; :: thesis: verum

end;

end;

end;

then RngA is Cover of T by SETFAM_1:def 11;
then consider G being Subset-Family of T such that
A13: G c= RngA and
A14: G is Cover of T and
A15: card G c= C by A1;
A16: for x being object st x in G \ AA holds
ex y being object st
( y in A & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in G \ AA implies ex y being object st
( y in A & S₁[x,y] ) )
assume x in G \ AA ; :: thesis: ex y being object st
( y in A & S₁[x,y] )
then ( x in G & not x in AA ) by XBOOLE_0:def 5;
then x in RNG by A13, XBOOLE_0:def 3;
then consider y being object such that
A17: ( y in dom p & p . y = x ) by FUNCT_1:def 3;
take y ; :: thesis: ( y in A & S₁[x,y] )
S₂[y,p . y] by A7, A17;
hence ( y in A & S₁[x,y] ) by A17; :: thesis: verum

end;

consider q being Function of (G \ AA),A such that
A18: for x being object st x in G \ AA holds
S₁[x,q . x] from FUNCT_2:sch 1(A16);

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: card A c= C

hence card A c= C ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: card A c= C

then A19: dom q = G \ AA by FUNCT_2:def 1;
A c= rng q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in rng q )
assume A20: x in A ; :: thesis: x in rng q
not T is empty by A20;
then consider U being Subset of T such that
A21: x in U and
A22: U in G by A14, A20, PCOMPS_1:3;
not x in A ` by A20, XBOOLE_0:def 5;
then not U in AA by A21, TARSKI:def 1;
then A23: U in G \ AA by A22, XBOOLE_0:def 5;
then S₁[U,q . U] by A18;
then A24: ( q . U in rng q & {(q . U)} = U /\ A ) by A19, FUNCT_1:def 3, A23;
x in A /\ U by A20, A21, XBOOLE_0:def 4;
hence x in rng q by A24, TARSKI:def 1; :: thesis: verum

end;

then A25: card A c= card (G \ AA) by A19, CARD_1:12;
card (G \ AA) c= card G by CARD_1:11, XBOOLE_1:36;
then card A c= card G by A25;
hence card A c= C by A15; :: thesis: verum

end;

end;