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

Metamath Proof Explorer

Theorem nrmtop

Description: A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion nrmtop ⊢ J ∈ Nrm → J ∈ Top

Proof

Step Hyp Ref Expression
1 isnrm ⊢ J ∈ Nrm ↔ J ∈ Top ∧ ∀ x ∈ J ∀ y ∈ Clsd ⁡ J ∩ 𝒫 x ∃ z ∈ J y ⊆ z ∧ cls ⁡ J ⁡ z ⊆ x
2 1 simplbi ⊢ J ∈ Nrm → J ∈ Top