Metamath Proof Explorer

Theorem cpnnen

Description: The complex numbers are equinumerous to the powerset of the positive integers. (Contributed by Mario Carneiro, 16-Jun-2013)

Ref Expression
Assertion cpnnen 
|- CC ~~ ~P NN

Proof

Step Hyp Ref Expression
1 rexpen 
 |-  ( RR X. RR ) ~~ RR
2 eleq1w 
 |-  ( v = x -> ( v e. RR <-> x e. RR ) )
3 eleq1w 
 |-  ( w = y -> ( w e. RR <-> y e. RR ) )
4 2 3 bi2anan9 
 |-  ( ( v = x /\ w = y ) -> ( ( v e. RR /\ w e. RR ) <-> ( x e. RR /\ y e. RR ) ) )
5 oveq2 
 |-  ( w = y -> ( _i x. w ) = ( _i x. y ) )
6 oveq12 
 |-  ( ( v = x /\ ( _i x. w ) = ( _i x. y ) ) -> ( v + ( _i x. w ) ) = ( x + ( _i x. y ) ) )
7 5 6 sylan2 
 |-  ( ( v = x /\ w = y ) -> ( v + ( _i x. w ) ) = ( x + ( _i x. y ) ) )
8 7 eqeq2d 
 |-  ( ( v = x /\ w = y ) -> ( z = ( v + ( _i x. w ) ) <-> z = ( x + ( _i x. y ) ) ) )
9 4 8 anbi12d 
 |-  ( ( v = x /\ w = y ) -> ( ( ( v e. RR /\ w e. RR ) /\ z = ( v + ( _i x. w ) ) ) <-> ( ( x e. RR /\ y e. RR ) /\ z = ( x + ( _i x. y ) ) ) ) )
10 9 cbvoprab12v 
 |-  { <. <. v , w >. , z >. | ( ( v e. RR /\ w e. RR ) /\ z = ( v + ( _i x. w ) ) ) } = { <. <. x , y >. , z >. | ( ( x e. RR /\ y e. RR ) /\ z = ( x + ( _i x. y ) ) ) }
11 df-mpo 
 |-  ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) = { <. <. x , y >. , z >. | ( ( x e. RR /\ y e. RR ) /\ z = ( x + ( _i x. y ) ) ) }
12 10 11 eqtr4i 
 |-  { <. <. v , w >. , z >. | ( ( v e. RR /\ w e. RR ) /\ z = ( v + ( _i x. w ) ) ) } = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
13 12 cnref1o 
 |-  { <. <. v , w >. , z >. | ( ( v e. RR /\ w e. RR ) /\ z = ( v + ( _i x. w ) ) ) } : ( RR X. RR ) -1-1-onto-> CC
14 reex 
 |-  RR e. _V
15 14 14 xpex 
 |-  ( RR X. RR ) e. _V
16 15 f1oen 
 |-  ( { <. <. v , w >. , z >. | ( ( v e. RR /\ w e. RR ) /\ z = ( v + ( _i x. w ) ) ) } : ( RR X. RR ) -1-1-onto-> CC -> ( RR X. RR ) ~~ CC )
17 13 16 ax-mp 
 |-  ( RR X. RR ) ~~ CC
18 1 17 entr3i 
 |-  RR ~~ CC
19 rpnnen 
 |-  RR ~~ ~P NN
20 18 19 entr3i 
 |-  CC ~~ ~P NN