Metamath Proof Explorer

Theorem seposep

Description: If two sets are separated by (open) neighborhoods, then they are separated subsets of the underlying set. Note that separatedness by open neighborhoods is equivalent to separatedness by neighborhoods. See sepnsepo . The relationship between separatedness and closure is also seen in isnrm , isnrm2 , isnrm3 . (Contributed by Zhi Wang, 7-Sep-2024)

Ref Expression
Hypotheses sepdisj.1 ⊢ ( 𝜑 → 𝐽 ∈ Top )
seposep.2 ⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )
Assertion seposep ( 𝜑 → ( ( 𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽 ) ∧ ( ( 𝑆 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) )

Proof

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 ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ ) ) )