Metamath Proof Explorer


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 ` RR*s )

Proof

Step Hyp Ref Expression
1 letopon
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
2 xrsbas
 |-  RR* = ( Base ` RR*s )
3 xrstset
 |-  ( ordTop ` <_ ) = ( TopSet ` RR*s )
4 2 3 topontopn
 |-  ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) -> ( ordTop ` <_ ) = ( TopOpen ` RR*s ) )
5 1 4 ax-mp
 |-  ( ordTop ` <_ ) = ( TopOpen ` RR*s )