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 ⊢ J ∈ CNrm ∧ A ∈ V → J ↾ 𝑡 A ∈ Nrm

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 restin ⊢ J ∈ CNrm ∧ A ∈ V → J ↾ 𝑡 A = J ↾ 𝑡 A ∩ ⋃ J
3 oveq2 ⊢ x = A ∩ ⋃ J → J ↾ 𝑡 x = J ↾ 𝑡 A ∩ ⋃ J
4 3 eleq1d ⊢ x = A ∩ ⋃ J → J ↾ 𝑡 x ∈ Nrm ↔ J ↾ 𝑡 A ∩ ⋃ J ∈ Nrm
5 1 iscnrm ⊢ J ∈ CNrm ↔ J ∈ Top ∧ ∀ x ∈ 𝒫 ⋃ J J ↾ 𝑡 x ∈ Nrm
6 5 simprbi ⊢ J ∈ CNrm → ∀ x ∈ 𝒫 ⋃ J J ↾ 𝑡 x ∈ Nrm
7 6 adantr ⊢ J ∈ CNrm ∧ A ∈ V → ∀ x ∈ 𝒫 ⋃ J J ↾ 𝑡 x ∈ Nrm
8 inss2 ⊢ A ∩ ⋃ J ⊆ ⋃ J
9 inex1g ⊢ A ∈ V → A ∩ ⋃ J ∈ V
10 elpwg ⊢ A ∩ ⋃ J ∈ V → A ∩ ⋃ J ∈ 𝒫 ⋃ J ↔ A ∩ ⋃ J ⊆ ⋃ J
11 9 10 syl ⊢ A ∈ V → A ∩ ⋃ J ∈ 𝒫 ⋃ J ↔ A ∩ ⋃ J ⊆ ⋃ J
12 8 11 mpbiri ⊢ A ∈ V → A ∩ ⋃ J ∈ 𝒫 ⋃ J
13 12 adantl ⊢ J ∈ CNrm ∧ A ∈ V → A ∩ ⋃ J ∈ 𝒫 ⋃ J
14 4 7 13 rspcdva ⊢ J ∈ CNrm ∧ A ∈ V → J ↾ 𝑡 A ∩ ⋃ J ∈ Nrm
15 2 14 eqeltrd ⊢ J ∈ CNrm ∧ A ∈ V → J ↾ 𝑡 A ∈ Nrm