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	$⊢ ℂ \approx 𝒫 ℕ$

Proof

Step	Hyp	Ref	Expression
1		rexpen	$⊢ ℝ^{2} \approx ℝ$
2		eleq1w	$⊢ v = x \to (v \in ℝ \leftrightarrow x \in ℝ)$
3		eleq1w	$⊢ w = y \to (w \in ℝ \leftrightarrow y \in ℝ)$
4	2 3	bi2anan9	$⊢ (v = x \land w = y) \to ((v \in ℝ \land w \in ℝ) \leftrightarrow (x \in ℝ \land y \in ℝ))$
5		oveq2	$⊢ w = y \to i w = i y$
6		oveq12	$⊢ (v = x \land i w = i y) \to v + i w = x + i y$
7	5 6	sylan2	$⊢ (v = x \land w = y) \to v + i w = x + i y$
8	7	eqeq2d	$⊢ (v = x \land w = y) \to (z = v + i w \leftrightarrow z = x + i y)$
9	4 8	anbi12d	$⊢ (v = x \land w = y) \to (((v \in ℝ \land w \in ℝ) \land z = v + i w) \leftrightarrow ((x \in ℝ \land y \in ℝ) \land z = x + i y))$
10	9	cbvoprab12v	$⊢ \{⟨⟨v, w⟩, z⟩ \| ((v \in ℝ \land w \in ℝ) \land z = v + i w)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in ℝ \land y \in ℝ) \land z = x + i y)\}$
11		df-mpo	$⊢ (x \in ℝ, y \in ℝ ⟼ x + i y) = \{⟨⟨x, y⟩, z⟩ \| ((x \in ℝ \land y \in ℝ) \land z = x + i y)\}$
12	10 11	eqtr4i	$⊢ \{⟨⟨v, w⟩, z⟩ \| ((v \in ℝ \land w \in ℝ) \land z = v + i w)\} = (x \in ℝ, y \in ℝ ⟼ x + i y)$
13	12	cnref1o	$⊢ \{⟨⟨v, w⟩, z⟩ \| ((v \in ℝ \land w \in ℝ) \land z = v + i w)\} : ℝ^{2} \underset{1-1 onto}{⟶} ℂ$
14		reex	$⊢ ℝ \in V$
15	14 14	xpex	$⊢ ℝ^{2} \in V$
16	15	f1oen	$⊢ \{⟨⟨v, w⟩, z⟩ \| ((v \in ℝ \land w \in ℝ) \land z = v + i w)\} : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \to ℝ^{2} \approx ℂ$
17	13 16	ax-mp	$⊢ ℝ^{2} \approx ℂ$
18	1 17	entr3i	$⊢ ℝ \approx ℂ$
19		rpnnen	$⊢ ℝ \approx 𝒫 ℕ$
20	18 19	entr3i	$⊢ ℂ \approx 𝒫 ℕ$

Metamath Proof Explorer

Theorem cpnnen

Proof