Theorem xrstps

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

	Ref	Expression
Assertion	xrstps	⊢ ℝ*𝑠 ∈ TopSp

Proof

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