Step |
Hyp |
Ref |
Expression |
1 |
|
sepdisj.1 |
⊢ ( 𝜑 → 𝐽 ∈ Top ) |
2 |
|
seposep.2 |
⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) |
3 |
|
simp31 |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑆 ⊆ 𝑛 ) |
4 |
|
simp1 |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝐽 ∈ Top ) |
5 |
|
simp2l |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑛 ∈ 𝐽 ) |
6 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
7 |
6
|
eltopss |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑛 ∈ 𝐽 ) → 𝑛 ⊆ ∪ 𝐽 ) |
8 |
4 5 7
|
syl2anc |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑛 ⊆ ∪ 𝐽 ) |
9 |
3 8
|
sstrd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑆 ⊆ ∪ 𝐽 ) |
10 |
|
simp32 |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑇 ⊆ 𝑚 ) |
11 |
|
simp2r |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑚 ∈ 𝐽 ) |
12 |
6
|
eltopss |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ) → 𝑚 ⊆ ∪ 𝐽 ) |
13 |
4 11 12
|
syl2anc |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑚 ⊆ ∪ 𝐽 ) |
14 |
10 13
|
sstrd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑇 ⊆ ∪ 𝐽 ) |
15 |
6
|
opncld |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑛 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑛 ) ∈ ( Clsd ‘ 𝐽 ) ) |
16 |
4 5 15
|
syl2anc |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ∪ 𝐽 ∖ 𝑛 ) ∈ ( Clsd ‘ 𝐽 ) ) |
17 |
|
incom |
⊢ ( 𝑛 ∩ 𝑚 ) = ( 𝑚 ∩ 𝑛 ) |
18 |
|
simp33 |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( 𝑛 ∩ 𝑚 ) = ∅ ) |
19 |
17 18
|
eqtr3id |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( 𝑚 ∩ 𝑛 ) = ∅ ) |
20 |
|
reldisj |
⊢ ( 𝑚 ⊆ ∪ 𝐽 → ( ( 𝑚 ∩ 𝑛 ) = ∅ ↔ 𝑚 ⊆ ( ∪ 𝐽 ∖ 𝑛 ) ) ) |
21 |
20
|
biimpd |
⊢ ( 𝑚 ⊆ ∪ 𝐽 → ( ( 𝑚 ∩ 𝑛 ) = ∅ → 𝑚 ⊆ ( ∪ 𝐽 ∖ 𝑛 ) ) ) |
22 |
13 19 21
|
sylc |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑚 ⊆ ( ∪ 𝐽 ∖ 𝑛 ) ) |
23 |
10 22
|
sstrd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑇 ⊆ ( ∪ 𝐽 ∖ 𝑛 ) ) |
24 |
6
|
clsss2 |
⊢ ( ( ( ∪ 𝐽 ∖ 𝑛 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑇 ⊆ ( ∪ 𝐽 ∖ 𝑛 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ⊆ ( ∪ 𝐽 ∖ 𝑛 ) ) |
25 |
16 23 24
|
syl2anc |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ⊆ ( ∪ 𝐽 ∖ 𝑛 ) ) |
26 |
3
|
sscond |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ∪ 𝐽 ∖ 𝑛 ) ⊆ ( ∪ 𝐽 ∖ 𝑆 ) ) |
27 |
25 26
|
sstrd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ⊆ ( ∪ 𝐽 ∖ 𝑆 ) ) |
28 |
|
disjdif |
⊢ ( 𝑆 ∩ ( ∪ 𝐽 ∖ 𝑆 ) ) = ∅ |
29 |
28
|
a1i |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( 𝑆 ∩ ( ∪ 𝐽 ∖ 𝑆 ) ) = ∅ ) |
30 |
27 29
|
ssdisjdr |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ) |
31 |
6
|
opncld |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑚 ) ∈ ( Clsd ‘ 𝐽 ) ) |
32 |
4 11 31
|
syl2anc |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ∪ 𝐽 ∖ 𝑚 ) ∈ ( Clsd ‘ 𝐽 ) ) |
33 |
|
reldisj |
⊢ ( 𝑛 ⊆ ∪ 𝐽 → ( ( 𝑛 ∩ 𝑚 ) = ∅ ↔ 𝑛 ⊆ ( ∪ 𝐽 ∖ 𝑚 ) ) ) |
34 |
33
|
biimpd |
⊢ ( 𝑛 ⊆ ∪ 𝐽 → ( ( 𝑛 ∩ 𝑚 ) = ∅ → 𝑛 ⊆ ( ∪ 𝐽 ∖ 𝑚 ) ) ) |
35 |
8 18 34
|
sylc |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑛 ⊆ ( ∪ 𝐽 ∖ 𝑚 ) ) |
36 |
3 35
|
sstrd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → 𝑆 ⊆ ( ∪ 𝐽 ∖ 𝑚 ) ) |
37 |
6
|
clsss2 |
⊢ ( ( ( ∪ 𝐽 ∖ 𝑚 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ ( ∪ 𝐽 ∖ 𝑚 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ∪ 𝐽 ∖ 𝑚 ) ) |
38 |
32 36 37
|
syl2anc |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ∪ 𝐽 ∖ 𝑚 ) ) |
39 |
10
|
sscond |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ∪ 𝐽 ∖ 𝑚 ) ⊆ ( ∪ 𝐽 ∖ 𝑇 ) ) |
40 |
38 39
|
sstrd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ∪ 𝐽 ∖ 𝑇 ) ) |
41 |
|
disjdifr |
⊢ ( ( ∪ 𝐽 ∖ 𝑇 ) ∩ 𝑇 ) = ∅ |
42 |
41
|
a1i |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( ∪ 𝐽 ∖ 𝑇 ) ∩ 𝑇 ) = ∅ ) |
43 |
40 42
|
ssdisjd |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) |
44 |
30 43
|
jca |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) |
45 |
9 14 44
|
jca31 |
⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( 𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ) |
46 |
45
|
3exp |
⊢ ( 𝐽 ∈ Top → ( ( 𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽 ) → ( ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) → ( ( 𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ) ) ) |
47 |
46
|
rexlimdvv |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) → ( ( 𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ) ) |
48 |
1 2 47
|
sylc |
⊢ ( 𝜑 → ( ( 𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) ) |