Metamath Proof Explorer


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 )