Metamath Proof Explorer


Theorem uniretop

Description: The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007)

Ref Expression
Assertion uniretop =topGenran.

Proof

Step Hyp Ref Expression
1 unirnioo =ran.
2 retopbas ran.TopBases
3 unitg ran.TopBasestopGenran.=ran.
4 2 3 ax-mp topGenran.=ran.
5 1 4 eqtr4i =topGenran.