Metamath Proof Explorer

Theorem xrstps

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

Ref Expression
Assertion xrstps 
|- RR*s e. TopSp

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 tsettps 
 |-  ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) -> RR*s e. TopSp )
5 1 4 ax-mp 
 |-  RR*s e. TopSp