Description: A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | pnrmnrm | ⊢ ( 𝐽 ∈ PNrm → 𝐽 ∈ Nrm ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ispnrm | ⊢ ( 𝐽 ∈ PNrm ↔ ( 𝐽 ∈ Nrm ∧ ( Clsd ‘ 𝐽 ) ⊆ ran ( 𝑥 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑥 ) ) ) | |
2 | 1 | simplbi | ⊢ ( 𝐽 ∈ PNrm → 𝐽 ∈ Nrm ) |