let T be non empty TopSpace; ( 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
; 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; ( 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
; 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 ;
( x in B implies ex y being object st
( y in bool the carrier of T & S1[x,y] ) )
assume
x in B
;
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 )
;
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
;
( y in bool the carrier of T & S1[x,y] )thus
y in bool the
carrier of
T
;
S1[x,y]take
y
;
( 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;
verum end; suppose A8:
for
y being
set st
y in F holds
not
b c= y
;
ex y being object st
( y in bool the carrier of T & S1[x,y] )take y =
{} T;
( y in bool the carrier of T & S1[x,y] )thus
y in bool the
carrier of
T
;
S1[x,y]take
y
;
( 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;
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) \ {{}}; ( RNG c= F & RNG is Cover of T & RNG is countable )
A10:
dom p = B
by FUNCT_2:def 1;
thus
RNG c= F
( RNG is Cover of T & RNG is countable )
the carrier of T c= union RNG
proof
let y be
object ;
TARSKI:def 3 ( not y in the carrier of T or y in union RNG )
assume
y in the
carrier of
T
;
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;
verum
end;
then
[#] T = union RNG
by XBOOLE_0:def 10;
hence
RNG is Cover of T
by SETFAM_1:45; 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; verum