Metamath Proof Explorer

Theorem rpnnen

Description: The cardinality of the continuum is the same as the powerset of _om . This is a stronger statement than ruc , which only asserts that RR is uncountable, i.e. has a cardinality larger than _om . The main proof is in two parts, rpnnen1 and rpnnen2 , each showing an injection in one direction, and this last part uses sbth to prove that the sets are equinumerous. By constructing explicit injections, we avoid the use of AC. (Contributed by Mario Carneiro, 13-May-2013) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion rpnnen 
|- RR ~~ ~P NN

Proof

Step Hyp Ref Expression
1 nnex 
 |-  NN e. _V
2 qex 
 |-  QQ e. _V
3 1 2 rpnnen1 
 |-  RR ~<_ ( QQ ^m NN )
4 qnnen 
 |-  QQ ~~ NN
5 1 canth2 
 |-  NN ~< ~P NN
6 ensdomtr 
 |-  ( ( QQ ~~ NN /\ NN ~< ~P NN ) -> QQ ~< ~P NN )
7 4 5 6 mp2an 
 |-  QQ ~< ~P NN
8 sdomdom 
 |-  ( QQ ~< ~P NN -> QQ ~<_ ~P NN )
9 mapdom1 
 |-  ( QQ ~<_ ~P NN -> ( QQ ^m NN ) ~<_ ( ~P NN ^m NN ) )
10 7 8 9 mp2b 
 |-  ( QQ ^m NN ) ~<_ ( ~P NN ^m NN )
11 1 pw2en 
 |-  ~P NN ~~ ( 2o ^m NN )
12 1 enref 
 |-  NN ~~ NN
13 mapen 
 |-  ( ( ~P NN ~~ ( 2o ^m NN ) /\ NN ~~ NN ) -> ( ~P NN ^m NN ) ~~ ( ( 2o ^m NN ) ^m NN ) )
14 11 12 13 mp2an 
 |-  ( ~P NN ^m NN ) ~~ ( ( 2o ^m NN ) ^m NN )
15 domentr 
 |-  ( ( ( QQ ^m NN ) ~<_ ( ~P NN ^m NN ) /\ ( ~P NN ^m NN ) ~~ ( ( 2o ^m NN ) ^m NN ) ) -> ( QQ ^m NN ) ~<_ ( ( 2o ^m NN ) ^m NN ) )
16 10 14 15 mp2an 
 |-  ( QQ ^m NN ) ~<_ ( ( 2o ^m NN ) ^m NN )
17 2onn 
 |-  2o e. _om
18 mapxpen 
 |-  ( ( 2o e. _om /\ NN e. _V /\ NN e. _V ) -> ( ( 2o ^m NN ) ^m NN ) ~~ ( 2o ^m ( NN X. NN ) ) )
19 17 1 1 18 mp3an 
 |-  ( ( 2o ^m NN ) ^m NN ) ~~ ( 2o ^m ( NN X. NN ) )
20 17 elexi 
 |-  2o e. _V
21 20 enref 
 |-  2o ~~ 2o
22 xpnnen 
 |-  ( NN X. NN ) ~~ NN
23 mapen 
 |-  ( ( 2o ~~ 2o /\ ( NN X. NN ) ~~ NN ) -> ( 2o ^m ( NN X. NN ) ) ~~ ( 2o ^m NN ) )
24 21 22 23 mp2an 
 |-  ( 2o ^m ( NN X. NN ) ) ~~ ( 2o ^m NN )
25 19 24 entri 
 |-  ( ( 2o ^m NN ) ^m NN ) ~~ ( 2o ^m NN )
26 25 11 entr4i 
 |-  ( ( 2o ^m NN ) ^m NN ) ~~ ~P NN
27 domentr 
 |-  ( ( ( QQ ^m NN ) ~<_ ( ( 2o ^m NN ) ^m NN ) /\ ( ( 2o ^m NN ) ^m NN ) ~~ ~P NN ) -> ( QQ ^m NN ) ~<_ ~P NN )
28 16 26 27 mp2an 
 |-  ( QQ ^m NN ) ~<_ ~P NN
29 domtr 
 |-  ( ( RR ~<_ ( QQ ^m NN ) /\ ( QQ ^m NN ) ~<_ ~P NN ) -> RR ~<_ ~P NN )
30 3 28 29 mp2an 
 |-  RR ~<_ ~P NN
31 rpnnen2 
 |-  ~P NN ~<_ ( 0 [,] 1 )
32 reex 
 |-  RR e. _V
33 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
34 ssdomg 
 |-  ( RR e. _V -> ( ( 0 [,] 1 ) C_ RR -> ( 0 [,] 1 ) ~<_ RR ) )
35 32 33 34 mp2 
 |-  ( 0 [,] 1 ) ~<_ RR
36 domtr 
 |-  ( ( ~P NN ~<_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) ~<_ RR ) -> ~P NN ~<_ RR )
37 31 35 36 mp2an 
 |-  ~P NN ~<_ RR
38 sbth 
 |-  ( ( RR ~<_ ~P NN /\ ~P NN ~<_ RR ) -> RR ~~ ~P NN )
39 30 37 38 mp2an 
 |-  RR ~~ ~P NN