Metamath Proof Explorer


Theorem xmetutop

Description: The topology induced by a uniform structure generated by an extended metric D is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion xmetutop X D ∞Met X unifTop metUnif D = MetOpen D

Proof

Step Hyp Ref Expression
1 xmetpsmet D ∞Met X D PsMet X
2 psmetutop X D PsMet X unifTop metUnif D = topGen ran ball D
3 1 2 sylan2 X D ∞Met X unifTop metUnif D = topGen ran ball D
4 eqid MetOpen D = MetOpen D
5 4 mopnval D ∞Met X MetOpen D = topGen ran ball D
6 5 adantl X D ∞Met X MetOpen D = topGen ran ball D
7 3 6 eqtr4d X D ∞Met X unifTop metUnif D = MetOpen D