Theorem xrge0haus

Description: The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017)

	Ref	Expression
Assertion	xrge0haus	$$⊢\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\in \mathrm{Haus}$$

Proof

Step	Hyp	Ref	Expression
1		xrge0topn	$$⊢\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]$$
2		xrhaus	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{Haus}$$
3		ovex	$$⊢\left[0,\mathrm{+\infty }\right]\in \mathrm{V}$$
4		resthaus	$$⊢\left(\mathrm{ordTop}\left(\le \right)\in \mathrm{Haus}\wedge \left[0,\mathrm{+\infty }\right]\in \mathrm{V}\right)\to \mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{Haus}$$
5	2 3 4	mp2an	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{Haus}$$
6	1 5	eqeltri	$$⊢\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\in \mathrm{Haus}$$