Theorem xrge0topn

Description: The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017)

	Ref	Expression
Assertion	xrge0topn	$$⊢\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]$$
2		xrstopn	$$⊢\mathrm{ordTop}\left(\le \right)=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}\right)$$
3	1 2	resstopn	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$$
4	3	eqcomi	$$⊢\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]$$