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 𝑍 ) ( 𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) |