Metamath Proof Explorer

Theorem cnrmnrm

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

Ref Expression
Assertion cnrmnrm 
|- ( J e. CNrm -> J e. Nrm )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 restid 
 |-  ( J e. CNrm -> ( J |`t U. J ) = J )
3 uniexg 
 |-  ( J e. CNrm -> U. J e. _V )
4 cnrmi 
 |-  ( ( J e. CNrm /\ U. J e. _V ) -> ( J |`t U. J ) e. Nrm )
5 3 4 mpdan 
 |-  ( J e. CNrm -> ( J |`t U. J ) e. Nrm )
6 2 5 eqeltrrd 
 |-  ( J e. CNrm -> J e. Nrm )