set S = Sorgenfrey-line ;
let U be Subset-Family of Sorgenfrey-line; METRIZTS:def 2 ( not U is open or not U is Cover of the carrier of Sorgenfrey-line or ex b1 being Element of bool (bool the carrier of Sorgenfrey-line) st
( b1 c= U & b1 is Cover of the carrier of Sorgenfrey-line & b1 is countable ) )
assume that
A1:
U is open
and
A2:
U is Cover of Sorgenfrey-line
; ex b1 being Element of bool (bool the carrier of Sorgenfrey-line) st
( b1 c= U & b1 is Cover of the carrier of Sorgenfrey-line & b1 is countable )
A3:
U <> {}
set V = { (Int u) where u is Subset of R^1 : u in U } ;
set W = union { (Int u) where u is Subset of R^1 : u in U } ;
reconsider K = ([#] Sorgenfrey-line) \ (union { (Int u) where u is Subset of R^1 : u in U } ) as set ;
{ (Int u) where u is Subset of R^1 : u in U } is non empty Subset-Family of R^1
then reconsider V = { (Int u) where u is Subset of R^1 : u in U } as non empty Subset-Family of R^1 ;
union { (Int u) where u is Subset of R^1 : u in U } c= [#] R^1
then reconsider W = union { (Int u) where u is Subset of R^1 : u in U } as Subset of R^1 ;
defpred S1[ object , object ] means ex y being Subset of R^1 st
( $2 = y & y in U & $1 = Int y );
A11:
for x being object st x in V holds
ex y being object st
( y in U & S1[x,y] )
proof
let x be
object ;
( x in V implies ex y being object st
( y in U & S1[x,y] ) )
assume A12:
x in V
;
ex y being object st
( y in U & S1[x,y] )
consider u being
Subset of
R^1 such that A13:
x = Int u
and A14:
u in U
by A12;
take
u
;
( u in U & S1[x,u] )
thus
u in U
by A14;
S1[x,u]
thus
S1[
x,
u]
by A13, A14;
verum
end;
consider h being Function of V,U such that
A15:
for x being object st x in V holds
S1[x,h . x]
from FUNCT_2:sch 1(A11);
A16:
for x being Element of V
for hx being Subset of R^1 st hx = h . x holds
x = Int hx
reconsider T = R^1 | W as SubSpace of R^1 ;
V c= bool ([#] T)
then reconsider V1 = V as non empty Subset-Family of T ;
A21:
V1 is open
A25:
the carrier of T c= union V
consider B being Subset-Family of T such that
A26:
B c= V
and
A27:
B is Cover of T
and
A28:
B is countable
by METRIZTS:def 2, A21, A25, SETFAM_1:def 11;
deffunc H1( object ) -> set = h . $1;
A29:
for x being object st x in B holds
H1(x) in U
consider f being Function of B,U such that
A30:
for x being object st x in B holds
f . x = H1(x)
from FUNCT_2:sch 2(A29);
reconsider Y = rng f as Subset-Family of Sorgenfrey-line by TOPS_2:2;
A31:
Y is Cover of W
A38:
card B c= omega
by CARD_3:def 14, A28;
dom f = B
by FUNCT_2:def 1, A3;
then
card (rng f) c= card B
by CARD_1:12;
then A39:
Y is countable
by CARD_3:def 14, A38, XBOOLE_1:1;
defpred S2[ object , object ] means ex S being set st
( S = $2 & $1 in S );
A40:
for x being object st x in K holds
ex y being object st
( y in U & S2[x,y] )
consider g being Function of K,U such that
A43:
for x being object st x in K holds
S2[x,g . x]
from FUNCT_2:sch 1(A40);
set Q = { [.p,r.[ where p, r is Real : r > p } ;
defpred S3[ object , object ] means ex S being set st
( S = $2 & S c= g . $1 & ex x, rx being Real st
( $1 = x & $2 = [.x,rx.[ ) );
A44:
for x being object st x in K holds
ex y being object st
( y in { [.p,r.[ where p, r is Real : r > p } & S3[x,y] )
proof
let x be
object ;
( x in K implies ex y being object st
( y in { [.p,r.[ where p, r is Real : r > p } & S3[x,y] ) )
assume A45:
x in K
;
ex y being object st
( y in { [.p,r.[ where p, r is Real : r > p } & S3[x,y] )
g . x in U
by FUNCT_2:5, A45, A3;
then reconsider gx =
g . x as
open Subset of
Sorgenfrey-line by A1, TOPS_2:def 1;
reconsider x1 =
x as
Point of
Sorgenfrey-line by A45;
S2[
x,
g . x]
by A43, A45;
then consider a being
Subset of
Sorgenfrey-line such that A46:
a in BB
and A47:
x1 in a
and A48:
a c= gx
by YELLOW_9:31, Lm8;
consider p,
r being
Real such that A49:
a = [.p,r.[
and
r > p
and
r is
rational
by Lm7, A46;
reconsider x2 =
x1 as
Real by A47, A49;
A50:
(
p <= x2 &
x2 < r )
by A47, A49, XXREAL_1:3;
set y =
[.x2,r.[;
take
[.x2,r.[
;
( [.x2,r.[ in { [.p,r.[ where p, r is Real : r > p } & S3[x,[.x2,r.[] )
A51:
[.x2,r.[ c= a
thus
[.x2,r.[ in { [.p,r.[ where p, r is Real : r > p }
by A50;
S3[x,[.x2,r.[]
thus
S3[
x,
[.x2,r.[]
by A51, A48, XBOOLE_1:1;
verum
end;
consider k being Function of K, { [.p,r.[ where p, r is Real : r > p } such that
A53:
for x being object st x in K holds
S3[x,k . x]
from FUNCT_2:sch 1(A44);
defpred S4[ object , object ] means ex S being set st
( S = $1 & $2 in S );
A54:
for x being object st x in rng k holds
ex y being object st
( y in RAT & S4[x,y] )
proof
let x be
object ;
( x in rng k implies ex y being object st
( y in RAT & S4[x,y] ) )
assume A55:
x in rng k
;
ex y being object st
( y in RAT & S4[x,y] )
x in { [.p,r.[ where p, r is Real : r > p }
by A55;
then consider p,
r being
Real such that A56:
x = [.p,r.[
and A57:
r > p
;
reconsider xx =
x as
set by TARSKI:1;
consider y being
Rational such that A58:
y in xx
by A56, A57, Lm4;
take
y
;
( y in RAT & S4[x,y] )
thus
y in RAT
by RAT_1:def 2;
S4[x,y]
take
xx
;
( xx = x & y in xx )
thus
(
xx = x &
y in xx )
by A58;
verum
end;
consider j being Function of (rng k),RAT such that
A59:
for x being object st x in rng k holds
S4[x,j . x]
from FUNCT_2:sch 1(A54);
A60:
for x, y being Element of Sorgenfrey-line st x in K & y in K & x <> y holds
k . x misses k . y
proof
let x,
y be
Element of
Sorgenfrey-line;
( x in K & y in K & x <> y implies k . x misses k . y )
assume that A61:
x in K
and A62:
y in K
and A63:
x <> y
;
k . x misses k . y
A64:
(
S3[
x,
k . x] &
S3[
y,
k . y] )
by A53, A61, A62;
A65:
(
g . x in U &
g . y in U )
by A3, A61, A62, FUNCT_2:5;
thus
(k . x) /\ (k . y) = {}
XBOOLE_0:def 7 verumproof
assume
not
(k . x) /\ (k . y) = {}
;
contradiction
then consider l being
object such that A66:
l in (k . x) /\ (k . y)
by XBOOLE_0:7;
A67:
(
l in k . x &
l in k . y )
by XBOOLE_0:def 4, A66;
S3[
x,
k . x]
by A53, A61;
then consider x1,
rx being
Real such that A68:
x = x1
and A69:
k . x = [.x1,rx.[
;
S3[
y,
k . y]
by A53, A62;
then consider y1,
ry being
Real such that A70:
y = y1
and A71:
k . y = [.y1,ry.[
;
reconsider l =
l as
Real by A69, A66;
A72:
(
x1 <= l &
l < rx )
by A69, A67, XXREAL_1:3;
A73:
(
y1 <= l &
l < ry )
by A71, A67, XXREAL_1:3;
per cases
( x1 < y1 or x1 > y1 )
by A63, XXREAL_0:1, A68, A70;
suppose A74:
x1 < y1
;
contradiction
y1 < rx
by A72, A73, XXREAL_0:2;
then A75:
y1 in ].x1,rx.[
by XXREAL_1:4, A74;
reconsider Y =
].x1,rx.[ as
Subset of
R^1 by TOPMETR:17;
Y c= k . x
by XXREAL_1:22, A69;
then A76:
Y c= g . x
by A64, XBOOLE_1:1;
reconsider gx =
g . x as
Subset of
R^1 by TOPGEN_3:def 2, TOPMETR:17, A65;
A77:
y in Int gx
by A76, BORSUK_5:40, A70, A75, TOPS_1:22;
Int gx in V
by A65;
then
y in union V
by A77, TARSKI:def 4;
hence
contradiction
by A62, XBOOLE_0:def 5;
verum end; suppose A78:
x1 > y1
;
contradiction
x1 < ry
by A72, A73, XXREAL_0:2;
then A79:
x1 in ].y1,ry.[
by XXREAL_1:4, A78;
reconsider X =
].y1,ry.[ as
Subset of
R^1 by TOPMETR:17;
X c= k . y
by XXREAL_1:22, A71;
then A80:
X c= g . y
by A64, XBOOLE_1:1;
reconsider gy =
g . y as
Subset of
R^1 by A65, TOPGEN_3:def 2, TOPMETR:17;
A81:
x in Int gy
by A80, BORSUK_5:40, A68, A79, TOPS_1:22;
Int gy in V
by A65;
then
x in union V
by A81, TARSKI:def 4;
hence
contradiction
by A61, XBOOLE_0:def 5;
verum end;
end;
end;
A82:
rng j c= RAT
;
A83:
dom j = rng k
by FUNCT_2:def 1;
A84:
j is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom j or not x2 in dom j or not j . x1 = j . x2 or x1 = x2 )
assume that A85:
x1 in dom j
and A86:
x2 in dom j
and A87:
j . x1 = j . x2
;
x1 = x2
reconsider x1 =
x1,
x2 =
x2 as
set by TARSKI:1;
consider y1 being
object such that A88:
(
y1 in dom k &
x1 = k . y1 )
by FUNCT_1:def 3, A85;
consider y2 being
object such that A89:
(
y2 in dom k &
x2 = k . y2 )
by FUNCT_1:def 3, A86;
A90:
(
y1 in K &
y2 in K )
by A88, A89;
(
S4[
x1,
j . x1] &
S4[
x2,
j . x2] )
by A85, A86, A59;
then
(k . y1) /\ (k . y2) <> {}
by A88, A89, XBOOLE_0:def 4, A87;
hence
x1 = x2
by A88, A89, A60, A90, XBOOLE_0:def 7;
verum
end;
A91:
card (rng k) c= omega
by TOPGEN_3:17, CARD_1:10, A82, A83, A84;
A92:
[.1,2.[ in { [.p,r.[ where p, r is Real : r > p }
;
then A93:
dom k = K
by FUNCT_2:def 1;
A94:
k is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom k or not x2 in dom k or not k . x1 = k . x2 or x1 = x2 )
assume that A95:
x1 in dom k
and A96:
x2 in dom k
and A97:
k . x1 = k . x2
;
x1 = x2
A98:
(
x1 in K &
x2 in K )
by A95, A96;
(
k . x1 in rng k &
k . x2 in rng k )
by A92, A95, A96, FUNCT_2:4;
then A99:
(
k . x1 in { [.p,r.[ where p, r is Real : r > p } &
k . x2 in { [.p,r.[ where p, r is Real : r > p } )
;
consider p1,
r1 being
Real such that A100:
k . x1 = [.p1,r1.[
and A101:
r1 > p1
by A99;
consider q being
Rational such that A102:
q in k . x1
by A100, A101, Lm4;
q in (k . x1) /\ (k . x2)
by A102, A97;
hence
x1 = x2
by A60, XBOOLE_0:def 7, A98;
verum
end;
A103:
card K c= card (rng k)
by CARD_1:10, A93, A94;
A104:
card K c= omega
by A103, A91, XBOOLE_1:1;
dom g = K
by FUNCT_2:def 1, A3;
then
card (rng g) c= card K
by CARD_1:12;
then A105:
rng g is countable
by CARD_3:def 14, A104, XBOOLE_1:1;
reconsider Z = rng g as Subset-Family of Sorgenfrey-line by TOPS_2:2;
A106:
Z is Cover of K
W c= [#] Sorgenfrey-line
then A109:
W \/ K = [#] Sorgenfrey-line
by XBOOLE_1:45;
A110:
Z \/ Y is Cover of [#] Sorgenfrey-line
reconsider G = Z \/ Y as Subset-Family of Sorgenfrey-line ;
take
G
; ( G c= U & G is Cover of the carrier of Sorgenfrey-line & G is countable )
thus
G c= U
by XBOOLE_1:8; ( G is Cover of the carrier of Sorgenfrey-line & G is countable )
thus
G is Cover of Sorgenfrey-line
by A110; G is countable
thus
G is countable
by CARD_2:85, A105, A39; verum