Theorem xrstset

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

	Ref	Expression
Assertion	xrstset	⊢ ( ordTop ‘ ≤ ) = ( TopSet ‘ ℝ*𝑠 )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( ordTop ‘ ≤ ) ∈ V
2		df-xrs	⊢ ℝ*𝑠 = ( { ⟨ ( Base ‘ ndx ) , ℝ* ⟩ , ⟨ ( +g ‘ ndx ) , +𝑒 ⟩ , ⟨ ( .r ‘ ndx ) , ·e ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) ⟩ } )
3	2	odrngtset	⊢ ( ( ordTop ‘ ≤ ) ∈ V → ( ordTop ‘ ≤ ) = ( TopSet ‘ ℝ*𝑠 ) )
4	1 3	ax-mp	⊢ ( ordTop ‘ ≤ ) = ( TopSet ‘ ℝ*𝑠 )