Metamath Proof Explorer

Theorem restcnrm

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

Ref Expression
Assertion restcnrm ⊢ J ∈ CNrm ∧ A ∈ V → J ↾ 𝑡 A ∈ CNrm

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 restin ⊢ J ∈ CNrm ∧ A ∈ V → J ↾ 𝑡 A = J ↾ 𝑡 A ∩ ⋃ J
3 simpll ⊢ J ∈ CNrm ∧ A ∈ V ∧ x ∈ 𝒫 A ∩ ⋃ J → J ∈ CNrm
4 elpwi ⊢ x ∈ 𝒫 A ∩ ⋃ J → x ⊆ A ∩ ⋃ J
5 4 adantl ⊢ J ∈ CNrm ∧ A ∈ V ∧ x ∈ 𝒫 A ∩ ⋃ J → x ⊆ A ∩ ⋃ J
6 inex1g ⊢ A ∈ V → A ∩ ⋃ J ∈ V
7 6 ad2antlr ⊢ J ∈ CNrm ∧ A ∈ V ∧ x ∈ 𝒫 A ∩ ⋃ J → A ∩ ⋃ J ∈ V
8 restabs ⊢ J ∈ CNrm ∧ x ⊆ A ∩ ⋃ J ∧ A ∩ ⋃ J ∈ V → J ↾ 𝑡 A ∩ ⋃ J ↾ 𝑡 x = J ↾ 𝑡 x
9 3 5 7 8 syl3anc ⊢ J ∈ CNrm ∧ A ∈ V ∧ x ∈ 𝒫 A ∩ ⋃ J → J ↾ 𝑡 A ∩ ⋃ J ↾ 𝑡 x = J ↾ 𝑡 x
10 cnrmi ⊢ J ∈ CNrm ∧ x ∈ 𝒫 A ∩ ⋃ J → J ↾ 𝑡 x ∈ Nrm
11 10 adantlr ⊢ J ∈ CNrm ∧ A ∈ V ∧ x ∈ 𝒫 A ∩ ⋃ J → J ↾ 𝑡 x ∈ Nrm
12 9 11 eqeltrd ⊢ J ∈ CNrm ∧ A ∈ V ∧ x ∈ 𝒫 A ∩ ⋃ J → J ↾ 𝑡 A ∩ ⋃ J ↾ 𝑡 x ∈ Nrm
13 12 ralrimiva ⊢ J ∈ CNrm ∧ A ∈ V → ∀ x ∈ 𝒫 A ∩ ⋃ J J ↾ 𝑡 A ∩ ⋃ J ↾ 𝑡 x ∈ Nrm
14 cnrmtop ⊢ J ∈ CNrm → J ∈ Top
15 14 adantr ⊢ J ∈ CNrm ∧ A ∈ V → J ∈ Top
16 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
17 15 16 sylib ⊢ J ∈ CNrm ∧ A ∈ V → J ∈ TopOn ⁡ ⋃ J
18 inss2 ⊢ A ∩ ⋃ J ⊆ ⋃ J
19 resttopon ⊢ J ∈ TopOn ⁡ ⋃ J ∧ A ∩ ⋃ J ⊆ ⋃ J → J ↾ 𝑡 A ∩ ⋃ J ∈ TopOn ⁡ A ∩ ⋃ J
20 17 18 19 sylancl ⊢ J ∈ CNrm ∧ A ∈ V → J ↾ 𝑡 A ∩ ⋃ J ∈ TopOn ⁡ A ∩ ⋃ J
21 iscnrm2 ⊢ J ↾ 𝑡 A ∩ ⋃ J ∈ TopOn ⁡ A ∩ ⋃ J → J ↾ 𝑡 A ∩ ⋃ J ∈ CNrm ↔ ∀ x ∈ 𝒫 A ∩ ⋃ J J ↾ 𝑡 A ∩ ⋃ J ↾ 𝑡 x ∈ Nrm
22 20 21 syl ⊢ J ∈ CNrm ∧ A ∈ V → J ↾ 𝑡 A ∩ ⋃ J ∈ CNrm ↔ ∀ x ∈ 𝒫 A ∩ ⋃ J J ↾ 𝑡 A ∩ ⋃ J ↾ 𝑡 x ∈ Nrm
23 13 22 mpbird ⊢ J ∈ CNrm ∧ A ∈ V → J ↾ 𝑡 A ∩ ⋃ J ∈ CNrm
24 2 23 eqeltrd ⊢ J ∈ CNrm ∧ A ∈ V → J ↾ 𝑡 A ∈ CNrm