Metamath Proof Explorer

Theorem sepfsepc

Description: If two sets are separated by a continuous function, then they are separated by closed neighborhoods. (Contributed by Zhi Wang, 9-Sep-2024)

Ref Expression
Hypothesis sepfsepc.1 
|- ( ph -> E. f e. ( J Cn II ) ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) )
Assertion sepfsepc 
|- ( ph -> E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) )

Proof

Step Hyp Ref Expression
1 sepfsepc.1 
 |-  ( ph -> E. f e. ( J Cn II ) ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) )
2 simpl 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> f e. ( J Cn II ) )
3 0re 
 |-  0 e. RR
4 1re 
 |-  1 e. RR
5 0le0 
 |-  0 <_ 0
6 3re 
 |-  3 e. RR
7 3ne0 
 |-  3 =/= 0
8 6 7 rereccli 
 |-  ( 1 / 3 ) e. RR
9 1lt3 
 |-  1 < 3
10 recgt1i 
 |-  ( ( 3 e. RR /\ 1 < 3 ) -> ( 0 < ( 1 / 3 ) /\ ( 1 / 3 ) < 1 ) )
11 6 9 10 mp2an 
 |-  ( 0 < ( 1 / 3 ) /\ ( 1 / 3 ) < 1 )
12 11 simpri 
 |-  ( 1 / 3 ) < 1
13 8 4 12 ltleii 
 |-  ( 1 / 3 ) <_ 1
14 iccss 
 |-  ( ( ( 0 e. RR /\ 1 e. RR ) /\ ( 0 <_ 0 /\ ( 1 / 3 ) <_ 1 ) ) -> ( 0 [,] ( 1 / 3 ) ) C_ ( 0 [,] 1 ) )
15 3 4 5 13 14 mp4an 
 |-  ( 0 [,] ( 1 / 3 ) ) C_ ( 0 [,] 1 )
16 i0oii 
 |-  ( ( 1 / 3 ) <_ 1 -> ( 0 [,) ( 1 / 3 ) ) e. II )
17 13 16 ax-mp 
 |-  ( 0 [,) ( 1 / 3 ) ) e. II
18 11 simpli 
 |-  0 < ( 1 / 3 )
19 8 rexri 
 |-  ( 1 / 3 ) e. RR*
20 elico2 
 |-  ( ( 0 e. RR /\ ( 1 / 3 ) e. RR* ) -> ( 0 e. ( 0 [,) ( 1 / 3 ) ) <-> ( 0 e. RR /\ 0 <_ 0 /\ 0 < ( 1 / 3 ) ) ) )
21 3 19 20 mp2an 
 |-  ( 0 e. ( 0 [,) ( 1 / 3 ) ) <-> ( 0 e. RR /\ 0 <_ 0 /\ 0 < ( 1 / 3 ) ) )
22 21 biimpri 
 |-  ( ( 0 e. RR /\ 0 <_ 0 /\ 0 < ( 1 / 3 ) ) -> 0 e. ( 0 [,) ( 1 / 3 ) ) )
23 22 snssd 
 |-  ( ( 0 e. RR /\ 0 <_ 0 /\ 0 < ( 1 / 3 ) ) -> { 0 } C_ ( 0 [,) ( 1 / 3 ) ) )
24 3 5 18 23 mp3an 
 |-  { 0 } C_ ( 0 [,) ( 1 / 3 ) )
25 icossicc 
 |-  ( 0 [,) ( 1 / 3 ) ) C_ ( 0 [,] ( 1 / 3 ) )
26 24 25 pm3.2i 
 |-  ( { 0 } C_ ( 0 [,) ( 1 / 3 ) ) /\ ( 0 [,) ( 1 / 3 ) ) C_ ( 0 [,] ( 1 / 3 ) ) )
27 sseq2 
 |-  ( g = ( 0 [,) ( 1 / 3 ) ) -> ( { 0 } C_ g <-> { 0 } C_ ( 0 [,) ( 1 / 3 ) ) ) )
28 sseq1 
 |-  ( g = ( 0 [,) ( 1 / 3 ) ) -> ( g C_ ( 0 [,] ( 1 / 3 ) ) <-> ( 0 [,) ( 1 / 3 ) ) C_ ( 0 [,] ( 1 / 3 ) ) ) )
29 27 28 anbi12d 
 |-  ( g = ( 0 [,) ( 1 / 3 ) ) -> ( ( { 0 } C_ g /\ g C_ ( 0 [,] ( 1 / 3 ) ) ) <-> ( { 0 } C_ ( 0 [,) ( 1 / 3 ) ) /\ ( 0 [,) ( 1 / 3 ) ) C_ ( 0 [,] ( 1 / 3 ) ) ) ) )
30 29 rspcev 
 |-  ( ( ( 0 [,) ( 1 / 3 ) ) e. II /\ ( { 0 } C_ ( 0 [,) ( 1 / 3 ) ) /\ ( 0 [,) ( 1 / 3 ) ) C_ ( 0 [,] ( 1 / 3 ) ) ) ) -> E. g e. II ( { 0 } C_ g /\ g C_ ( 0 [,] ( 1 / 3 ) ) ) )
31 17 26 30 mp2an 
 |-  E. g e. II ( { 0 } C_ g /\ g C_ ( 0 [,] ( 1 / 3 ) ) )
32 iitop 
 |-  II e. Top
33 24 25 sstri 
 |-  { 0 } C_ ( 0 [,] ( 1 / 3 ) )
34 33 15 sstri 
 |-  { 0 } C_ ( 0 [,] 1 )
35 iiuni 
 |-  ( 0 [,] 1 ) = U. II
36 35 isnei 
 |-  ( ( II e. Top /\ { 0 } C_ ( 0 [,] 1 ) ) -> ( ( 0 [,] ( 1 / 3 ) ) e. ( ( nei ` II ) ` { 0 } ) <-> ( ( 0 [,] ( 1 / 3 ) ) C_ ( 0 [,] 1 ) /\ E. g e. II ( { 0 } C_ g /\ g C_ ( 0 [,] ( 1 / 3 ) ) ) ) ) )
37 32 34 36 mp2an 
 |-  ( ( 0 [,] ( 1 / 3 ) ) e. ( ( nei ` II ) ` { 0 } ) <-> ( ( 0 [,] ( 1 / 3 ) ) C_ ( 0 [,] 1 ) /\ E. g e. II ( { 0 } C_ g /\ g C_ ( 0 [,] ( 1 / 3 ) ) ) ) )
38 15 31 37 mpbir2an 
 |-  ( 0 [,] ( 1 / 3 ) ) e. ( ( nei ` II ) ` { 0 } )
39 38 a1i 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> ( 0 [,] ( 1 / 3 ) ) e. ( ( nei ` II ) ` { 0 } ) )
40 simprl 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> S C_ ( `' f " { 0 } ) )
41 2 39 40 cnneiima 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> ( `' f " ( 0 [,] ( 1 / 3 ) ) ) e. ( ( nei ` J ) ` S ) )
42 halfge0 
 |-  0 <_ ( 1 / 2 )
43 1le1 
 |-  1 <_ 1
44 iccss 
 |-  ( ( ( 0 e. RR /\ 1 e. RR ) /\ ( 0 <_ ( 1 / 2 ) /\ 1 <_ 1 ) ) -> ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 ) )
45 3 4 42 43 44 mp4an 
 |-  ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 )
46 io1ii 
 |-  ( 0 <_ ( 1 / 2 ) -> ( ( 1 / 2 ) (,] 1 ) e. II )
47 42 46 ax-mp 
 |-  ( ( 1 / 2 ) (,] 1 ) e. II
48 halflt1 
 |-  ( 1 / 2 ) < 1
49 halfre 
 |-  ( 1 / 2 ) e. RR
50 49 rexri 
 |-  ( 1 / 2 ) e. RR*
51 elioc2 
 |-  ( ( ( 1 / 2 ) e. RR* /\ 1 e. RR ) -> ( 1 e. ( ( 1 / 2 ) (,] 1 ) <-> ( 1 e. RR /\ ( 1 / 2 ) < 1 /\ 1 <_ 1 ) ) )
52 50 4 51 mp2an 
 |-  ( 1 e. ( ( 1 / 2 ) (,] 1 ) <-> ( 1 e. RR /\ ( 1 / 2 ) < 1 /\ 1 <_ 1 ) )
53 52 biimpri 
 |-  ( ( 1 e. RR /\ ( 1 / 2 ) < 1 /\ 1 <_ 1 ) -> 1 e. ( ( 1 / 2 ) (,] 1 ) )
54 53 snssd 
 |-  ( ( 1 e. RR /\ ( 1 / 2 ) < 1 /\ 1 <_ 1 ) -> { 1 } C_ ( ( 1 / 2 ) (,] 1 ) )
55 4 48 43 54 mp3an 
 |-  { 1 } C_ ( ( 1 / 2 ) (,] 1 )
56 iocssicc 
 |-  ( ( 1 / 2 ) (,] 1 ) C_ ( ( 1 / 2 ) [,] 1 )
57 55 56 pm3.2i 
 |-  ( { 1 } C_ ( ( 1 / 2 ) (,] 1 ) /\ ( ( 1 / 2 ) (,] 1 ) C_ ( ( 1 / 2 ) [,] 1 ) )
58 sseq2 
 |-  ( h = ( ( 1 / 2 ) (,] 1 ) -> ( { 1 } C_ h <-> { 1 } C_ ( ( 1 / 2 ) (,] 1 ) ) )
59 sseq1 
 |-  ( h = ( ( 1 / 2 ) (,] 1 ) -> ( h C_ ( ( 1 / 2 ) [,] 1 ) <-> ( ( 1 / 2 ) (,] 1 ) C_ ( ( 1 / 2 ) [,] 1 ) ) )
60 58 59 anbi12d 
 |-  ( h = ( ( 1 / 2 ) (,] 1 ) -> ( ( { 1 } C_ h /\ h C_ ( ( 1 / 2 ) [,] 1 ) ) <-> ( { 1 } C_ ( ( 1 / 2 ) (,] 1 ) /\ ( ( 1 / 2 ) (,] 1 ) C_ ( ( 1 / 2 ) [,] 1 ) ) ) )
61 60 rspcev 
 |-  ( ( ( ( 1 / 2 ) (,] 1 ) e. II /\ ( { 1 } C_ ( ( 1 / 2 ) (,] 1 ) /\ ( ( 1 / 2 ) (,] 1 ) C_ ( ( 1 / 2 ) [,] 1 ) ) ) -> E. h e. II ( { 1 } C_ h /\ h C_ ( ( 1 / 2 ) [,] 1 ) ) )
62 47 57 61 mp2an 
 |-  E. h e. II ( { 1 } C_ h /\ h C_ ( ( 1 / 2 ) [,] 1 ) )
63 55 56 sstri 
 |-  { 1 } C_ ( ( 1 / 2 ) [,] 1 )
64 63 45 sstri 
 |-  { 1 } C_ ( 0 [,] 1 )
65 35 isnei 
 |-  ( ( II e. Top /\ { 1 } C_ ( 0 [,] 1 ) ) -> ( ( ( 1 / 2 ) [,] 1 ) e. ( ( nei ` II ) ` { 1 } ) <-> ( ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 ) /\ E. h e. II ( { 1 } C_ h /\ h C_ ( ( 1 / 2 ) [,] 1 ) ) ) ) )
66 32 64 65 mp2an 
 |-  ( ( ( 1 / 2 ) [,] 1 ) e. ( ( nei ` II ) ` { 1 } ) <-> ( ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 ) /\ E. h e. II ( { 1 } C_ h /\ h C_ ( ( 1 / 2 ) [,] 1 ) ) ) )
67 45 62 66 mpbir2an 
 |-  ( ( 1 / 2 ) [,] 1 ) e. ( ( nei ` II ) ` { 1 } )
68 67 a1i 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> ( ( 1 / 2 ) [,] 1 ) e. ( ( nei ` II ) ` { 1 } ) )
69 simprr 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> T C_ ( `' f " { 1 } ) )
70 2 68 69 cnneiima 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> ( `' f " ( ( 1 / 2 ) [,] 1 ) ) e. ( ( nei ` J ) ` T ) )
71 icccldii 
 |-  ( ( 0 <_ 0 /\ ( 1 / 3 ) <_ 1 ) -> ( 0 [,] ( 1 / 3 ) ) e. ( Clsd ` II ) )
72 5 13 71 mp2an 
 |-  ( 0 [,] ( 1 / 3 ) ) e. ( Clsd ` II )
73 cnclima 
 |-  ( ( f e. ( J Cn II ) /\ ( 0 [,] ( 1 / 3 ) ) e. ( Clsd ` II ) ) -> ( `' f " ( 0 [,] ( 1 / 3 ) ) ) e. ( Clsd ` J ) )
74 2 72 73 sylancl 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> ( `' f " ( 0 [,] ( 1 / 3 ) ) ) e. ( Clsd ` J ) )
75 icccldii 
 |-  ( ( 0 <_ ( 1 / 2 ) /\ 1 <_ 1 ) -> ( ( 1 / 2 ) [,] 1 ) e. ( Clsd ` II ) )
76 42 43 75 mp2an 
 |-  ( ( 1 / 2 ) [,] 1 ) e. ( Clsd ` II )
77 cnclima 
 |-  ( ( f e. ( J Cn II ) /\ ( ( 1 / 2 ) [,] 1 ) e. ( Clsd ` II ) ) -> ( `' f " ( ( 1 / 2 ) [,] 1 ) ) e. ( Clsd ` J ) )
78 2 76 77 sylancl 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> ( `' f " ( ( 1 / 2 ) [,] 1 ) ) e. ( Clsd ` J ) )
79 eqid 
 |-  U. J = U. J
80 79 35 cnf 
 |-  ( f e. ( J Cn II ) -> f : U. J --> ( 0 [,] 1 ) )
81 80 ffund 
 |-  ( f e. ( J Cn II ) -> Fun f )
82 2 81 syl 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> Fun f )
83 0xr 
 |-  0 e. RR*
84 1xr 
 |-  1 e. RR*
85 2lt3 
 |-  2 < 3
86 2re 
 |-  2 e. RR
87 2pos 
 |-  0 < 2
88 3pos 
 |-  0 < 3
89 86 6 87 88 ltrecii 
 |-  ( 2 < 3 <-> ( 1 / 3 ) < ( 1 / 2 ) )
90 85 89 mpbi 
 |-  ( 1 / 3 ) < ( 1 / 2 )
91 iccdisj2 
 |-  ( ( 0 e. RR* /\ 1 e. RR* /\ ( 1 / 3 ) < ( 1 / 2 ) ) -> ( ( 0 [,] ( 1 / 3 ) ) i^i ( ( 1 / 2 ) [,] 1 ) ) = (/) )
92 83 84 90 91 mp3an 
 |-  ( ( 0 [,] ( 1 / 3 ) ) i^i ( ( 1 / 2 ) [,] 1 ) ) = (/)
93 92 a1i 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> ( ( 0 [,] ( 1 / 3 ) ) i^i ( ( 1 / 2 ) [,] 1 ) ) = (/) )
94 ssidd 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> ( `' f " ( 0 [,] ( 1 / 3 ) ) ) C_ ( `' f " ( 0 [,] ( 1 / 3 ) ) ) )
95 ssidd 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> ( `' f " ( ( 1 / 2 ) [,] 1 ) ) C_ ( `' f " ( ( 1 / 2 ) [,] 1 ) ) )
96 82 93 94 95 predisj 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i ( `' f " ( ( 1 / 2 ) [,] 1 ) ) ) = (/) )
97 eleq1 
 |-  ( n = ( `' f " ( 0 [,] ( 1 / 3 ) ) ) -> ( n e. ( Clsd ` J ) <-> ( `' f " ( 0 [,] ( 1 / 3 ) ) ) e. ( Clsd ` J ) ) )
98 ineq1 
 |-  ( n = ( `' f " ( 0 [,] ( 1 / 3 ) ) ) -> ( n i^i m ) = ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i m ) )
99 98 eqeq1d 
 |-  ( n = ( `' f " ( 0 [,] ( 1 / 3 ) ) ) -> ( ( n i^i m ) = (/) <-> ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i m ) = (/) ) )
100 97 99 3anbi13d 
 |-  ( n = ( `' f " ( 0 [,] ( 1 / 3 ) ) ) -> ( ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) <-> ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i m ) = (/) ) ) )
101 eleq1 
 |-  ( m = ( `' f " ( ( 1 / 2 ) [,] 1 ) ) -> ( m e. ( Clsd ` J ) <-> ( `' f " ( ( 1 / 2 ) [,] 1 ) ) e. ( Clsd ` J ) ) )
102 ineq2 
 |-  ( m = ( `' f " ( ( 1 / 2 ) [,] 1 ) ) -> ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i m ) = ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i ( `' f " ( ( 1 / 2 ) [,] 1 ) ) ) )
103 102 eqeq1d 
 |-  ( m = ( `' f " ( ( 1 / 2 ) [,] 1 ) ) -> ( ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i m ) = (/) <-> ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i ( `' f " ( ( 1 / 2 ) [,] 1 ) ) ) = (/) ) )
104 101 103 3anbi23d 
 |-  ( m = ( `' f " ( ( 1 / 2 ) [,] 1 ) ) -> ( ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i m ) = (/) ) <-> ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) e. ( Clsd ` J ) /\ ( `' f " ( ( 1 / 2 ) [,] 1 ) ) e. ( Clsd ` J ) /\ ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i ( `' f " ( ( 1 / 2 ) [,] 1 ) ) ) = (/) ) ) )
105 100 104 rspc2ev 
 |-  ( ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) e. ( ( nei ` J ) ` S ) /\ ( `' f " ( ( 1 / 2 ) [,] 1 ) ) e. ( ( nei ` J ) ` T ) /\ ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) e. ( Clsd ` J ) /\ ( `' f " ( ( 1 / 2 ) [,] 1 ) ) e. ( Clsd ` J ) /\ ( ( `' f " ( 0 [,] ( 1 / 3 ) ) ) i^i ( `' f " ( ( 1 / 2 ) [,] 1 ) ) ) = (/) ) ) -> E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) )
106 41 70 74 78 96 105 syl113anc 
 |-  ( ( f e. ( J Cn II ) /\ ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) ) -> E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) )
107 106 rexlimiva 
 |-  ( E. f e. ( J Cn II ) ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) -> E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) )
108 1 107 syl 
 |-  ( ph -> E. n e. ( ( nei ` J ) ` S ) E. m e. ( ( nei ` J ) ` T ) ( n e. ( Clsd ` J ) /\ m e. ( Clsd ` J ) /\ ( n i^i m ) = (/) ) )