Metamath Proof Explorer

Theorem rexpen

Description: The real numbers are equinumerous to their own Cartesian product, even though it is not necessarily true that RR is well-orderable (so we cannot use infxpidm2 directly). (Contributed by NM, 30-Jul-2004) (Revised by Mario Carneiro, 16-Jun-2013)

Ref Expression
Assertion rexpen 
|- ( RR X. RR ) ~~ RR

Proof

Step Hyp Ref Expression
1 rpnnen 
 |-  RR ~~ ~P NN
2 nnenom 
 |-  NN ~~ _om
3 pwen 
 |-  ( NN ~~ _om -> ~P NN ~~ ~P _om )
4 2 3 ax-mp 
 |-  ~P NN ~~ ~P _om
5 1 4 entri 
 |-  RR ~~ ~P _om
6 omex 
 |-  _om e. _V
7 6 pw2en 
 |-  ~P _om ~~ ( 2o ^m _om )
8 5 7 entri 
 |-  RR ~~ ( 2o ^m _om )
9 xpen 
 |-  ( ( RR ~~ ( 2o ^m _om ) /\ RR ~~ ( 2o ^m _om ) ) -> ( RR X. RR ) ~~ ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) )
10 8 8 9 mp2an 
 |-  ( RR X. RR ) ~~ ( ( 2o ^m _om ) X. ( 2o ^m _om ) )
11 2onn 
 |-  2o e. _om
12 11 elexi 
 |-  2o e. _V
13 12 12 6 xpmapen 
 |-  ( ( 2o X. 2o ) ^m _om ) ~~ ( ( 2o ^m _om ) X. ( 2o ^m _om ) )
14 13 ensymi 
 |-  ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) ~~ ( ( 2o X. 2o ) ^m _om )
15 ssid 
 |-  2o C_ 2o
16 ssnnfi 
 |-  ( ( 2o e. _om /\ 2o C_ 2o ) -> 2o e. Fin )
17 11 15 16 mp2an 
 |-  2o e. Fin
18 xpfi 
 |-  ( ( 2o e. Fin /\ 2o e. Fin ) -> ( 2o X. 2o ) e. Fin )
19 17 17 18 mp2an 
 |-  ( 2o X. 2o ) e. Fin
20 isfinite 
 |-  ( ( 2o X. 2o ) e. Fin <-> ( 2o X. 2o ) ~< _om )
21 19 20 mpbi 
 |-  ( 2o X. 2o ) ~< _om
22 6 canth2 
 |-  _om ~< ~P _om
23 sdomtr 
 |-  ( ( ( 2o X. 2o ) ~< _om /\ _om ~< ~P _om ) -> ( 2o X. 2o ) ~< ~P _om )
24 21 22 23 mp2an 
 |-  ( 2o X. 2o ) ~< ~P _om
25 sdomdom 
 |-  ( ( 2o X. 2o ) ~< ~P _om -> ( 2o X. 2o ) ~<_ ~P _om )
26 24 25 ax-mp 
 |-  ( 2o X. 2o ) ~<_ ~P _om
27 domentr 
 |-  ( ( ( 2o X. 2o ) ~<_ ~P _om /\ ~P _om ~~ ( 2o ^m _om ) ) -> ( 2o X. 2o ) ~<_ ( 2o ^m _om ) )
28 26 7 27 mp2an 
 |-  ( 2o X. 2o ) ~<_ ( 2o ^m _om )
29 mapdom1 
 |-  ( ( 2o X. 2o ) ~<_ ( 2o ^m _om ) -> ( ( 2o X. 2o ) ^m _om ) ~<_ ( ( 2o ^m _om ) ^m _om ) )
30 28 29 ax-mp 
 |-  ( ( 2o X. 2o ) ^m _om ) ~<_ ( ( 2o ^m _om ) ^m _om )
31 mapxpen 
 |-  ( ( 2o e. _om /\ _om e. _V /\ _om e. _V ) -> ( ( 2o ^m _om ) ^m _om ) ~~ ( 2o ^m ( _om X. _om ) ) )
32 11 6 6 31 mp3an 
 |-  ( ( 2o ^m _om ) ^m _om ) ~~ ( 2o ^m ( _om X. _om ) )
33 12 enref 
 |-  2o ~~ 2o
34 xpomen 
 |-  ( _om X. _om ) ~~ _om
35 mapen 
 |-  ( ( 2o ~~ 2o /\ ( _om X. _om ) ~~ _om ) -> ( 2o ^m ( _om X. _om ) ) ~~ ( 2o ^m _om ) )
36 33 34 35 mp2an 
 |-  ( 2o ^m ( _om X. _om ) ) ~~ ( 2o ^m _om )
37 32 36 entri 
 |-  ( ( 2o ^m _om ) ^m _om ) ~~ ( 2o ^m _om )
38 domentr 
 |-  ( ( ( ( 2o X. 2o ) ^m _om ) ~<_ ( ( 2o ^m _om ) ^m _om ) /\ ( ( 2o ^m _om ) ^m _om ) ~~ ( 2o ^m _om ) ) -> ( ( 2o X. 2o ) ^m _om ) ~<_ ( 2o ^m _om ) )
39 30 37 38 mp2an 
 |-  ( ( 2o X. 2o ) ^m _om ) ~<_ ( 2o ^m _om )
40 endomtr 
 |-  ( ( ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) ~~ ( ( 2o X. 2o ) ^m _om ) /\ ( ( 2o X. 2o ) ^m _om ) ~<_ ( 2o ^m _om ) ) -> ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) ~<_ ( 2o ^m _om ) )
41 14 39 40 mp2an 
 |-  ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) ~<_ ( 2o ^m _om )
42 ovex 
 |-  ( 2o ^m _om ) e. _V
43 0ex 
 |-  (/) e. _V
44 42 43 xpsnen 
 |-  ( ( 2o ^m _om ) X. { (/) } ) ~~ ( 2o ^m _om )
45 44 ensymi 
 |-  ( 2o ^m _om ) ~~ ( ( 2o ^m _om ) X. { (/) } )
46 snfi 
 |-  { (/) } e. Fin
47 isfinite 
 |-  ( { (/) } e. Fin <-> { (/) } ~< _om )
48 46 47 mpbi 
 |-  { (/) } ~< _om
49 sdomtr 
 |-  ( ( { (/) } ~< _om /\ _om ~< ~P _om ) -> { (/) } ~< ~P _om )
50 48 22 49 mp2an 
 |-  { (/) } ~< ~P _om
51 sdomdom 
 |-  ( { (/) } ~< ~P _om -> { (/) } ~<_ ~P _om )
52 50 51 ax-mp 
 |-  { (/) } ~<_ ~P _om
53 domentr 
 |-  ( ( { (/) } ~<_ ~P _om /\ ~P _om ~~ ( 2o ^m _om ) ) -> { (/) } ~<_ ( 2o ^m _om ) )
54 52 7 53 mp2an 
 |-  { (/) } ~<_ ( 2o ^m _om )
55 42 xpdom2 
 |-  ( { (/) } ~<_ ( 2o ^m _om ) -> ( ( 2o ^m _om ) X. { (/) } ) ~<_ ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) )
56 54 55 ax-mp 
 |-  ( ( 2o ^m _om ) X. { (/) } ) ~<_ ( ( 2o ^m _om ) X. ( 2o ^m _om ) )
57 endomtr 
 |-  ( ( ( 2o ^m _om ) ~~ ( ( 2o ^m _om ) X. { (/) } ) /\ ( ( 2o ^m _om ) X. { (/) } ) ~<_ ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) ) -> ( 2o ^m _om ) ~<_ ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) )
58 45 56 57 mp2an 
 |-  ( 2o ^m _om ) ~<_ ( ( 2o ^m _om ) X. ( 2o ^m _om ) )
59 sbth 
 |-  ( ( ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) ~<_ ( 2o ^m _om ) /\ ( 2o ^m _om ) ~<_ ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) ) -> ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) ~~ ( 2o ^m _om ) )
60 41 58 59 mp2an 
 |-  ( ( 2o ^m _om ) X. ( 2o ^m _om ) ) ~~ ( 2o ^m _om )
61 10 60 entri 
 |-  ( RR X. RR ) ~~ ( 2o ^m _om )
62 61 8 entr4i 
 |-  ( RR X. RR ) ~~ RR