Metamath Proof Explorer

Theorem iscnrm3rlem8

Description: Lemma for iscnrm3r . Disjoint open neighborhoods in the subspace topology are disjoint open neighborhoods in the original topology given that the subspace is an open set in the original topology. Therefore, given any two sets separated in the original topology and separated by open neighborhoods in the subspace topology, they must be separated by open neighborhoods in the original topology. (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Assertion iscnrm3rlem8 ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) → ( ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 sseq2 ⊢ ( 𝑛 = 𝑙 → ( 𝑆 ⊆ 𝑛 ↔ 𝑆 ⊆ 𝑙 ) )
2 ineq1 ⊢ ( 𝑛 = 𝑙 → ( 𝑛 ∩ 𝑚 ) = ( 𝑙 ∩ 𝑚 ) )
3 2 eqeq1d ⊢ ( 𝑛 = 𝑙 → ( ( 𝑛 ∩ 𝑚 ) = ∅ ↔ ( 𝑙 ∩ 𝑚 ) = ∅ ) )
4 1 3 3anbi13d ⊢ ( 𝑛 = 𝑙 → ( ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ( 𝑆 ⊆ 𝑙 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑙 ∩ 𝑚 ) = ∅ ) ) )
5 sseq2 ⊢ ( 𝑚 = 𝑘 → ( 𝑇 ⊆ 𝑚 ↔ 𝑇 ⊆ 𝑘 ) )
6 ineq2 ⊢ ( 𝑚 = 𝑘 → ( 𝑙 ∩ 𝑚 ) = ( 𝑙 ∩ 𝑘 ) )
7 6 eqeq1d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑙 ∩ 𝑚 ) = ∅ ↔ ( 𝑙 ∩ 𝑘 ) = ∅ ) )
8 5 7 3anbi23d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑆 ⊆ 𝑙 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑙 ∩ 𝑚 ) = ∅ ) ↔ ( 𝑆 ⊆ 𝑙 ∧ 𝑇 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) )
9 simp11 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝐽 ∈ Top )
10 simp12l ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝑆 ∈ 𝒫 ∪ 𝐽 )
11 10 elpwid ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝑆 ⊆ ∪ 𝐽 )
12 simp12r ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝑇 ∈ 𝒫 ∪ 𝐽 )
13 12 elpwid ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝑇 ⊆ ∪ 𝐽 )
14 simp2l ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) )
15 9 11 13 14 iscnrm3rlem7 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝑙 ∈ 𝐽 )
16 simp2r ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) )
17 9 11 13 16 iscnrm3rlem7 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝑘 ∈ 𝐽 )
18 simp13l ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ )
19 simp31 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 )
20 9 11 18 19 iscnrm3rlem4 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝑆 ⊆ 𝑙 )
21 incom ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ( 𝑇 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
22 simp13r ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ )
23 21 22 eqtr3id ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( 𝑇 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ∅ )
24 simp32 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 )
25 9 13 23 24 iscnrm3rlem4 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → 𝑇 ⊆ 𝑘 )
26 simp33 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( 𝑙 ∩ 𝑘 ) = ∅ )
27 20 25 26 3jca ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( 𝑆 ⊆ 𝑙 ∧ 𝑇 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) )
28 15 17 27 3jca ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ∧ ( 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∧ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( 𝑙 ∈ 𝐽 ∧ 𝑘 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑙 ∧ 𝑇 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) )
29 4 8 28 iscnrm3lem7 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) → ( ∃ 𝑙 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ∃ 𝑘 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ⊆ 𝑙 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )