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

Metamath Proof Explorer

Theorem xrsstr

Description: The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion xrsstr ⊢ ℝ 𝑠 * Struct 1 12

Proof

Step Hyp Ref Expression
1 df-xrs ⊢ ℝ 𝑠 * = Base ndx ℝ * + ndx + 𝑒 ⋅ ndx ⋅ 𝑒 ∪ TopSet ⁡ ndx ordTop ⁡ ≤ ≤ ndx ≤ dist ⁡ ndx x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y
2 1 odrngstr ⊢ ℝ 𝑠 * Struct 1 12