Theorem xrstopn

Description: The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Assertion	xrstopn	$$⊢\mathrm{ordTop}\left(\le \right)=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}\right)$$

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	topontopn	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)\to \mathrm{ordTop}\left(\le \right)=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}\right)$$
5	1 4	ax-mp	$$⊢\mathrm{ordTop}\left(\le \right)=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}\right)$$