Metamath Proof Explorer

Theorem iscnrm3rlem5

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

Ref Expression
Hypotheses iscnrm3rlem4.1 ⊢ φ → J ∈ Top
iscnrm3rlem4.2 ⊢ φ → S ⊆ ⋃ J
iscnrm3rlem5.3 ⊢ φ → T ⊆ ⋃ J
Assertion iscnrm3rlem5 ⊢ φ → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ J

Proof

Step Hyp Ref Expression
1 iscnrm3rlem4.1 ⊢ φ → J ∈ Top
2 iscnrm3rlem4.2 ⊢ φ → S ⊆ ⋃ J
3 iscnrm3rlem5.3 ⊢ φ → T ⊆ ⋃ J
4 eqid ⊢ ⋃ J = ⋃ J
5 4 clscld ⊢ J ∈ Top ∧ S ⊆ ⋃ J → cls ⁡ J ⁡ S ∈ Clsd ⁡ J
6 1 2 5 syl2anc ⊢ φ → cls ⁡ J ⁡ S ∈ Clsd ⁡ J
7 4 clscld ⊢ J ∈ Top ∧ T ⊆ ⋃ J → cls ⁡ J ⁡ T ∈ Clsd ⁡ J
8 1 3 7 syl2anc ⊢ φ → cls ⁡ J ⁡ T ∈ Clsd ⁡ J
9 incld ⊢ cls ⁡ J ⁡ S ∈ Clsd ⁡ J ∧ cls ⁡ J ⁡ T ∈ Clsd ⁡ J → cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ Clsd ⁡ J
10 6 8 9 syl2anc ⊢ φ → cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ Clsd ⁡ J
11 4 cldopn ⊢ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ Clsd ⁡ J → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ J
12 10 11 syl ⊢ φ → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ J