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

Metamath Proof Explorer

Theorem retos

Description: The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018)

Ref Expression
Assertion retos ⊢ ℝ fld ∈ Toset

Proof

Step Hyp Ref Expression
1 ltso ⊢ < Or ℝ
2 idref ⊢ I ↾ ℝ ⊆ ≤ ↔ ∀ x ∈ ℝ x ≤ x
3 leid ⊢ x ∈ ℝ → x ≤ x
4 2 3 mprgbir ⊢ I ↾ ℝ ⊆ ≤
5 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
6 5 ovexi ⊢ ℝ fld ∈ V
7 rebase ⊢ ℝ = Base ℝ fld
8 rele2 ⊢ ≤ = ≤ ℝ fld
9 relt ⊢ < = < ℝ fld
10 7 8 9 tosso ⊢ ℝ fld ∈ V → ℝ fld ∈ Toset ↔ < Or ℝ ∧ I ↾ ℝ ⊆ ≤
11 6 10 ax-mp ⊢ ℝ fld ∈ Toset ↔ < Or ℝ ∧ I ↾ ℝ ⊆ ≤
12 1 4 11 mpbir2an ⊢ ℝ fld ∈ Toset