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 ( ( 𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ CNrm )

Proof

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