Metamath Proof Explorer

Theorem nrmtop

Description: A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion nrmtop 
|- ( J e. Nrm -> J e. Top )

Proof

Step Hyp Ref Expression
1 isnrm 
 |-  ( J e. Nrm <-> ( J e. Top /\ A. x e. J A. y e. ( ( Clsd ` J ) i^i ~P x ) E. z e. J ( y C_ z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
2 1 simplbi 
 |-  ( J e. Nrm -> J e. Top )