Metamath Proof Explorer

Theorem iscnrm3rlem7

Description: Lemma for iscnrm3rlem8 . Open neighborhoods in the subspace topology are open neighborhoods in the original topology given that the subspace is an open set in the original topology. (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Hypotheses iscnrm3rlem4.1 ⊢ ( 𝜑 → 𝐽 ∈ Top )
iscnrm3rlem4.2 ⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
iscnrm3rlem5.3 ⊢ ( 𝜑 → 𝑇 ⊆ ∪ 𝐽 )
iscnrm3rlem7.4 ⊢ ( 𝜑 → 𝑂 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) )
Assertion iscnrm3rlem7 ( 𝜑 → 𝑂 ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 iscnrm3rlem4.1 ⊢ ( 𝜑 → 𝐽 ∈ Top )
2 iscnrm3rlem4.2 ⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
3 iscnrm3rlem5.3 ⊢ ( 𝜑 → 𝑇 ⊆ ∪ 𝐽 )
4 iscnrm3rlem7.4 ⊢ ( 𝜑 → 𝑂 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) )
5 1 uniexd ⊢ ( 𝜑 → ∪ 𝐽 ∈ V )
6 5 difexd ⊢ ( 𝜑 → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ V )
7 resttop ⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ V ) → ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∈ Top )
8 1 6 7 syl2anc ⊢ ( 𝜑 → ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∈ Top )
9 eqid ⊢ ∪ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) = ∪ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) )
10 9 eltopss ⊢ ( ( ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∈ Top ∧ 𝑂 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) → 𝑂 ⊆ ∪ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) )
11 8 4 10 syl2anc ⊢ ( 𝜑 → 𝑂 ⊆ ∪ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) )
12 difssd ⊢ ( 𝜑 → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ⊆ ∪ 𝐽 )
13 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
14 13 restuni ⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ⊆ ∪ 𝐽 ) → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) = ∪ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) )
15 1 12 14 syl2anc ⊢ ( 𝜑 → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) = ∪ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) )
16 11 15 sseqtrrd ⊢ ( 𝜑 → 𝑂 ⊆ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) )
17 1 2 3 16 iscnrm3rlem6 ⊢ ( 𝜑 → ( 𝑂 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ↔ 𝑂 ∈ 𝐽 ) )
18 4 17 mpbid ⊢ ( 𝜑 → 𝑂 ∈ 𝐽 )