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 
|- ( ph -> J e. Top )
seposep.2 
|- ( ph -> E. n e. J E. m e. J ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) )
Assertion seposep 
|- ( ph -> ( ( S C_ U. J /\ T C_ U. J ) /\ ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) ) )

Proof

Step Hyp Ref Expression
1 sepdisj.1 
 |-  ( ph -> J e. Top )
2 seposep.2 
 |-  ( ph -> E. n e. J E. m e. J ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) )
3 simp31 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> S C_ n )
4 simp1 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> J e. Top )
5 simp2l 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> n e. J )
6 eqid 
 |-  U. J = U. J
7 6 eltopss 
 |-  ( ( J e. Top /\ n e. J ) -> n C_ U. J )
8 4 5 7 syl2anc 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> n C_ U. J )
9 3 8 sstrd 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> S C_ U. J )
10 simp32 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> T C_ m )
11 simp2r 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> m e. J )
12 6 eltopss 
 |-  ( ( J e. Top /\ m e. J ) -> m C_ U. J )
13 4 11 12 syl2anc 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> m C_ U. J )
14 10 13 sstrd 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> T C_ U. J )
15 6 opncld 
 |-  ( ( J e. Top /\ n e. J ) -> ( U. J \ n ) e. ( Clsd ` J ) )
16 4 5 15 syl2anc 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( U. J \ n ) e. ( Clsd ` J ) )
17 incom 
 |-  ( n i^i m ) = ( m i^i n )
18 simp33 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( n i^i m ) = (/) )
19 17 18 eqtr3id 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( m i^i n ) = (/) )
20 reldisj 
 |-  ( m C_ U. J -> ( ( m i^i n ) = (/) <-> m C_ ( U. J \ n ) ) )
21 20 biimpd 
 |-  ( m C_ U. J -> ( ( m i^i n ) = (/) -> m C_ ( U. J \ n ) ) )
22 13 19 21 sylc 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> m C_ ( U. J \ n ) )
23 10 22 sstrd 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> T C_ ( U. J \ n ) )
24 6 clsss2 
 |-  ( ( ( U. J \ n ) e. ( Clsd ` J ) /\ T C_ ( U. J \ n ) ) -> ( ( cls ` J ) ` T ) C_ ( U. J \ n ) )
25 16 23 24 syl2anc 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( cls ` J ) ` T ) C_ ( U. J \ n ) )
26 3 sscond 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( U. J \ n ) C_ ( U. J \ S ) )
27 25 26 sstrd 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( cls ` J ) ` T ) C_ ( U. J \ S ) )
28 disjdif 
 |-  ( S i^i ( U. J \ S ) ) = (/)
29 28 a1i 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( S i^i ( U. J \ S ) ) = (/) )
30 27 29 ssdisjdr 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( S i^i ( ( cls ` J ) ` T ) ) = (/) )
31 6 opncld 
 |-  ( ( J e. Top /\ m e. J ) -> ( U. J \ m ) e. ( Clsd ` J ) )
32 4 11 31 syl2anc 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( U. J \ m ) e. ( Clsd ` J ) )
33 reldisj 
 |-  ( n C_ U. J -> ( ( n i^i m ) = (/) <-> n C_ ( U. J \ m ) ) )
34 33 biimpd 
 |-  ( n C_ U. J -> ( ( n i^i m ) = (/) -> n C_ ( U. J \ m ) ) )
35 8 18 34 sylc 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> n C_ ( U. J \ m ) )
36 3 35 sstrd 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> S C_ ( U. J \ m ) )
37 6 clsss2 
 |-  ( ( ( U. J \ m ) e. ( Clsd ` J ) /\ S C_ ( U. J \ m ) ) -> ( ( cls ` J ) ` S ) C_ ( U. J \ m ) )
38 32 36 37 syl2anc 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( cls ` J ) ` S ) C_ ( U. J \ m ) )
39 10 sscond 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( U. J \ m ) C_ ( U. J \ T ) )
40 38 39 sstrd 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( cls ` J ) ` S ) C_ ( U. J \ T ) )
41 disjdifr 
 |-  ( ( U. J \ T ) i^i T ) = (/)
42 41 a1i 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( U. J \ T ) i^i T ) = (/) )
43 40 42 ssdisjd 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( ( cls ` J ) ` S ) i^i T ) = (/) )
44 30 43 jca 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) )
45 9 14 44 jca31 
 |-  ( ( J e. Top /\ ( n e. J /\ m e. J ) /\ ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) -> ( ( S C_ U. J /\ T C_ U. J ) /\ ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) ) )
46 45 3exp 
 |-  ( J e. Top -> ( ( n e. J /\ m e. J ) -> ( ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) -> ( ( S C_ U. J /\ T C_ U. J ) /\ ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) ) ) ) )
47 46 rexlimdvv 
 |-  ( J e. Top -> ( E. n e. J E. m e. J ( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) -> ( ( S C_ U. J /\ T C_ U. J ) /\ ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) ) ) )
48 1 2 47 sylc 
 |-  ( ph -> ( ( S C_ U. J /\ T C_ U. J ) /\ ( ( S i^i ( ( cls ` J ) ` T ) ) = (/) /\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) ) )