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

Metamath Proof Explorer

Theorem relt

Description: The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018)

Ref Expression
Assertion relt ⊢ < = < ℝ fld

Proof

Step Hyp Ref Expression
1 dflt2 ⊢ < = ≤ ∖ I
2 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
3 2 ovexi ⊢ ℝ fld ∈ V
4 rele2 ⊢ ≤ = ≤ ℝ fld
5 eqid ⊢ < ℝ fld = < ℝ fld
6 4 5 pltfval ⊢ ℝ fld ∈ V → < ℝ fld = ≤ ∖ I
7 3 6 ax-mp ⊢ < ℝ fld = ≤ ∖ I
8 1 7 eqtr4i ⊢ < = < ℝ fld