let T be non empty TopSpace; :: thesis: ( T is second-countable implies for F being Subset-Family of T st F is Cover of T & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable ) )
assume T is second-countable ; :: thesis: for F being Subset-Family of T st F is Cover of T & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable )
then consider B being Basis of T such that
A1: B is countable by TOPGEN_4:60;
A2: card B c= omega by A1, CARD_3:def 15;
let F be Subset-Family of T; :: thesis: ( F is Cover of T & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable ) )
assume that
A3: F is Cover of T and
A4: F is open ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable )
defpred S₁[ set , set ] means for b being Subset of T st b = $1 holds
( ( ex y being set st
( y in F & b c= y ) implies ( $2 in F & b c= $2 ) ) & ( ( for y being set st y in F holds
not b c= y ) implies $2 = {} ) );
A5: for x being set st x in B holds
ex y being set st
( y in bool the carrier of T & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in B implies ex y being set st
( y in bool the carrier of T & S₁[x,y] ) )
assume x in B ; :: thesis: ex y being set st
( y in bool the carrier of T & S₁[x,y] )
then reconsider b = x as Subset of T ;

per cases ( ex y being set st
( y in F & b c= y ) or for y being set st y in F holds
not b c= y ) ;

suppose ex y being set st
( y in F & b c= y ) ; :: thesis: ex y being set st
( y in bool the carrier of T & S₁[x,y] )

then consider y being set such that
A6: y in F and
A7: b c= y ;
reconsider y = y as Subset of T by A6;
take y ; :: thesis: ( y in bool the carrier of T & S₁[x,y] )
thus ( y in bool the carrier of T & S₁[x,y] ) by A6, A7; :: thesis: verum

end;

suppose A8: for y being set st y in F holds
not b c= y ; :: thesis: ex y being set st
( y in bool the carrier of T & S₁[x,y] )

take {} T ; :: thesis: ( {} T in bool the carrier of T & S₁[x, {} T] )
thus ( {} T in bool the carrier of T & S₁[x, {} T] ) by A8; :: thesis: verum

end;

end;

end;

consider p being Function of B,(bool the carrier of T) such that
A9: for x being set st x in B holds
S₁[x,p . x] from FUNCT_2:sch 1(A5);
take RNG = (rng p) \ {{}}; :: thesis: ( RNG c= F & RNG is Cover of T & RNG is countable )
A10: dom p = B by FUNCT_2:def 1;
thus RNG c= F :: thesis: ( RNG is Cover of T & RNG is countable )

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in RNG or y in F )
assume A11: y in RNG ; :: thesis: y in F
y in rng p by A11, XBOOLE_0:def 5;
then consider z being set such that
A12: z in dom p and
A13: p . z = y by FUNCT_1:def 5;
reconsider z = z as Subset of T by A10, A12;
( ex y being set st
( y in F & z c= y ) or for y being set st y in F holds
not z c= y ) ;
then ( ( p . z in F & z c= p . z ) or p . z = {} ) by A9, A12;
hence y in F by A11, A13, ZFMISC_1:64; :: thesis: verum

end;

the carrier of T c= union RNG

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of T or y in union RNG )
assume y in the carrier of T ; :: thesis: y in union RNG
then reconsider q = y as Point of T ;
consider W being Subset of T such that
A14: q in W and
A15: W in F by A3, PCOMPS_1:5;
W is open by A4, A15, TOPS_2:def 1;
then consider U being Subset of T such that
A16: U in B and
A17: q in U and
A18: U c= W by A14, YELLOW_9:31;
A19: p . U in rng p by A10, A16, FUNCT_1:def 5;
then reconsider pU = p . U as Subset of T ;
A20: U c= pU by A9, A15, A16, A18;
then pU in RNG by A17, A19, ZFMISC_1:64;
hence y in union RNG by A17, A20, TARSKI:def 4; :: thesis: verum

end;

then [#] T = union RNG by XBOOLE_0:def 10;
hence RNG is Cover of T by SETFAM_1:60; :: thesis: RNG is countable
card (rng p) c= card B by A10, CARD_2:80;
then card (rng p) c= omega by A2, XBOOLE_1:1;
then rng p is countable by CARD_3:def 15;
hence RNG is countable by CARD_3:130; :: thesis: verum