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

Metamath Proof Explorer

Theorem cnso

Description: The complex numbers can be linearly ordered. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion cnso ∃ 𝑥 𝑥 Or ℂ

Proof

Step Hyp Ref Expression
1 ltso ⊢ < Or ℝ
2 eqid ⊢ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } = { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) }
3 f1oiso ⊢ ( ( 𝑎 : ℝ –1-1-onto→ ℂ ∧ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } = { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ) → 𝑎 Isom < , { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ( ℝ , ℂ ) )
4 2 3 mpan2 ⊢ ( 𝑎 : ℝ –1-1-onto→ ℂ → 𝑎 Isom < , { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ( ℝ , ℂ ) )
5 isoso ⊢ ( 𝑎 Isom < , { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ( ℝ , ℂ ) → ( < Or ℝ ↔ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } Or ℂ ) )
6 soinxp ⊢ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } Or ℂ ↔ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ )
7 5 6 bitrdi ⊢ ( 𝑎 Isom < , { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ( ℝ , ℂ ) → ( < Or ℝ ↔ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ ) )
8 4 7 syl ⊢ ( 𝑎 : ℝ –1-1-onto→ ℂ → ( < Or ℝ ↔ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ ) )
9 1 8 mpbii ⊢ ( 𝑎 : ℝ –1-1-onto→ ℂ → ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ )
10 cnex ⊢ ℂ ∈ V
11 10 10 xpex ⊢ ( ℂ × ℂ ) ∈ V
12 11 inex2 ⊢ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) ∈ V
13 soeq1 ⊢ ( 𝑥 = ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) → ( 𝑥 Or ℂ ↔ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ ) )
14 12 13 spcev ⊢ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ → ∃ 𝑥 𝑥 Or ℂ )
15 9 14 syl ⊢ ( 𝑎 : ℝ –1-1-onto→ ℂ → ∃ 𝑥 𝑥 Or ℂ )
16 rpnnen ⊢ ℝ ≈ 𝒫 ℕ
17 cpnnen ⊢ ℂ ≈ 𝒫 ℕ
18 16 17 entr4i ⊢ ℝ ≈ ℂ
19 bren ⊢ ( ℝ ≈ ℂ ↔ ∃ 𝑎 𝑎 : ℝ –1-1-onto→ ℂ )
20 18 19 mpbi ⊢ ∃ 𝑎 𝑎 : ℝ –1-1-onto→ ℂ
21 15 20 exlimiiv ⊢ ∃ 𝑥 𝑥 Or ℂ