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 )