let T be non empty TopSpace; :: thesis: ( T is metrizable implies ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite )
assume A1: T is metrizable ; :: thesis: ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite
then consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that
A2: metr is_metric_of the carrier of T and
A3: Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T ;
set PM = SpaceMetr ( the carrier of T,metr);
reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A2, PCOMPS_1:36;
deffunc H1( Element of NAT ) -> set = { (Ball (x,(1 / (2 |^ $1)))) where x is Element of PM : x is Element of PM } ;
defpred S1[ Element of NAT , set ] means $2 = H1($1);
A4: for k being Element of NAT ex y being Subset-Family of T st S1[k,y]
proof
let k be Element of NAT ; :: thesis: ex y being Subset-Family of T st S1[k,y]
set Ak = H1(k);
H1(k) c= bool the carrier of T
proof
let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in H1(k) or B in bool the carrier of T )
assume B in H1(k) ; :: thesis: B in bool the carrier of T
then ex x being Element of PM st
( B = Ball (x,(1 / (2 |^ k))) & x is Element of PM ) ;
then B in Family_open_set PM by PCOMPS_1:29;
hence B in bool the carrier of T by A3; :: thesis: verum
end;
hence ex y being Subset-Family of T st S1[k,y] ; :: thesis: verum
end;
consider FB being sequence of (bool (bool the carrier of T)) such that
A5: for k being Element of NAT holds S1[k,FB . k] from FUNCT_2:sch 3(A4);
 defpred S2[ object , object ] means ex W being Subset-Family of T st
( W = $2 & W is open & W is Cover of T & W is_finer_than FB . $1 & W is locally_finite );
set TPM = TopSpaceMetr PM;
A6: [#] T = [#] (TopSpaceMetr PM) by A2, PCOMPS_2:4;
A7: for n being Element of NAT ex PP being Subset-Family of T st
( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite )
proof
let n be Element of NAT ; :: thesis: ex PP being Subset-Family of T st
( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite )
[#] (TopSpaceMetr PM) c= union (FB . n)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (TopSpaceMetr PM) or x in union (FB . n) )
assume x in [#] (TopSpaceMetr PM) ; :: thesis: x in union (FB . n)
then reconsider x9 = x as Element of PM ;
( dist (x9,x9) = 0 & 2 |^ n > 0 ) by METRIC_1:1, NEWTON:83;
then dist (x9,x9) < 1 / (2 |^ n) by XREAL_1:139;
then A8: x9 in Ball (x9,(1 / (2 |^ n))) by METRIC_1:11;
Ball (x9,(1 / (2 |^ n))) in H1(n) ;
then Ball (x9,(1 / (2 |^ n))) in FB . n by A5;
hence x in union (FB . n) by A8, TARSKI:def 4; :: thesis: verum
end;
then A9: FB . n is Cover of T by A6, SETFAM_1:def 11;
for U being Subset of T st U in FB . n holds
U is open
proof
let U be Subset of T; :: thesis: ( U in FB . n implies U is open )
assume U in FB . n ; :: thesis: U is open
then U in H1(n) by A5;
then ex x being Element of PM st
( U = Ball (x,(1 / (2 |^ n))) & x is Element of PM ) ;
then U in the topology of T by A3, PCOMPS_1:29;
hence U is open by PRE_TOPC:def 2; :: thesis: verum
end;
then FB . n is open by TOPS_2:def 1;
then ex PP being Subset-Family of T st
( PP is open & PP is Cover of T & PP is_finer_than FB . n & PP is locally_finite ) by A1, A9, PCOMPS_2:6;
hence ex PP being Subset-Family of T st
( PP is_finer_than FB . n & PP is Cover of T & PP is open & PP is locally_finite ) ; :: thesis: verum
end;
A10: for k being object st k in NAT holds
ex y being object st
( y in bool (bool the carrier of T) & S2[k,y] )
proof
let k be object ; :: thesis: ( k in NAT implies ex y being object st
( y in bool (bool the carrier of T) & S2[k,y] ) )
assume k in NAT ; :: thesis: ex y being object st
( y in bool (bool the carrier of T) & S2[k,y] )
then reconsider k = k as Element of NAT ;
ex PP being Subset-Family of T st
( PP is_finer_than FB . k & PP is Cover of T & PP is open & PP is locally_finite ) by A7;
hence ex y being object st
( y in bool (bool the carrier of T) & S2[k,y] ) ; :: thesis: verum
end;
consider UC being FamilySequence of T such that
A11: for x being object st x in NAT holds
S2[x,UC . x] from FUNCT_2:sch 1(A10);
 A12: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex B being Subset of T st
( B in Union UC & p in B & B c= A )
proof
let A be Subset of T; :: thesis: ( A is open implies for p being Point of T st p in A holds
ex B being Subset of T st
( B in Union UC & p in B & B c= A ) )
assume A is open ; :: thesis: for p being Point of T st p in A holds
ex B being Subset of T st
( B in Union UC & p in B & B c= A )
then A13: A in Family_open_set PM by A3, PRE_TOPC:def 2;
let p be Point of T; :: thesis: ( p in A implies ex B being Subset of T st
( B in Union UC & p in B & B c= A ) )
assume A14: p in A ; :: thesis: ex B being Subset of T st
( B in Union UC & p in B & B c= A )
then reconsider p = p as Element of PM by A13;
consider r1 being Real such that
A15: r1 > 0 and
A16: Ball (p,r1) c= A by A14, A13, PCOMPS_1:def 4;
consider n being Nat such that
A17: 1 / (2 |^ n) <= r1 by A15, PREPOWER:92;
A18: S2[n + 1,UC . (n + 1)] by A11;
then union (UC . (n + 1)) = the carrier of T by SETFAM_1:45;
then consider B being set such that
A19: p in B and
A20: B in UC . (n + 1) by TARSKI:def 4;
reconsider B = B as Subset of PM by A2, A20, PCOMPS_2:4;
consider B1 being set such that
A21: B1 in FB . (n + 1) and
A22: B c= B1 by A18, A20, SETFAM_1:def 2;
B1 in H1(n + 1) by A5, A21;
then consider q being Element of PM such that
A23: B1 = Ball (q,(1 / (2 |^ (n + 1)))) and
q is Element of PM ;
A24: dist (q,p) < 1 / (2 |^ (n + 1)) by A19, A22, A23, METRIC_1:11;
now :: thesis: for r being Element of PM st r in B holds
r in Ball (p,r1)
let r be Element of PM; :: thesis: ( r in B implies r in Ball (p,r1) )
assume r in B ; :: thesis: r in Ball (p,r1)
then dist (q,r) < 1 / (2 |^ (n + 1)) by A22, A23, METRIC_1:11;
then ( dist (p,r) <= (dist (q,p)) + (dist (q,r)) & (dist (q,p)) + (dist (q,r)) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) ) by A24, METRIC_1:4, XREAL_1:8;
then dist (p,r) < 2 * (1 / (2 |^ (n + 1))) by XXREAL_0:2;
then dist (p,r) < (1 / ((2 |^ n) * 2)) * 2 by NEWTON:6;
then dist (p,r) < 1 / (2 |^ n) by XCMPLX_1:92;
then dist (p,r) < r1 by A17, XXREAL_0:2;
hence r in Ball (p,r1) by METRIC_1:11; :: thesis: verum
end;
then A25: B c= Ball (p,r1) ;
B in Union UC by A20, PROB_1:12;
hence ex B being Subset of T st
( B in Union UC & p in B & B c= A ) by A16, A19, A25, XBOOLE_1:1; :: thesis: verum
end;
for n being Element of NAT holds UC . n is locally_finite
proof
let n be Element of NAT ; :: thesis: UC . n is locally_finite
S2[n,UC . n] by A11;
hence UC . n is locally_finite ; :: thesis: verum
end;
then A26: UC is sigma_locally_finite ;
Union UC c= the topology of T
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Union UC or u in the topology of T )
assume u in Union UC ; :: thesis: u in the topology of T
then consider k being Nat such that
A27: u in UC . k by PROB_1:12;
A28: k in NAT by ORDINAL1:def 12;
reconsider u9 = u as Subset of T by A27;
S2[k,UC . k] by A11, A28;
then u9 is open by A27, TOPS_2:def 1;
hence u in the topology of T by PRE_TOPC:def 2; :: thesis: verum
end;
then Union UC is Basis of T by A12, YELLOW_9:32;
then UC is Basis_sigma_locally_finite by A26;
hence ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite ; :: thesis: verum