Metamath Proof Explorer

Theorem cnrmtop

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

Ref Expression
Assertion cnrmtop 
|- ( J e. CNrm -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 iscnrm 
 |-  ( J e. CNrm <-> ( J e. Top /\ A. x e. ~P U. J ( J |`t x ) e. Nrm ) )
3 2 simplbi 
 |-  ( J e. CNrm -> J e. Top )