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

Metamath Proof Explorer

Theorem xrsle

Description: The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion xrsle ⊢ ≤ = ≤ ℝ 𝑠 *

Proof

Step Hyp Ref Expression
1 xrex ⊢ ℝ * ∈ V
2 1 1 xpex ⊢ ℝ * × ℝ * ∈ V
3 lerelxr ⊢ ≤ ⊆ ℝ * × ℝ *
4 2 3 ssexi ⊢ ≤ ∈ V
5 df-xrs ⊢ ℝ 𝑠 * = Base ndx ℝ * + ndx + 𝑒 ⋅ ndx ⋅ 𝑒 ∪ TopSet ⁡ ndx ordTop ⁡ ≤ ≤ ndx ≤ dist ⁡ ndx x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y
6 5 odrngle ⊢ ≤ ∈ V → ≤ = ≤ ℝ 𝑠 *
7 4 6 ax-mp ⊢ ≤ = ≤ ℝ 𝑠 *