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:57;
A2: card B c= omega by A1, CARD_3:def 14;
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 S1[ object , object ] means ex D2 being set st
( D2 = $2 & ( 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= D2 ) ) & ( ( for y being set st y in F holds
not b c= y ) implies $2 = {} ) ) ) );
A5: for x being object st x in B holds
ex y being object st
( y in bool the carrier of T & S1[x,y] )
proof
let x be object ; :: thesis: ( x in B implies ex y being object st
( y in bool the carrier of T & S1[x,y] ) )
assume x in B ; :: thesis: ex y being object st
( y in bool the carrier of T & S1[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 object st
( y in bool the carrier of T & S1[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 & S1[x,y] )
thus y in bool the carrier of T ; :: thesis: S1[x,y]
take y ; :: thesis: ( y = y & ( for b being Subset of T st b = x holds
( ( ex y being set st
( y in F & b c= y ) implies ( y in F & b c= y ) ) & ( ( for y being set st y in F holds
not b c= y ) implies y = {} ) ) ) )
thus ( y = y & ( for b being Subset of T st b = x holds
( ( ex y being set st
( y in F & b c= y ) implies ( y in F & b c= y ) ) & ( ( for y being set st y in F holds
not b c= y ) implies 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 object st
( y in bool the carrier of T & S1[x,y] )
take y = {} T; :: thesis: ( y in bool the carrier of T & S1[x,y] )
thus y in bool the carrier of T ; :: thesis: S1[x,y]
take y ; :: thesis: ( y = y & ( for b being Subset of T st b = x holds
( ( ex y being set st
( y in F & b c= y ) implies ( y in F & b c= y ) ) & ( ( for y being set st y in F holds
not b c= y ) implies y = {} ) ) ) )
thus ( y = y & ( for b being Subset of T st b = x holds
( ( ex y being set st
( y in F & b c= y ) implies ( y in F & b c= y ) ) & ( ( for y being set st y in F holds
not b c= y ) implies y = {} ) ) ) ) by A8; :: thesis: verum
end;
end;
end;
consider p being Function of B,(bool the carrier of T) such that
A9: for x being object st x in B holds
S1[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 object ; :: 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 object such that
A12: z in dom p and
A13: p . z = y by FUNCT_1:def 3;
reconsider z = z as Subset of T by A10, A12;
A14: S1[z,p . z] by A9, 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 A14;
hence y in F by A11, A13, ZFMISC_1:56; :: thesis: verum
end;
the carrier of T c= union RNG
proof
let y be object ; :: 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
A15: q in W and
A16: W in F by A3, PCOMPS_1:3;
W is open by A4, A16;
then consider U being Subset of T such that
A17: U in B and
A18: q in U and
A19: U c= W by A15, YELLOW_9:31;
A20: p . U in rng p by A10, A17, FUNCT_1:def 3;
then reconsider pU = p . U as Subset of T ;
S1[U,p . U] by A9, A17;
then A21: U c= pU by A16, A19;
then pU in RNG by A18, A20, ZFMISC_1:56;
hence y in union RNG by A18, A21, TARSKI:def 4; :: thesis: verum
end;
then [#] T = union RNG by XBOOLE_0:def 10;
hence RNG is Cover of T by SETFAM_1:45; :: thesis: RNG is countable
card (rng p) c= card B by A10, CARD_2:61;
then card (rng p) c= omega by A2;
then rng p is countable by CARD_3:def 14;
hence RNG is countable by CARD_3:95; :: thesis: verum