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, +∞] \in TopSp$

Step	Hyp	Ref	Expression
1		xrstps	$⊢ ℝ_{𝑠}^{*} \in TopSp$
2		ovex	$⊢ [0, +∞] \in V$
3		resstps	$⊢ (ℝ_{𝑠}^{} \in TopSp \land [0, +∞] \in V) \to ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] \in TopSp$
4	1 2 3	mp2an	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in TopSp$