Metamath Proof Explorer

Theorem pnrmnrm

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

Ref Expression
Assertion pnrmnrm 
|- ( J e. PNrm -> J e. Nrm )

Proof

Step Hyp Ref Expression
1 ispnrm 
 |-  ( J e. PNrm <-> ( J e. Nrm /\ ( Clsd ` J ) C_ ran ( x e. ( J ^m NN ) |-> |^| ran x ) ) )
2 1 simplbi 
 |-  ( J e. PNrm -> J e. Nrm )