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 A1: 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 )
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
A2: F is Cover of T and
A3: F is open ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable )
consider B being Basis of T such that
A4: B is countable by A1, TOPGEN_4:60;
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 A6: x in B ; :: thesis: ex y being set st
( y in bool the carrier of T & S₁[x,y] )
reconsider b = x as Subset of T by A6;

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
A7: ( y in F & b c= y ) ;
reconsider y = y as Subset of T by A7;
take Y = y; :: thesis: ( Y in bool the carrier of T & S₁[x,Y] )
thus ( Y in bool the carrier of T & S₁[x,Y] ) by 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 E = {} T; :: thesis: ( E in bool the carrier of T & S₁[x,E] )
thus ( E in bool the carrier of T & S₁[x,E] ) 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 & 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 = {} ) & y <> {} ) by A9, A11, A12, ZFMISC_1:64;
hence y in F by A12; :: thesis: verum

end;

thus RNG is Cover of T :: thesis: RNG is countable

proof

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 A13: y in the carrier of T ; :: thesis: y in union RNG
reconsider q = y as Point of T by A13;
consider W being Subset of T such that
A14: ( q in W & W in F ) by A2, PCOMPS_1:5;
W is open by A3, A14, TOPS_2:def 1;
then consider U being Subset of T such that
A15: ( U in B & q in U & U c= W ) by A14, YELLOW_9:31;
A16: p . U in rng p by A10, A15, FUNCT_1:def 5;
then reconsider pU = p . U as Subset of T ;
A17: ( pU in F & U c= pU ) by A9, A14, A15;
then pU in RNG by A15, A16, ZFMISC_1:64;
hence y in union RNG by A15, A17, 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: verum

end;

( card (rng p) c= card B & card B c= omega ) by A4, A10, CARD_2:80, CARD_3:def 15;
then card (rng p) c= omega by XBOOLE_1:1;
then rng p is countable by CARD_3:def 15;
hence RNG is countable by CARD_3:130; :: thesis: verum