This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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