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

Metamath Proof Explorer

Theorem mopntop

Description: The set of open sets of a metric space is a topology. (Contributed by NM, 28-Aug-2006) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopnval.1 ⊢ J = MetOpen ⁡ D
Assertion mopntop ⊢ D ∈ ∞Met ⁡ X → J ∈ Top

Proof

Step Hyp Ref Expression
1 mopnval.1 ⊢ J = MetOpen ⁡ D
2 1 mopntopon ⊢ D ∈ ∞Met ⁡ X → J ∈ TopOn ⁡ X
3 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
4 2 3 syl ⊢ D ∈ ∞Met ⁡ X → J ∈ Top