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	⊢ ℂ ≈ 𝒫 ℕ

Proof

Step	Hyp	Ref	Expression
1		rexpen	⊢ ( ℝ × ℝ ) ≈ ℝ
2		eleq1w	⊢ ( 𝑣 = 𝑥 → ( 𝑣 ∈ ℝ ↔ 𝑥 ∈ ℝ ) )
3		eleq1w	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ ℝ ↔ 𝑦 ∈ ℝ ) )
4	2 3	bi2anan9	⊢ ( ( 𝑣 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ( 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) )
5		oveq2	⊢ ( 𝑤 = 𝑦 → ( i · 𝑤 ) = ( i · 𝑦 ) )
6		oveq12	⊢ ( ( 𝑣 = 𝑥 ∧ ( i · 𝑤 ) = ( i · 𝑦 ) ) → ( 𝑣 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
7	5 6	sylan2	⊢ ( ( 𝑣 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( 𝑣 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
8	7	eqeq2d	⊢ ( ( 𝑣 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( 𝑧 = ( 𝑣 + ( i · 𝑤 ) ) ↔ 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) ) )
9	4 8	anbi12d	⊢ ( ( 𝑣 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ( ( 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 = ( 𝑣 + ( i · 𝑤 ) ) ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) ) ) )
10	9	cbvoprab12v	⊢ { ⟨ ⟨ 𝑣 , 𝑤 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 = ( 𝑣 + ( i · 𝑤 ) ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) ) }
11		df-mpo	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) ) }
12	10 11	eqtr4i	⊢ { ⟨ ⟨ 𝑣 , 𝑤 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 = ( 𝑣 + ( i · 𝑤 ) ) ) } = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
13	12	cnref1o	⊢ { ⟨ ⟨ 𝑣 , 𝑤 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 = ( 𝑣 + ( i · 𝑤 ) ) ) } : ( ℝ × ℝ ) –1-1-onto→ ℂ
14		reex	⊢ ℝ ∈ V
15	14 14	xpex	⊢ ( ℝ × ℝ ) ∈ V
16	15	f1oen	⊢ ( { ⟨ ⟨ 𝑣 , 𝑤 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 = ( 𝑣 + ( i · 𝑤 ) ) ) } : ( ℝ × ℝ ) –1-1-onto→ ℂ → ( ℝ × ℝ ) ≈ ℂ )
17	13 16	ax-mp	⊢ ( ℝ × ℝ ) ≈ ℂ
18	1 17	entr3i	⊢ ℝ ≈ ℂ
19		rpnnen	⊢ ℝ ≈ 𝒫 ℕ
20	18 19	entr3i	⊢ ℂ ≈ 𝒫 ℕ