defpred S1[ object , object ] means ex x, q being Element of REAL st
( $1 = x & $2 = [.x,q.[ & x < q & q is rational );
deffunc H1( Element of [:REAL,RAT:]) -> Element of bool REAL = [.($1 `1),($1 `2).[;
set X = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ;
consider f being Function such that
A1:
dom f = [:REAL,RAT:]
and
A2:
for z being Element of [:REAL,RAT:] holds f . z = H1(z)
from FUNCT_1:sch 4();
A3:
{ [.x,q.[ where x, q is Real : ( x < q & q is rational ) } c= rng f
proof
let a be
object ;
TARSKI:def 3 ( not a in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } or a in rng f )
assume
a in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) }
;
a in rng f
then consider x,
q being
Real such that A4:
a = [.x,q.[
and
x < q
and A5:
q is
rational
;
(
x in REAL &
q in RAT )
by A5, RAT_1:def 2, XREAL_0:def 1;
then reconsider b =
[x,q] as
Element of
[:REAL,RAT:] by ZFMISC_1:def 2;
A6:
b `2 = q
;
b `1 = x
;
then
f . b = [.x,q.[
by A6, A2;
hence
a in rng f
by A1, A4, FUNCT_1:def 3;
verum
end;
card omega c= card REAL
by CARD_1:11, NUMBERS:19;
then A7:
omega c= continuum
;
card [:REAL,RAT:] =
card [:(card REAL),(card RAT):]
by CARD_2:7
.=
continuum *` omega
by Th17, CARD_2:def 2
.=
continuum
by A7, CARD_4:16
;
hence
card { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } c= continuum
by A1, A3, CARD_1:12; XBOOLE_0:def 10 continuum c= card { [.x,q.[ where x, q is Real : ( x < q & q is rational ) }
A8:
for a being object st a in REAL holds
ex b being object st
( b in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } & S1[a,b] )
proof
let a be
object ;
( a in REAL implies ex b being object st
( b in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } & S1[a,b] ) )
assume
a in REAL
;
ex b being object st
( b in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } & S1[a,b] )
then reconsider x =
a as
Element of
REAL ;
x + 0 < x + 1
by XREAL_1:6;
then consider q being
Rational such that A9:
x < q
and
q < x + 1
by RAT_1:7;
q in RAT
by RAT_1:def 2;
then reconsider q =
q as
Element of
REAL by NUMBERS:12;
[.x,q.[ in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) }
by A9;
hence
ex
b being
object st
(
b in { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } &
S1[
a,
b] )
by A9;
verum
end;
consider f being Function such that
A10:
( dom f = REAL & rng f c= { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } & ( for a being object st a in REAL holds
S1[a,f . a] ) )
from FUNCT_1:sch 6(A8);
f is one-to-one
proof
let a,
b be
object ;
FUNCT_1:def 4 ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume
a in dom f
;
( not b in dom f or not f . a = f . b or a = b )
then consider x,
q being
Element of
REAL such that A11:
a = x
and A12:
f . a = [.x,q.[
and A13:
x < q
and
q is
rational
by A10;
assume
b in dom f
;
( not f . a = f . b or a = b )
then consider y,
r being
Element of
REAL such that A14:
b = y
and A15:
f . b = [.y,r.[
and A16:
y < r
and
r is
rational
by A10;
assume A17:
f . a = f . b
;
a = b
then
y in [.x,q.[
by A12, A15, A16, XXREAL_1:3;
then A18:
x <= y
by XXREAL_1:3;
x in [.y,r.[
by A17, A12, A13, A15, XXREAL_1:3;
then
y <= x
by XXREAL_1:3;
hence
a = b
by A18, A11, A14, XXREAL_0:1;
verum
end;
hence
continuum c= card { [.x,q.[ where x, q is Real : ( x < q & q is rational ) }
by A10, CARD_1:10; verum