Theorem pnrmnrm

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

	Ref	Expression
Assertion	pnrmnrm	$$⊢J\in \mathrm{PNrm}\to J\in \mathrm{Nrm}$$

Proof

Step	Hyp	Ref	Expression
1		ispnrm	$$⊢J\in \mathrm{PNrm}\leftrightarrow \left(J\in \mathrm{Nrm}\wedge \mathrm{Clsd}\left(J\right)\subseteq \mathrm{ran}\left(x\in \left(J^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}x\right)\right)$$
2	1	simplbi	$$⊢J\in \mathrm{PNrm}\to J\in \mathrm{Nrm}$$