Metamath Proof Explorer

Theorem xmstopn

Description: The topology component of an extended metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses isms.j J = TopOpen K
isms.x X = Base K
isms.d D = dist K X × X
Assertion xmstopn K ∞MetSp J = MetOpen D


Step Hyp Ref Expression
1 isms.j J = TopOpen K
2 isms.x X = Base K
3 isms.d D = dist K X × X
4 1 2 3 isxms K ∞MetSp K TopSp J = MetOpen D
5 4 simprbi K ∞MetSp J = MetOpen D