Theorem xrstps

Description: The extended real number structure is a topological space. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Assertion	xrstps	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		letopon	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
2		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
3		xrstset	$$⊢\mathrm{ordTop}\left(\le \right)=\mathrm{TopSet}\left({ℝ}_{𝑠}^{*}\right)$$
4	2 3	tsettps	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)\to {ℝ}_{𝑠}^{*}\in \mathrm{TopSp}$$
5	1 4	ax-mp	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{TopSp}$$