reconsider y = REAL as Point of REAL? by Th27;
assume
REAL? is first-countable
; contradiction
then consider B being Basis of y such that
A1:
B is countable
;
consider h being sequence of B such that
A2:
rng h = B
by A1, CARD_3:96;
defpred S1[ object , object ] means ex m being Element of NAT st
( m = $1 & $2 in (h . $1) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ );
A3:
for n being object st n in NAT holds
ex x being object st
( x in REAL \ NAT & S1[n,x] )
proof
let n be
object ;
( n in NAT implies ex x being object st
( x in REAL \ NAT & S1[n,x] ) )
assume A4:
n in NAT
;
ex x being object st
( x in REAL \ NAT & S1[n,x] )
then reconsider m =
n as
Element of
NAT ;
n in dom h
by A4, FUNCT_2:def 1;
then A5:
h . n in rng h
by FUNCT_1:def 3;
then reconsider Bn =
h . n as
Subset of
REAL? by A2;
m in REAL
by XREAL_0:def 1;
then reconsider m9 =
m as
Point of
RealSpace by METRIC_1:def 13;
reconsider Kn =
Ball (
m9,
(1 / 4)) as
Subset of
R^1 by TOPMETR:12;
reconsider Bn =
Bn as
Subset of
REAL? ;
(
Bn is
open &
y in Bn )
by A5, YELLOW_8:12;
then consider An being
Subset of
R^1 such that A6:
An is
open
and A7:
NAT c= An
and A8:
Bn = (An \ NAT) \/ {REAL}
by Th28;
reconsider An9 =
An as
Subset of
R^1 ;
Kn is
open
by TOPMETR:14;
then A9:
An9 /\ Kn is
open
by A6, TOPS_1:11;
dist (
m9,
m9)
= 0
by METRIC_1:1;
then
m9 in Ball (
m9,
(1 / 4))
by METRIC_1:11;
then
n in An /\ (Ball (m9,(1 / 4)))
by A4, A7, XBOOLE_0:def 4;
then consider r being
Real such that A10:
r > 0
and A11:
Ball (
m9,
r)
c= An /\ Kn
by A9, TOPMETR:15;
reconsider r =
r as
Real ;
m < m + r
by A10, XREAL_1:29;
then
m - r < m
by XREAL_1:19;
then consider x being
Real such that A12:
m - r < x
and A13:
x < m
by XREAL_1:5;
reconsider x =
x as
Element of
REAL by XREAL_0:def 1;
take
x
;
( x in REAL \ NAT & S1[n,x] )
A14:
r < 1
A16:
not
x in NAT
hence
x in REAL \ NAT
by XBOOLE_0:def 5;
S1[n,x]
x + 0 < m + r
by A10, A13, XREAL_1:8;
then
x in { a where a is Real : ( m - r < a & a < m + r ) }
by A12;
then
x in ].(m - r),(m + r).[
by RCOMP_1:def 2;
then A19:
x in Ball (
m9,
r)
by Th7;
then
x in An
by A11, XBOOLE_0:def 4;
then
x in An \ NAT
by A16, XBOOLE_0:def 5;
then A20:
x in Bn
by A8, XBOOLE_0:def 3;
take
m
;
( m = n & x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ )
Ball (
m9,
(1 / 4))
= ].(m - (1 / 4)),(m + (1 / 4)).[
by Th7;
then
x in ].(m - (1 / 4)),(m + (1 / 4)).[
by A11, A19, XBOOLE_0:def 4;
hence
(
m = n &
x in (h . n) /\ ].(m - (1 / 4)),(m + (1 / 4)).[ )
by A20, XBOOLE_0:def 4;
verum
end;
consider S being Function such that
A21:
dom S = NAT
and
A22:
rng S c= REAL \ NAT
and
A23:
for n being object st n in NAT holds
S1[n,S . n]
from FUNCT_1:sch 6(A3);
reconsider S = S as sequence of R^1 by A21, A22, FUNCT_2:2, TOPMETR:17, XBOOLE_1:1;
reconsider O = rng S as Subset of R^1 ;
for n being Element of NAT holds S . n in ].(n - (1 / 4)),(n + (1 / 4)).[
then
O is closed
by Th9;
then A24:
([#] R^1) \ O is open
by PRE_TOPC:def 3;
set A = ((O `) \ NAT) \/ {REAL};
((O `) \ NAT) \/ {REAL} c= (REAL \ NAT) \/ {REAL}
then reconsider A = ((O `) \ NAT) \/ {REAL} as Subset of REAL? by Def8;
reconsider A = A as Subset of REAL? ;
NAT c= O `
then
( A is open & REAL in A )
by A24, Th28;
then consider V being Subset of REAL? such that
A26:
V in B
and
A27:
V c= A
by YELLOW_8:13;
consider n1 being object such that
A28:
n1 in dom h
and
A29:
V = h . n1
by A2, A26, FUNCT_1:def 3;
reconsider n = n1 as Element of NAT by A28;
for n being Element of NAT ex x being set st
( x in h . n & not x in A )
then
ex x being set st
( x in h . n & not x in A )
;
hence
contradiction
by A27, A29; verum