Metamath Proof Explorer

Theorem cnrmtop

Description: A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion cnrmtop ⊢ J ∈ CNrm → J ∈ Top

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 iscnrm ⊢ J ∈ CNrm ↔ J ∈ Top ∧ ∀ x ∈ 𝒫 ⋃ J J ↾ 𝑡 x ∈ Nrm
3 2 simplbi ⊢ J ∈ CNrm → J ∈ Top