Metamath Proof Explorer

Theorem iscnrm3rlem2

Description: Lemma for iscnrm3rlem3 . (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Hypotheses iscnrm3rlem2.1 ⊢ φ → J ∈ Top
iscnrm3rlem2.2 ⊢ φ → S ⊆ ⋃ J
Assertion iscnrm3rlem2 ⊢ φ → cls ⁡ J ⁡ S ∖ T ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ T

Proof

Step Hyp Ref Expression
1 iscnrm3rlem2.1 ⊢ φ → J ∈ Top
2 iscnrm3rlem2.2 ⊢ φ → S ⊆ ⋃ J
3 eqid ⊢ ⋃ J = ⋃ J
4 3 clscld ⊢ J ∈ Top ∧ S ⊆ ⋃ J → cls ⁡ J ⁡ S ∈ Clsd ⁡ J
5 3 clsss3 ⊢ J ∈ Top ∧ S ⊆ ⋃ J → cls ⁡ J ⁡ S ⊆ ⋃ J
6 5 iscnrm3rlem1 ⊢ J ∈ Top ∧ S ⊆ ⋃ J → cls ⁡ J ⁡ S ∖ T = cls ⁡ J ⁡ S ∩ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T
7 ineq1 ⊢ c = cls ⁡ J ⁡ S → c ∩ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T = cls ⁡ J ⁡ S ∩ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T
8 7 rspceeqv ⊢ cls ⁡ J ⁡ S ∈ Clsd ⁡ J ∧ cls ⁡ J ⁡ S ∖ T = cls ⁡ J ⁡ S ∩ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T → ∃ c ∈ Clsd ⁡ J cls ⁡ J ⁡ S ∖ T = c ∩ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T
9 4 6 8 syl2anc ⊢ J ∈ Top ∧ S ⊆ ⋃ J → ∃ c ∈ Clsd ⁡ J cls ⁡ J ⁡ S ∖ T = c ∩ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T
10 1 2 9 syl2anc ⊢ φ → ∃ c ∈ Clsd ⁡ J cls ⁡ J ⁡ S ∖ T = c ∩ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T
11 difss ⊢ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T ⊆ ⋃ J
12 3 restcld ⊢ J ∈ Top ∧ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T ⊆ ⋃ J → cls ⁡ J ⁡ S ∖ T ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ T ↔ ∃ c ∈ Clsd ⁡ J cls ⁡ J ⁡ S ∖ T = c ∩ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T
13 1 11 12 sylancl ⊢ φ → cls ⁡ J ⁡ S ∖ T ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ T ↔ ∃ c ∈ Clsd ⁡ J cls ⁡ J ⁡ S ∖ T = c ∩ ⋃ J ∖ cls ⁡ J ⁡ S ∩ T
14 10 13 mpbird ⊢ φ → cls ⁡ J ⁡ S ∖ T ∈ Clsd ⁡ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ T