Metamath Proof Explorer

Theorem xrge0tps

Description: The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017)

Ref Expression
Assertion xrge0tps ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp

Proof

Step Hyp Ref Expression
1 xrstps ⊢ ℝ 𝑠 * ∈ TopSp
2 ovex ⊢ 0 +∞ ∈ V
3 resstps ⊢ ℝ 𝑠 * ∈ TopSp ∧ 0 +∞ ∈ V → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
4 1 2 3 mp2an ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp