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

Metamath Proof Explorer

Theorem tmstopn

Description: The topology of a constructed metric. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tmsbas.k ⊢ K = toMetSp ⁡ D
tmstopn.j ⊢ J = MetOpen ⁡ D
Assertion tmstopn ⊢ D ∈ ∞Met ⁡ X → J = TopOpen ⁡ K

Proof

Step Hyp Ref Expression
1 tmsbas.k ⊢ K = toMetSp ⁡ D
2 tmstopn.j ⊢ J = MetOpen ⁡ D
3 eqid ⊢ Base ndx X dist ⁡ ndx D = Base ndx X dist ⁡ ndx D
4 3 1 tmslem ⊢ D ∈ ∞Met ⁡ X → X = Base K ∧ D = dist ⁡ K ∧ MetOpen ⁡ D = TopOpen ⁡ K
5 4 simp3d ⊢ D ∈ ∞Met ⁡ X → MetOpen ⁡ D = TopOpen ⁡ K
6 2 5 eqtrid ⊢ D ∈ ∞Met ⁡ X → J = TopOpen ⁡ K