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 ⊢∃xxOrℂ

Proof

Step Hyp Ref Expression
1 ltso ⊢<Orℝ
2 eqid ⊢bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e=bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e
3 f1oiso ⊢a:ℝ⟶1-1 ontoℂ∧bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e=bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e→aIsom<,bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<eℝℂ
4 2 3 mpan2 ⊢a:ℝ⟶1-1 ontoℂ→aIsom<,bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<eℝℂ
5 isoso ⊢aIsom<,bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<eℝℂ→<Orℝ↔bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<eOrℂ
6 soinxp ⊢bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<eOrℂ↔bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e∩ℂ×ℂOrℂ
7 5 6 bitrdi ⊢aIsom<,bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<eℝℂ→<Orℝ↔bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e∩ℂ×ℂOrℂ
8 4 7 syl ⊢a:ℝ⟶1-1 ontoℂ→<Orℝ↔bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e∩ℂ×ℂOrℂ
9 1 8 mpbii ⊢a:ℝ⟶1-1 ontoℂ→bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e∩ℂ×ℂOrℂ
10 cnex ⊢ℂ∈V
11 10 10 xpex ⊢ℂ×ℂ∈V
12 11 inex2 ⊢bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e∩ℂ×ℂ∈V
13 soeq1 ⊢x=bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e∩ℂ×ℂ→xOrℂ↔bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e∩ℂ×ℂOrℂ
14 12 13 spcev ⊢bc|∃d∈ℝ∃e∈ℝb=a⁡d∧c=a⁡e∧d<e∩ℂ×ℂOrℂ→∃xxOrℂ
15 9 14 syl ⊢a:ℝ⟶1-1 ontoℂ→∃xxOrℂ
16 rpnnen ⊢ℝ≈𝒫ℕ
17 cpnnen ⊢ℂ≈𝒫ℕ
18 16 17 entr4i ⊢ℝ≈ℂ
19 bren ⊢ℝ≈ℂ↔∃aa:ℝ⟶1-1 ontoℂ
20 18 19 mpbi ⊢∃aa:ℝ⟶1-1 ontoℂ
21 15 20 exlimiiv ⊢∃xxOrℂ