Metamath Proof Explorer

Theorem iscnrm3llem2

Description: Lemma for iscnrm3l . If there exist disjoint open neighborhoods in the original topology for two disjoint closed sets in a subspace, then they can be separated by open neighborhoods in the subspace topology. (Could shorten proof with ssin0 .) (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Assertion iscnrm3llem2 ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑍 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑍 ) ( 𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) )

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 ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝐽 ∈ Top )
10 simp121 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑍 ∈ 𝒫 ∪ 𝐽 )
11 simp2l ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑛 ∈ 𝐽 )
12 elrestr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → ( 𝑛 ∩ 𝑍 ) ∈ ( 𝐽 ↾t 𝑍 ) )
13 9 10 11 12 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( 𝑛 ∩ 𝑍 ) ∈ ( 𝐽 ↾t 𝑍 ) )
14 simp2r ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑚 ∈ 𝐽 )
15 elrestr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝑚 ∈ 𝐽 ) → ( 𝑚 ∩ 𝑍 ) ∈ ( 𝐽 ↾t 𝑍 ) )
16 9 10 14 15 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( 𝑚 ∩ 𝑍 ) ∈ ( 𝐽 ↾t 𝑍 ) )
17 simp31 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝐶 ⊆ 𝑛 )
18 eqidd ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ∪ 𝐽 = ∪ 𝐽 )
19 10 elpwid ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑍 ⊆ ∪ 𝐽 )
20 eqidd ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( 𝐽 ↾t 𝑍 ) = ( 𝐽 ↾t 𝑍 ) )
21 simp122 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) )
22 9 18 19 20 21 restcls2lem ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝐶 ⊆ 𝑍 )
23 17 22 ssind ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝐶 ⊆ ( 𝑛 ∩ 𝑍 ) )
24 simp32 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝐷 ⊆ 𝑚 )
25 simp123 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) )
26 9 18 19 20 25 restcls2lem ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝐷 ⊆ 𝑍 )
27 24 26 ssind ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝐷 ⊆ ( 𝑚 ∩ 𝑍 ) )
28 inss1 ⊢ ( 𝑛 ∩ 𝑍 ) ⊆ 𝑛
29 inss1 ⊢ ( 𝑚 ∩ 𝑍 ) ⊆ 𝑚
30 ss2in ⊢ ( ( ( 𝑛 ∩ 𝑍 ) ⊆ 𝑛 ∧ ( 𝑚 ∩ 𝑍 ) ⊆ 𝑚 ) → ( ( 𝑛 ∩ 𝑍 ) ∩ ( 𝑚 ∩ 𝑍 ) ) ⊆ ( 𝑛 ∩ 𝑚 ) )
31 28 29 30 mp2an ⊢ ( ( 𝑛 ∩ 𝑍 ) ∩ ( 𝑚 ∩ 𝑍 ) ) ⊆ ( 𝑛 ∩ 𝑚 )
32 simp33 ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( 𝑛 ∩ 𝑚 ) = ∅ )
33 31 32 sseqtrid ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( 𝑛 ∩ 𝑍 ) ∩ ( 𝑚 ∩ 𝑍 ) ) ⊆ ∅ )
34 ss0 ⊢ ( ( ( 𝑛 ∩ 𝑍 ) ∩ ( 𝑚 ∩ 𝑍 ) ) ⊆ ∅ → ( ( 𝑛 ∩ 𝑍 ) ∩ ( 𝑚 ∩ 𝑍 ) ) = ∅ )
35 33 34 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( 𝑛 ∩ 𝑍 ) ∩ ( 𝑚 ∩ 𝑍 ) ) = ∅ )
36 23 27 35 3jca ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( 𝐶 ⊆ ( 𝑛 ∩ 𝑍 ) ∧ 𝐷 ⊆ ( 𝑚 ∩ 𝑍 ) ∧ ( ( 𝑛 ∩ 𝑍 ) ∩ ( 𝑚 ∩ 𝑍 ) ) = ∅ ) )
37 13 16 36 3jca ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( 𝑛 ∩ 𝑍 ) ∈ ( 𝐽 ↾t 𝑍 ) ∧ ( 𝑚 ∩ 𝑍 ) ∈ ( 𝐽 ↾t 𝑍 ) ∧ ( 𝐶 ⊆ ( 𝑛 ∩ 𝑍 ) ∧ 𝐷 ⊆ ( 𝑚 ∩ 𝑍 ) ∧ ( ( 𝑛 ∩ 𝑍 ) ∩ ( 𝑚 ∩ 𝑍 ) ) = ∅ ) ) )
38 4 8 37 iscnrm3lem7 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ∧ 𝐷 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑍 ) ) ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑍 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑍 ) ( 𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) )