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