Theorem xrge0tps

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

	Ref	Expression
Assertion	xrge0tps	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp

Proof

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