Metamath Proof Explorer


Theorem tmsds

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

Ref Expression
Hypothesis tmsbas.k K = toMetSp D
Assertion tmsds D ∞Met X D = dist K

Proof

Step Hyp Ref Expression
1 tmsbas.k K = toMetSp D
2 eqid Base ndx X dist ndx D = Base ndx X dist ndx D
3 2 1 tmslem D ∞Met X X = Base K D = dist K MetOpen D = TopOpen K
4 3 simp2d D ∞Met X D = dist K