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

Metamath Proof Explorer

Theorem xrstps

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

Ref Expression
Assertion xrstps ⊢ ℝ 𝑠 * ∈ TopSp

Proof

Step Hyp Ref Expression
1 letopon ⊢ ordTop ⁡ ≤ ∈ TopOn ⁡ ℝ *
2 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
3 xrstset ⊢ ordTop ⁡ ≤ = TopSet ⁡ ℝ 𝑠 *
4 2 3 tsettps ⊢ ordTop ⁡ ≤ ∈ TopOn ⁡ ℝ * → ℝ 𝑠 * ∈ TopSp
5 1 4 ax-mp ⊢ ℝ 𝑠 * ∈ TopSp