let T be non empty TopSpace; ( T is first-countable implies for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) ) )
assume A1:
T is first-countable
; for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
let x be Point of T; ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
consider B1 being Basis of x such that
A2:
B1 is countable
by A1;
consider f being sequence of B1 such that
A3:
rng f = B1
by A2, CARD_3:96;
defpred S1[ object , object ] means ex D1 being set st
( D1 = $1 & $2 = meet (f .: (succ D1)) );
A4:
for n being object st n in NAT holds
ex A being object st S1[n,A]
consider S being Function such that
A5:
dom S = NAT
and
A6:
for n being object st n in NAT holds
S1[n,S . n]
from CLASSES1:sch 1(A4);
A7:
rng S c= bool the carrier of T
then reconsider B = rng S as Subset-Family of T ;
reconsider B = B as Subset-Family of T ;
A10:
ex A being set st A in B
then A11:
Intersect B = meet B
by SETFAM_1:def 9;
for A being set st A in B holds
x in A
then A18:
x in meet B
by A10, SETFAM_1:def 1;
A19:
B c= the topology of T
for O being Subset of T st O is open & x in O holds
ex A being Subset of T st
( A in B & A c= O )
proof
let O be
Subset of
T;
( O is open & x in O implies ex A being Subset of T st
( A in B & A c= O ) )
assume
(
O is
open &
x in O )
;
ex A being Subset of T st
( A in B & A c= O )
then consider A1 being
Subset of
T such that A24:
A1 in B1
and A25:
A1 c= O
by YELLOW_8:def 1;
consider n being
object such that A26:
n in dom f
and A27:
A1 = f . n
by A3, A24, FUNCT_1:def 3;
reconsider n =
n as
set by TARSKI:1;
S . n in rng S
by A5, A26, FUNCT_1:def 3;
then reconsider A =
S . n as
Subset of
T by A7;
reconsider A =
A as
Subset of
T ;
take
A
;
( A in B & A c= O )
thus
A in B
by A5, A26, FUNCT_1:def 3;
A c= O
n in succ n
by ORDINAL1:6;
then
f . n in f .: (succ n)
by A26, FUNCT_1:def 6;
then A28:
meet (f .: (succ n)) c= A1
by A27, SETFAM_1:3;
S1[
n,
S . n]
by A26, A6;
then
S . n c= A1
by A28;
hence
A c= O
by A25;
verum
end;
then reconsider B = B as Basis of x by A19, A11, A18, TOPS_2:64, YELLOW_8:def 1;
take
B
; ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
take
S
; ( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
thus
dom S = NAT
by A5; ( rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
thus
rng S = B
; for n, m being Element of NAT st m >= n holds
S . m c= S . n
for n, m being Element of NAT st m >= n holds
S . m c= S . n
hence
for n, m being Element of NAT st m >= n holds
S . m c= S . n
; verum