This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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