Theorem pnrmnrm

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

	Ref	Expression
Assertion	pnrmnrm	⊢ ( 𝐽 ∈ PNrm → 𝐽 ∈ Nrm )

Proof

Step	Hyp	Ref	Expression
1		ispnrm	⊢ ( 𝐽 ∈ PNrm ↔ ( 𝐽 ∈ Nrm ∧ ( Clsd ‘ 𝐽 ) ⊆ ran ( 𝑥 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑥 ) ) )
2	1	simplbi	⊢ ( 𝐽 ∈ PNrm → 𝐽 ∈ Nrm )