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

Metamath Proof Explorer

Theorem cpnnen

Proof