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

Metamath Proof Explorer

Theorem xmstps

Description: An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion xmstps ⊢ M ∈ ∞MetSp → M ∈ TopSp

Proof

Step Hyp Ref Expression
1 eqid ⊢ TopOpen ⁡ M = TopOpen ⁡ M
2 eqid ⊢ Base M = Base M
3 eqid ⊢ dist ⁡ M ↾ Base M × Base M = dist ⁡ M ↾ Base M × Base M
4 1 2 3 isxms ⊢ M ∈ ∞MetSp ↔ M ∈ TopSp ∧ TopOpen ⁡ M = MetOpen ⁡ dist ⁡ M ↾ Base M × Base M
5 4 simplbi ⊢ M ∈ ∞MetSp → M ∈ TopSp