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

Metamath Proof Explorer

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 focdmex ⊢ ( ( ℝ × ℝ ) ∈ V → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) : ( ℝ × ℝ ) –onto→ ℂ → ℂ ∈ V ) )
8 2 6 7 mp2 ⊢ ℂ ∈ V