Metamath Proof Explorer


Theorem cnrmnrm

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

Ref Expression
Assertion cnrmnrm ( 𝐽 ∈ CNrm → 𝐽 ∈ Nrm )

Proof

Step Hyp Ref Expression
1 eqid 𝐽 = 𝐽
2 1 restid ( 𝐽 ∈ CNrm → ( 𝐽t 𝐽 ) = 𝐽 )
3 uniexg ( 𝐽 ∈ CNrm → 𝐽 ∈ V )
4 cnrmi ( ( 𝐽 ∈ CNrm ∧ 𝐽 ∈ V ) → ( 𝐽t 𝐽 ) ∈ Nrm )
5 3 4 mpdan ( 𝐽 ∈ CNrm → ( 𝐽t 𝐽 ) ∈ Nrm )
6 2 5 eqeltrrd ( 𝐽 ∈ CNrm → 𝐽 ∈ Nrm )