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	⊢ ℂ ∈ V

Proof

Step	Hyp	Ref	Expression
1		reexALT	⊢ ℝ ∈ V
2	1 1	xpex	⊢ ( ℝ × ℝ ) ∈ V
3		eqid	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
4	3	cnref1o	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) : ( ℝ × ℝ ) –1-1-onto→ ℂ
5		f1ofo	⊢ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) : ( ℝ × ℝ ) –1-1-onto→ ℂ → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) : ( ℝ × ℝ ) –onto→ ℂ )
6	4 5	ax-mp	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) : ( ℝ × ℝ ) –onto→ ℂ
7		fornex	⊢ ( ( ℝ × ℝ ) ∈ V → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) : ( ℝ × ℝ ) –onto→ ℂ → ℂ ∈ V ) )
8	2 6 7	mp2	⊢ ℂ ∈ V