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 ⊢ φ → J ∈ Top
iscnrm3rlem4.2 ⊢ φ → S ⊆ ⋃ J
iscnrm3rlem5.3 ⊢ φ → T ⊆ ⋃ J
iscnrm3rlem7.4 ⊢ φ → O ∈ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
Assertion iscnrm3rlem7 ⊢ φ → O ∈ J

Proof

Step Hyp Ref Expression
1 iscnrm3rlem4.1 ⊢ φ → J ∈ Top
2 iscnrm3rlem4.2 ⊢ φ → S ⊆ ⋃ J
3 iscnrm3rlem5.3 ⊢ φ → T ⊆ ⋃ J
4 iscnrm3rlem7.4 ⊢ φ → O ∈ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
5 1 uniexd ⊢ φ → ⋃ J ∈ V
6 5 difexd ⊢ φ → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ V
7 resttop ⊢ J ∈ Top ∧ ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ V → J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ Top
8 1 6 7 syl2anc ⊢ φ → J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ Top
9 eqid ⊢ ⋃ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T = ⋃ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
10 9 eltopss ⊢ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ∈ Top ∧ O ∈ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T → O ⊆ ⋃ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
11 8 4 10 syl2anc ⊢ φ → O ⊆ ⋃ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
12 difssd ⊢ φ → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ⊆ ⋃ J
13 eqid ⊢ ⋃ J = ⋃ J
14 13 restuni ⊢ J ∈ Top ∧ ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ⊆ ⋃ J → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T = ⋃ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
15 1 12 14 syl2anc ⊢ φ → ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T = ⋃ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
16 11 15 sseqtrrd ⊢ φ → O ⊆ ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T
17 1 2 3 16 iscnrm3rlem6 ⊢ φ → O ∈ J ↾ 𝑡 ⋃ J ∖ cls ⁡ J ⁡ S ∩ cls ⁡ J ⁡ T ↔ O ∈ J
18 4 17 mpbid ⊢ φ → O ∈ J