Theorem cnrmtop

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

	Ref	Expression
Assertion	cnrmtop	⊢ ( 𝐽 ∈ CNrm → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	iscnrm	⊢ ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) )
3	2	simplbi	⊢ ( 𝐽 ∈ CNrm → 𝐽 ∈ Top )