not [0,0] in RAT+
by ARYTM_3:33;
then A1:
RAT = RAT+ \/ ([:{0},RAT+:] \ {[0,0]})
by NUMBERS:def 3, XBOOLE_1:87, ZFMISC_1:50;
then
bool RAT+ c= bool RAT
by XBOOLE_1:7, ZFMISC_1:67;
then A2:
DEDEKIND_CUTS c= bool RAT
;
RAT+ c= RAT
by A1, XBOOLE_1:7;
then
RAT+ \/ DEDEKIND_CUTS c= RAT \/ (bool RAT)
by A2, XBOOLE_1:13;
then
REAL+ c= RAT \/ (bool RAT)
by ARYTM_2:def 2;
then A3:
card REAL+ c= card (RAT \/ (bool RAT))
by CARD_1:11;
set INFNAT = (bool NAT) \ (Fin NAT);
A4:
card RAT in card (bool RAT)
by CARD_1:14;
card (RAT \/ (bool RAT)) c= (card RAT) +` (card (bool RAT))
by CARD_2:34;
then
card REAL+ c= (card RAT) +` (card (bool RAT))
by A3;
then
card REAL+ c= card (bool RAT)
by A4, CARD_2:76;
then
card REAL+ c= exp (2,omega)
by Th17, CARD_2:31;
then
(card REAL+) +` (card REAL+) c= (exp (2,omega)) +` (exp (2,omega))
by CARD_2:83;
then A5:
(card REAL+) +` (card REAL+) c= exp (2,omega)
by CARD_2:76;
deffunc H1( set ) -> Element of REAL = In ((Sum ($1 -powers (1 / 2))),REAL);
A6: card [:{0},REAL+:] =
card [:REAL+,{0}:]
by CARD_2:4
.=
card REAL+
by CARD_1:69
;
A7:
continuum c= card (REAL+ \/ [:{0},REAL+:])
by CARD_1:11, NUMBERS:def 1;
card (REAL+ \/ [:{0},REAL+:]) c= (card REAL+) +` (card [:{0},REAL+:])
by CARD_2:34;
then
continuum c= (card REAL+) +` (card REAL+)
by A7, A6;
hence
continuum c= exp (2,omega)
by A5; XBOOLE_0:def 10 exp (2,omega) c= continuum
Fin NAT is countable
by Th28, CARD_4:2;
then A8:
card (Fin NAT) c= omega
;
then
card (Fin NAT) in card (bool NAT)
by CARD_1:14, CARD_1:47, ORDINAL1:12;
then A9:
(card (bool NAT)) +` (card (Fin NAT)) = card (bool NAT)
by CARD_2:76;
A10:
omega in card (bool NAT)
by CARD_1:14, CARD_1:47;
then reconsider INFNAT = (bool NAT) \ (Fin NAT) as non empty set by A8, CARD_1:68, ORDINAL1:12;
consider f being Function of INFNAT,REAL such that
A11:
for X being Element of INFNAT holds f . X = H1(X)
from FUNCT_2:sch 4();
A12:
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 that A13:
a in dom f
and A14:
b in dom f
;
( not f . a = f . b or a = b )
reconsider a =
a,
b =
b as
set by TARSKI:1;
A15:
f . b = H1(
b)
by A11, A14;
not
b in Fin NAT
by A14, XBOOLE_0:def 5;
then A16:
b is
infinite Subset of
NAT
by A14, FINSUB_1:def 5, XBOOLE_0:def 5;
not
a in Fin NAT
by A13, XBOOLE_0:def 5;
then A17:
a is
infinite Subset of
NAT
by A13, FINSUB_1:def 5, XBOOLE_0:def 5;
f . a = H1(
a)
by A11, A13;
hence
( not
f . a = f . b or
a = b )
by A17, A16, A15, Th27;
verum
end;
A18:
rng f c= REAL
by RELAT_1:def 19;
dom f = INFNAT
by FUNCT_2:def 1;
then
card INFNAT c= continuum
by A12, A18, CARD_1:10;
then
card (bool NAT) c= continuum
by A9, A8, A10, CARD_2:98, ORDINAL1:12;
hence
exp (2,omega) c= continuum
by CARD_1:47, CARD_2:31; verum