This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )