Metamath Proof Explorer

Theorem rrexttps

Description: An extension of RR is a topological space. (Contributed by Thierry Arnoux, 7-Sep-2018)

Ref Expression
Assertion rrexttps 
|- ( R e. RRExt -> R e. TopSp )

Proof

Step Hyp Ref Expression
1 rrextnrg 
 |-  ( R e. RRExt -> R e. NrmRing )
2 nrgngp 
 |-  ( R e. NrmRing -> R e. NrmGrp )
3 ngpxms 
 |-  ( R e. NrmGrp -> R e. *MetSp )
4 1 2 3 3syl 
 |-  ( R e. RRExt -> R e. *MetSp )
5 xmstps 
 |-  ( R e. *MetSp -> R e. TopSp )
6 4 5 syl 
 |-  ( R e. RRExt -> R e. TopSp )