Metamath Proof Explorer

Theorem iscnrm3rlem6

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

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

Proof

Step Hyp Ref Expression
1 iscnrm3rlem4.1 ⊢ φ → J ∈ Top
2 iscnrm3rlem4.2 ⊢ φ → S ⊆ ⋃ J
3 iscnrm3rlem5.3 ⊢ φ → T ⊆ ⋃ J
4 iscnrm3rlem6.4 ⊢ φ → O ⊆ ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
5 1 2 3 iscnrm3rlem5 ⊢ φ → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ J
6 restopn2 ⊢ J ∈ Top ∧ ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ J → O ∈ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ↔ O ∈ J ∧ O ⊆ ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
7 1 5 6 syl2anc ⊢ φ → O ∈ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ↔ O ∈ J ∧ O ⊆ ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
8 4 7 mpbiran2d ⊢ φ → O ∈ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ↔ O ∈ J