Theorem 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 \mathrm{V}$$

Proof

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