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 ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ 𝑘 ∧ ( 𝑙𝑘 ) = ∅ ) → ∃ 𝑛𝐽𝑚𝐽 ( 𝑆𝑛𝑇𝑚 ∧ ( 𝑛𝑚 ) = ∅ ) ) )