Metamath Proof Explorer

Theorem iscnrm3rlem3

Description: Lemma for iscnrm3r . The designed subspace is a subset of the original set; the two sets are closed sets in the subspace. (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Assertion iscnrm3rlem3 ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ 𝒫 ⋃ J ∧ cls ⁡ J ⁡ S ∖ cls ⁡ J ⁡ T ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∧ cls ⁡ J ⁡ T ∖ cls ⁡ J ⁡ S ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T

Proof

Step Hyp Ref Expression
1 uniexg ⊢ J ∈ Top → ⋃ J ∈ V
2 difssd ⊢ J ∈ Top → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ⊆ ⋃ J
3 1 2 sselpwd ⊢ J ∈ Top → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ 𝒫 ⋃ J
4 3 adantr ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ 𝒫 ⋃ J
5 simpl ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → J ∈ Top
6 simprl ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → S ∈ 𝒫 ⋃ J
7 6 elpwid ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → S ⊆ ⋃ J
8 5 7 iscnrm3rlem2 ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → cls ⁡ J ⁡ S ∖ cls ⁡ J ⁡ T ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
9 simprr ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → T ∈ 𝒫 ⋃ J
10 9 elpwid ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → T ⊆ ⋃ J
11 5 10 iscnrm3rlem2 ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → cls ⁡ J ⁡ T ∖ cls ⁡ J ⁡ S ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ T ∩ cls ⁡ J ⁡ S
12 incom ⊢ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T = cls ⁡ J ⁡ T ∩ cls ⁡ J ⁡ S
13 12 difeq2i ⊢ ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T = ⋃ J ∖ cls ⁡ J ⁡ T ∩ cls ⁡ J ⁡ S
14 13 oveq2i ⊢ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T = J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ T ∩ cls ⁡ J ⁡ S
15 14 fveq2i ⊢ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T = Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ T ∩ cls ⁡ J ⁡ S
16 11 15 eleqtrrdi ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → cls ⁡ J ⁡ T ∖ cls ⁡ J ⁡ S ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
17 4 8 16 3jca ⊢ J ∈ Top ∧ S ∈ 𝒫 ⋃ J ∧ T ∈ 𝒫 ⋃ J → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ 𝒫 ⋃ J ∧ cls ⁡ J ⁡ S ∖ cls ⁡ J ⁡ T ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∧ cls ⁡ J ⁡ T ∖ cls ⁡ J ⁡ S ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T