Metamath Proof Explorer

Theorem xrge0tps

Description: The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017)

Ref Expression
Assertion xrge0tps 
|- ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp

Proof

Step Hyp Ref Expression
1 xrstps 
 |-  RR*s e. TopSp
2 ovex 
 |-  ( 0 [,] +oo ) e. _V
3 resstps 
 |-  ( ( RR*s e. TopSp /\ ( 0 [,] +oo ) e. _V ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp )
4 1 2 3 mp2an 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp