cnexALT

Description: The set of complex numbers exists. This theorem shows that ax-cnex is redundant if we assume ax-rep . See also ax-cnex . (Contributed by NM, 30-Jul-2004) (Revised by Mario Carneiro, 16-Jun-2013) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	cnexALT	$⊢ ℂ \in V$

Proof

Step	Hyp	Ref	Expression
1		reexALT	$⊢ ℝ \in V$
2	1 1	xpex	$⊢ ℝ^{2} \in V$
3		eqid	$⊢ (x \in ℝ, y \in ℝ ⟼ x + i y) = (x \in ℝ, y \in ℝ ⟼ x + i y)$
4	3	cnref1o	$⊢ (x \in ℝ, y \in ℝ ⟼ x + i y) : ℝ^{2} \underset{1-1 onto}{⟶} ℂ$
5		f1ofo	$⊢ (x \in ℝ, y \in ℝ ⟼ x + i y) : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \to (x \in ℝ, y \in ℝ ⟼ x + i y) : ℝ^{2} \underset{onto}{⟶} ℂ$
6	4 5	ax-mp	$⊢ (x \in ℝ, y \in ℝ ⟼ x + i y) : ℝ^{2} \underset{onto}{⟶} ℂ$
7		focdmex	$⊢ ℝ^{2} \in V \to ((x \in ℝ, y \in ℝ ⟼ x + i y) : ℝ^{2} \underset{onto}{⟶} ℂ \to ℂ \in V)$
8	2 6 7	mp2	$⊢ ℂ \in V$

Metamath Proof Explorer

Theorem cnexALT

Proof