Theorem cnrmi

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

	Ref	Expression
Assertion	cnrmi	⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Nrm )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	restin	⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝐴 ∩ ∪ 𝐽 ) ) )
3		oveq2	⊢ ( 𝑥 = ( 𝐴 ∩ ∪ 𝐽 ) → ( 𝐽 ↾t 𝑥 ) = ( 𝐽 ↾t ( 𝐴 ∩ ∪ 𝐽 ) ) )
4	3	eleq1d	⊢ ( 𝑥 = ( 𝐴 ∩ ∪ 𝐽 ) → ( ( 𝐽 ↾t 𝑥 ) ∈ Nrm ↔ ( 𝐽 ↾t ( 𝐴 ∩ ∪ 𝐽 ) ) ∈ Nrm ) )
5	1	iscnrm	⊢ ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm ) )
6	5	simprbi	⊢ ( 𝐽 ∈ CNrm → ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm )
7	6	adantr	⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑥 ) ∈ Nrm )
8		inss2	⊢ ( 𝐴 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽
9		inex1g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ∪ 𝐽 ) ∈ V )
10		elpwg	⊢ ( ( 𝐴 ∩ ∪ 𝐽 ) ∈ V → ( ( 𝐴 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ↔ ( 𝐴 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) )
11	9 10	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ↔ ( 𝐴 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) )
12	8 11	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 )
13	12	adantl	⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 )
14	4 7 13	rspcdva	⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t ( 𝐴 ∩ ∪ 𝐽 ) ) ∈ Nrm )
15	2 14	eqeltrd	⊢ ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Nrm )