Metamath Proof Explorer

Theorem pnrmtop

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

Ref Expression
Assertion pnrmtop 
|- ( J e. PNrm -> J e. Top )

Proof

Step Hyp Ref Expression
1 pnrmnrm 
 |-  ( J e. PNrm -> J e. Nrm )
2 nrmtop 
 |-  ( J e. Nrm -> J e. Top )
3 1 2 syl 
 |-  ( J e. PNrm -> J e. Top )