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