Theorem xrstopn

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

	Ref	Expression
Assertion	xrstopn	⊢ ( ordTop ‘ ≤ ) = ( TopOpen ‘ ℝ*𝑠 )

Proof

Step	Hyp	Ref	Expression
1		letopon	⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
2		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
3		xrstset	⊢ ( ordTop ‘ ≤ ) = ( TopSet ‘ ℝ*𝑠 )
4	2 3	topontopn	⊢ ( ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) → ( ordTop ‘ ≤ ) = ( TopOpen ‘ ℝ*𝑠 ) )
5	1 4	ax-mp	⊢ ( ordTop ‘ ≤ ) = ( TopOpen ‘ ℝ*𝑠 )