let M be non empty TopSpace; :: thesis: ( M is without_boundary & M is locally_euclidean implies M is first-countable )

assume A1: ( M is without_boundary & M is locally_euclidean ) ; :: thesis: M is first-countable

for p being Point of M ex B being Basis of p st B is countable

assume A1: ( M is without_boundary & M is locally_euclidean ) ; :: thesis: M is first-countable

for p being Point of M ex B being Basis of p st B is countable

proof

hence
M is first-countable
by FRECHET:def 2; :: thesis: verum
let p be Point of M; :: thesis: ex B being Basis of p st B is countable

consider U being a_neighborhood of p, n being Nat such that

A2: M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A1, MFOLD_0:6;

set TR = TOP-REAL n;

p in Int U by CONNSP_2:def 1;

then K1: ex W being Subset of M st

( W is open & W c= U & p in W ) by TOPS_1:22;

( not Ball ((0. (TOP-REAL n)),1) is empty & Ball ((0. (TOP-REAL n)),1) is ball ) ;

then Tball ((0. (TOP-REAL n)),1),(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic by Th10, METRIZTS:def 1;

then M | U,(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic by A2, K1, BORSUK_3:3;

then M | U, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by TSEP_1:93;

then consider f being Function of (M | U),TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) such that

A3: f is being_homeomorphism by T_0TOPSP:def 1;

A4: ( dom f = [#] (M | U) & rng f = [#] TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) & f is one-to-one & f is continuous & f " is continuous ) by A3, TOPS_2:def 5;

then A5: dom f = U by PRE_TOPC:def 5;

A6: f is onto by A4, FUNCT_2:def 3;

A7: Int U c= U by TOPS_1:16;

A8: p in Int U by CONNSP_2:def 1;

A9: p in dom f by CONNSP_2:def 1, A7, A5;

f . p in rng f by A8, A7, A5, FUNCT_1:3;

then reconsider q = f . p as Point of (TOP-REAL n) ;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

consider B1 being Basis of q such that

A10: B1 is countable by FRECHET:def 2;

reconsider A = bool the carrier of (TOP-REAL n) as non empty set ;

deffunc H_{1}( set ) -> Element of bool the carrier of M = ((f ") .: c_{1}) /\ (Int U);

set B = { H_{1}(X) where X is Element of A : X in B1 } ;

A11: card B1 c= omega by A10, CARD_3:def 14;

card { H_{1}(X) where X is Element of A : X in B1 } c= card B1
from TREES_2:sch 2();

then A12: card { H_{1}(X) where X is Element of A : X in B1 } c= omega
by A11;

for x being object st x in { H_{1}(X) where X is Element of A : X in B1 } holds

x in bool the carrier of M_{1}(X) where X is Element of A : X in B1 } as Subset-Family of M by TARSKI:def 3;

A14: for P being Subset of M st P in B holds

P is open

p in Y

for S being Subset of M st S is open & p in S holds

ex V being Subset of M st

( V in B & V c= S )

take B ; :: thesis: B is countable

thus B is countable by A12, CARD_3:def 14; :: thesis: verum

end;consider U being a_neighborhood of p, n being Nat such that

A2: M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A1, MFOLD_0:6;

set TR = TOP-REAL n;

p in Int U by CONNSP_2:def 1;

then K1: ex W being Subset of M st

( W is open & W c= U & p in W ) by TOPS_1:22;

( not Ball ((0. (TOP-REAL n)),1) is empty & Ball ((0. (TOP-REAL n)),1) is ball ) ;

then Tball ((0. (TOP-REAL n)),1),(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic by Th10, METRIZTS:def 1;

then M | U,(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic by A2, K1, BORSUK_3:3;

then M | U, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by TSEP_1:93;

then consider f being Function of (M | U),TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) such that

A3: f is being_homeomorphism by T_0TOPSP:def 1;

A4: ( dom f = [#] (M | U) & rng f = [#] TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) & f is one-to-one & f is continuous & f " is continuous ) by A3, TOPS_2:def 5;

then A5: dom f = U by PRE_TOPC:def 5;

A6: f is onto by A4, FUNCT_2:def 3;

A7: Int U c= U by TOPS_1:16;

A8: p in Int U by CONNSP_2:def 1;

A9: p in dom f by CONNSP_2:def 1, A7, A5;

f . p in rng f by A8, A7, A5, FUNCT_1:3;

then reconsider q = f . p as Point of (TOP-REAL n) ;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

consider B1 being Basis of q such that

A10: B1 is countable by FRECHET:def 2;

reconsider A = bool the carrier of (TOP-REAL n) as non empty set ;

deffunc H

set B = { H

A11: card B1 c= omega by A10, CARD_3:def 14;

card { H

then A12: card { H

for x being object st x in { H

x in bool the carrier of M

proof

then reconsider B = { H
let x be object ; :: thesis: ( x in { H_{1}(X) where X is Element of A : X in B1 } implies x in bool the carrier of M )

assume x in { H_{1}(X) where X is Element of A : X in B1 }
; :: thesis: x in bool the carrier of M

then consider X1 being Element of A such that

A13: ( x = H_{1}(X1) & X1 in B1 )
;

thus x in bool the carrier of M by A13; :: thesis: verum

end;assume x in { H

then consider X1 being Element of A such that

A13: ( x = H

thus x in bool the carrier of M by A13; :: thesis: verum

A14: for P being Subset of M st P in B holds

P is open

proof

for Y being set st Y in B holds
let P be Subset of M; :: thesis: ( P in B implies P is open )

assume P in B ; :: thesis: P is open

then consider X1 being Element of A such that

A15: ( P = H_{1}(X1) & X1 in B1 )
;

reconsider X1 = X1 as Subset of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) ;

reconsider X2 = X1 as Subset of (TOP-REAL n) ;

X2 in the topology of (TOP-REAL n) by PRE_TOPC:def 2, A15, YELLOW_8:12;

then A16: X1 is open by PRE_TOPC:def 2;

reconsider U1 = M | U as non empty TopStruct by A8, A7;

reconsider g = f " as Function of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),U1 ;

A17: g is being_homeomorphism by A3, TOPS_2:56;

A18: g .: X1 is open by A16, A17, TOPGRP_1:25;

g .: X1 in the topology of (M | U) by A18, PRE_TOPC:def 2;

then consider Q being Subset of M such that

A19: ( Q in the topology of M & g .: X1 = Q /\ ([#] (M | U)) ) by PRE_TOPC:def 4;

[#] (M | U) = U by PRE_TOPC:def 5;

then A20: P = Q /\ (U /\ (Int U)) by A19, A15, XBOOLE_1:16

.= Q /\ (Int U) by TOPS_1:16, XBOOLE_1:28 ;

Q is open by A19, PRE_TOPC:def 2;

hence P is open by A20; :: thesis: verum

end;assume P in B ; :: thesis: P is open

then consider X1 being Element of A such that

A15: ( P = H

reconsider X1 = X1 as Subset of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) ;

reconsider X2 = X1 as Subset of (TOP-REAL n) ;

X2 in the topology of (TOP-REAL n) by PRE_TOPC:def 2, A15, YELLOW_8:12;

then A16: X1 is open by PRE_TOPC:def 2;

reconsider U1 = M | U as non empty TopStruct by A8, A7;

reconsider g = f " as Function of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),U1 ;

A17: g is being_homeomorphism by A3, TOPS_2:56;

A18: g .: X1 is open by A16, A17, TOPGRP_1:25;

g .: X1 in the topology of (M | U) by A18, PRE_TOPC:def 2;

then consider Q being Subset of M such that

A19: ( Q in the topology of M & g .: X1 = Q /\ ([#] (M | U)) ) by PRE_TOPC:def 4;

[#] (M | U) = U by PRE_TOPC:def 5;

then A20: P = Q /\ (U /\ (Int U)) by A19, A15, XBOOLE_1:16

.= Q /\ (Int U) by TOPS_1:16, XBOOLE_1:28 ;

Q is open by A19, PRE_TOPC:def 2;

hence P is open by A20; :: thesis: verum

p in Y

proof

then A23:
p in Intersect B
by SETFAM_1:43;
let Y be set ; :: thesis: ( Y in B implies p in Y )

assume Y in B ; :: thesis: p in Y

then consider X1 being Element of A such that

A21: ( Y = H_{1}(X1) & X1 in B1 )
;

reconsider g = f as Function ;

[p,(g . p)] in g by A8, A7, A5, FUNCT_1:def 2;

then [q,p] in g ~ by RELAT_1:def 7;

then [q,p] in g " by A4, FUNCT_1:def 5;

then A22: [q,p] in f " by A6, A4, TOPS_2:def 4;

q in X1 by A21, YELLOW_8:12;

then p in (f ") .: X1 by A22, RELAT_1:def 13;

hence p in Y by A21, A8, XBOOLE_0:def 4; :: thesis: verum

end;assume Y in B ; :: thesis: p in Y

then consider X1 being Element of A such that

A21: ( Y = H

reconsider g = f as Function ;

[p,(g . p)] in g by A8, A7, A5, FUNCT_1:def 2;

then [q,p] in g ~ by RELAT_1:def 7;

then [q,p] in g " by A4, FUNCT_1:def 5;

then A22: [q,p] in f " by A6, A4, TOPS_2:def 4;

q in X1 by A21, YELLOW_8:12;

then p in (f ") .: X1 by A22, RELAT_1:def 13;

hence p in Y by A21, A8, XBOOLE_0:def 4; :: thesis: verum

for S being Subset of M st S is open & p in S holds

ex V being Subset of M st

( V in B & V c= S )

proof

then reconsider B = B as Basis of p by A14, A23, TOPS_2:def 1, YELLOW_8:def 1;
let S be Subset of M; :: thesis: ( S is open & p in S implies ex V being Subset of M st

( V in B & V c= S ) )

assume A24: ( S is open & p in S ) ; :: thesis: ex V being Subset of M st

( V in B & V c= S )

set S1 = S /\ ([#] (M | U));

S in the topology of M by A24, PRE_TOPC:def 2;

then A25: S /\ ([#] (M | U)) in the topology of (M | U) by PRE_TOPC:def 4;

reconsider U1 = M | U as non empty TopStruct by A8, A7;

reconsider S1 = S /\ ([#] (M | U)) as Subset of U1 ;

S1 is open by A25, PRE_TOPC:def 2;

then A26: f .: S1 is open by A3, TOPGRP_1:25;

reconsider S2 = f .: S1 as Subset of (TOP-REAL n) ;

K: f .: S1 in the topology of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by A26, PRE_TOPC:def 2;

reconsider g1 = f as Function ;

A28: [p,q] in f by A8, A7, A5, FUNCT_1:def 2;

p in S1 by A9, A24, XBOOLE_0:def 4;

then A29: q in S2 by A28, RELAT_1:def 13;

consider W being Subset of (TOP-REAL n) such that

A30: ( W in B1 & W c= S2 ) by A29, K, PRE_TOPC:def 2, YELLOW_8:13;

reconsider W = W as Element of A ;

set V = ((f ") .: W) /\ (Int U);

reconsider V = ((f ") .: W) /\ (Int U) as Subset of M ;

take V ; :: thesis: ( V in B & V c= S )

thus V in B by A30; :: thesis: V c= S

A31: g1 " = f " by A6, A4, TOPS_2:def 4;

A32: (f ") .: (f .: S1) = S1 by A31, A4, FUNCT_1:107;

A33: ((f ") .: W) /\ (Int U) c= (f ") .: W by XBOOLE_1:17;

A34: S1 c= S by XBOOLE_1:17;

(f ") .: W c= (f ") .: (f .: S1) by A30, RELAT_1:123;

hence V c= S by A33, A32, A34; :: thesis: verum

end;( V in B & V c= S ) )

assume A24: ( S is open & p in S ) ; :: thesis: ex V being Subset of M st

( V in B & V c= S )

set S1 = S /\ ([#] (M | U));

S in the topology of M by A24, PRE_TOPC:def 2;

then A25: S /\ ([#] (M | U)) in the topology of (M | U) by PRE_TOPC:def 4;

reconsider U1 = M | U as non empty TopStruct by A8, A7;

reconsider S1 = S /\ ([#] (M | U)) as Subset of U1 ;

S1 is open by A25, PRE_TOPC:def 2;

then A26: f .: S1 is open by A3, TOPGRP_1:25;

reconsider S2 = f .: S1 as Subset of (TOP-REAL n) ;

K: f .: S1 in the topology of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by A26, PRE_TOPC:def 2;

reconsider g1 = f as Function ;

A28: [p,q] in f by A8, A7, A5, FUNCT_1:def 2;

p in S1 by A9, A24, XBOOLE_0:def 4;

then A29: q in S2 by A28, RELAT_1:def 13;

consider W being Subset of (TOP-REAL n) such that

A30: ( W in B1 & W c= S2 ) by A29, K, PRE_TOPC:def 2, YELLOW_8:13;

reconsider W = W as Element of A ;

set V = ((f ") .: W) /\ (Int U);

reconsider V = ((f ") .: W) /\ (Int U) as Subset of M ;

take V ; :: thesis: ( V in B & V c= S )

thus V in B by A30; :: thesis: V c= S

A31: g1 " = f " by A6, A4, TOPS_2:def 4;

A32: (f ") .: (f .: S1) = S1 by A31, A4, FUNCT_1:107;

A33: ((f ") .: W) /\ (Int U) c= (f ") .: W by XBOOLE_1:17;

A34: S1 c= S by XBOOLE_1:17;

(f ") .: W c= (f ") .: (f .: S1) by A30, RELAT_1:123;

hence V c= S by A33, A32, A34; :: thesis: verum

take B ; :: thesis: B is countable

thus B is countable by A12, CARD_3:def 14; :: thesis: verum