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

Metamath Proof Explorer

Theorem xrsbas

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

Ref Expression
Assertion xrsbas ⊢ ℝ * = Base ℝ 𝑠 *

Proof

Step Hyp Ref Expression
1 xrex ⊢ ℝ * ∈ V
2 df-xrs ⊢ ℝ 𝑠 * = Base ndx ℝ * + ndx + 𝑒 ⋅ ndx ⋅ 𝑒 ∪ TopSet ⁡ ndx ordTop ⁡ ≤ ≤ ndx ≤ dist ⁡ ndx x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y
3 2 odrngbas ⊢ ℝ * ∈ V → ℝ * = Base ℝ 𝑠 *
4 1 3 ax-mp ⊢ ℝ * = Base ℝ 𝑠 *