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 ( 𝜑 → ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) )
Assertion sepfsepc ( 𝜑 → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛𝑚 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 sepfsepc.1 ( 𝜑 → ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) )
2 simpl ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → 𝑓 ∈ ( 𝐽 Cn II ) )
3 0re 0 ∈ ℝ
4 1re 1 ∈ ℝ
5 0le0 0 ≤ 0
6 3re 3 ∈ ℝ
7 3ne0 3 ≠ 0
8 6 7 rereccli ( 1 / 3 ) ∈ ℝ
9 1lt3 1 < 3
10 recgt1i ( ( 3 ∈ ℝ ∧ 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 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ 0 ∧ ( 1 / 3 ) ≤ 1 ) ) → ( 0 [,] ( 1 / 3 ) ) ⊆ ( 0 [,] 1 ) )
15 3 4 5 13 14 mp4an ( 0 [,] ( 1 / 3 ) ) ⊆ ( 0 [,] 1 )
16 i0oii ( ( 1 / 3 ) ≤ 1 → ( 0 [,) ( 1 / 3 ) ) ∈ II )
17 13 16 ax-mp ( 0 [,) ( 1 / 3 ) ) ∈ II
18 11 simpli 0 < ( 1 / 3 )
19 8 rexri ( 1 / 3 ) ∈ ℝ*
20 elico2 ( ( 0 ∈ ℝ ∧ ( 1 / 3 ) ∈ ℝ* ) → ( 0 ∈ ( 0 [,) ( 1 / 3 ) ) ↔ ( 0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 < ( 1 / 3 ) ) ) )
21 3 19 20 mp2an ( 0 ∈ ( 0 [,) ( 1 / 3 ) ) ↔ ( 0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 < ( 1 / 3 ) ) )
22 21 biimpri ( ( 0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 < ( 1 / 3 ) ) → 0 ∈ ( 0 [,) ( 1 / 3 ) ) )
23 22 snssd ( ( 0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 < ( 1 / 3 ) ) → { 0 } ⊆ ( 0 [,) ( 1 / 3 ) ) )
24 3 5 18 23 mp3an { 0 } ⊆ ( 0 [,) ( 1 / 3 ) )
25 icossicc ( 0 [,) ( 1 / 3 ) ) ⊆ ( 0 [,] ( 1 / 3 ) )
26 24 25 pm3.2i ( { 0 } ⊆ ( 0 [,) ( 1 / 3 ) ) ∧ ( 0 [,) ( 1 / 3 ) ) ⊆ ( 0 [,] ( 1 / 3 ) ) )
27 sseq2 ( 𝑔 = ( 0 [,) ( 1 / 3 ) ) → ( { 0 } ⊆ 𝑔 ↔ { 0 } ⊆ ( 0 [,) ( 1 / 3 ) ) ) )
28 sseq1 ( 𝑔 = ( 0 [,) ( 1 / 3 ) ) → ( 𝑔 ⊆ ( 0 [,] ( 1 / 3 ) ) ↔ ( 0 [,) ( 1 / 3 ) ) ⊆ ( 0 [,] ( 1 / 3 ) ) ) )
29 27 28 anbi12d ( 𝑔 = ( 0 [,) ( 1 / 3 ) ) → ( ( { 0 } ⊆ 𝑔𝑔 ⊆ ( 0 [,] ( 1 / 3 ) ) ) ↔ ( { 0 } ⊆ ( 0 [,) ( 1 / 3 ) ) ∧ ( 0 [,) ( 1 / 3 ) ) ⊆ ( 0 [,] ( 1 / 3 ) ) ) ) )
30 29 rspcev ( ( ( 0 [,) ( 1 / 3 ) ) ∈ II ∧ ( { 0 } ⊆ ( 0 [,) ( 1 / 3 ) ) ∧ ( 0 [,) ( 1 / 3 ) ) ⊆ ( 0 [,] ( 1 / 3 ) ) ) ) → ∃ 𝑔 ∈ II ( { 0 } ⊆ 𝑔𝑔 ⊆ ( 0 [,] ( 1 / 3 ) ) ) )
31 17 26 30 mp2an 𝑔 ∈ II ( { 0 } ⊆ 𝑔𝑔 ⊆ ( 0 [,] ( 1 / 3 ) ) )
32 iitop II ∈ Top
33 24 25 sstri { 0 } ⊆ ( 0 [,] ( 1 / 3 ) )
34 33 15 sstri { 0 } ⊆ ( 0 [,] 1 )
35 iiuni ( 0 [,] 1 ) = II
36 35 isnei ( ( II ∈ Top ∧ { 0 } ⊆ ( 0 [,] 1 ) ) → ( ( 0 [,] ( 1 / 3 ) ) ∈ ( ( nei ‘ II ) ‘ { 0 } ) ↔ ( ( 0 [,] ( 1 / 3 ) ) ⊆ ( 0 [,] 1 ) ∧ ∃ 𝑔 ∈ II ( { 0 } ⊆ 𝑔𝑔 ⊆ ( 0 [,] ( 1 / 3 ) ) ) ) ) )
37 32 34 36 mp2an ( ( 0 [,] ( 1 / 3 ) ) ∈ ( ( nei ‘ II ) ‘ { 0 } ) ↔ ( ( 0 [,] ( 1 / 3 ) ) ⊆ ( 0 [,] 1 ) ∧ ∃ 𝑔 ∈ II ( { 0 } ⊆ 𝑔𝑔 ⊆ ( 0 [,] ( 1 / 3 ) ) ) ) )
38 15 31 37 mpbir2an ( 0 [,] ( 1 / 3 ) ) ∈ ( ( nei ‘ II ) ‘ { 0 } )
39 38 a1i ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ( 0 [,] ( 1 / 3 ) ) ∈ ( ( nei ‘ II ) ‘ { 0 } ) )
40 simprl ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → 𝑆 ⊆ ( 𝑓 “ { 0 } ) )
41 2 39 40 cnneiima ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
42 halfge0 0 ≤ ( 1 / 2 )
43 1le1 1 ≤ 1
44 iccss ( ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ ( 1 / 2 ) ∧ 1 ≤ 1 ) ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ( 0 [,] 1 ) )
45 3 4 42 43 44 mp4an ( ( 1 / 2 ) [,] 1 ) ⊆ ( 0 [,] 1 )
46 io1ii ( 0 ≤ ( 1 / 2 ) → ( ( 1 / 2 ) (,] 1 ) ∈ II )
47 42 46 ax-mp ( ( 1 / 2 ) (,] 1 ) ∈ II
48 halflt1 ( 1 / 2 ) < 1
49 halfre ( 1 / 2 ) ∈ ℝ
50 49 rexri ( 1 / 2 ) ∈ ℝ*
51 elioc2 ( ( ( 1 / 2 ) ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 1 ∈ ( ( 1 / 2 ) (,] 1 ) ↔ ( 1 ∈ ℝ ∧ ( 1 / 2 ) < 1 ∧ 1 ≤ 1 ) ) )
52 50 4 51 mp2an ( 1 ∈ ( ( 1 / 2 ) (,] 1 ) ↔ ( 1 ∈ ℝ ∧ ( 1 / 2 ) < 1 ∧ 1 ≤ 1 ) )
53 52 biimpri ( ( 1 ∈ ℝ ∧ ( 1 / 2 ) < 1 ∧ 1 ≤ 1 ) → 1 ∈ ( ( 1 / 2 ) (,] 1 ) )
54 53 snssd ( ( 1 ∈ ℝ ∧ ( 1 / 2 ) < 1 ∧ 1 ≤ 1 ) → { 1 } ⊆ ( ( 1 / 2 ) (,] 1 ) )
55 4 48 43 54 mp3an { 1 } ⊆ ( ( 1 / 2 ) (,] 1 )
56 iocssicc ( ( 1 / 2 ) (,] 1 ) ⊆ ( ( 1 / 2 ) [,] 1 )
57 55 56 pm3.2i ( { 1 } ⊆ ( ( 1 / 2 ) (,] 1 ) ∧ ( ( 1 / 2 ) (,] 1 ) ⊆ ( ( 1 / 2 ) [,] 1 ) )
58 sseq2 ( = ( ( 1 / 2 ) (,] 1 ) → ( { 1 } ⊆ ↔ { 1 } ⊆ ( ( 1 / 2 ) (,] 1 ) ) )
59 sseq1 ( = ( ( 1 / 2 ) (,] 1 ) → ( ⊆ ( ( 1 / 2 ) [,] 1 ) ↔ ( ( 1 / 2 ) (,] 1 ) ⊆ ( ( 1 / 2 ) [,] 1 ) ) )
60 58 59 anbi12d ( = ( ( 1 / 2 ) (,] 1 ) → ( ( { 1 } ⊆ ⊆ ( ( 1 / 2 ) [,] 1 ) ) ↔ ( { 1 } ⊆ ( ( 1 / 2 ) (,] 1 ) ∧ ( ( 1 / 2 ) (,] 1 ) ⊆ ( ( 1 / 2 ) [,] 1 ) ) ) )
61 60 rspcev ( ( ( ( 1 / 2 ) (,] 1 ) ∈ II ∧ ( { 1 } ⊆ ( ( 1 / 2 ) (,] 1 ) ∧ ( ( 1 / 2 ) (,] 1 ) ⊆ ( ( 1 / 2 ) [,] 1 ) ) ) → ∃ ∈ II ( { 1 } ⊆ ⊆ ( ( 1 / 2 ) [,] 1 ) ) )
62 47 57 61 mp2an ∈ II ( { 1 } ⊆ ⊆ ( ( 1 / 2 ) [,] 1 ) )
63 55 56 sstri { 1 } ⊆ ( ( 1 / 2 ) [,] 1 )
64 63 45 sstri { 1 } ⊆ ( 0 [,] 1 )
65 35 isnei ( ( II ∈ Top ∧ { 1 } ⊆ ( 0 [,] 1 ) ) → ( ( ( 1 / 2 ) [,] 1 ) ∈ ( ( nei ‘ II ) ‘ { 1 } ) ↔ ( ( ( 1 / 2 ) [,] 1 ) ⊆ ( 0 [,] 1 ) ∧ ∃ ∈ II ( { 1 } ⊆ ⊆ ( ( 1 / 2 ) [,] 1 ) ) ) ) )
66 32 64 65 mp2an ( ( ( 1 / 2 ) [,] 1 ) ∈ ( ( nei ‘ II ) ‘ { 1 } ) ↔ ( ( ( 1 / 2 ) [,] 1 ) ⊆ ( 0 [,] 1 ) ∧ ∃ ∈ II ( { 1 } ⊆ ⊆ ( ( 1 / 2 ) [,] 1 ) ) ) )
67 45 62 66 mpbir2an ( ( 1 / 2 ) [,] 1 ) ∈ ( ( nei ‘ II ) ‘ { 1 } )
68 67 a1i ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ( ( 1 / 2 ) [,] 1 ) ∈ ( ( nei ‘ II ) ‘ { 1 } ) )
69 simprr ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → 𝑇 ⊆ ( 𝑓 “ { 1 } ) )
70 2 68 69 cnneiima ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) )
71 icccldii ( ( 0 ≤ 0 ∧ ( 1 / 3 ) ≤ 1 ) → ( 0 [,] ( 1 / 3 ) ) ∈ ( Clsd ‘ II ) )
72 5 13 71 mp2an ( 0 [,] ( 1 / 3 ) ) ∈ ( Clsd ‘ II )
73 cnclima ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 0 [,] ( 1 / 3 ) ) ∈ ( Clsd ‘ II ) ) → ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∈ ( Clsd ‘ 𝐽 ) )
74 2 72 73 sylancl ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∈ ( Clsd ‘ 𝐽 ) )
75 icccldii ( ( 0 ≤ ( 1 / 2 ) ∧ 1 ≤ 1 ) → ( ( 1 / 2 ) [,] 1 ) ∈ ( Clsd ‘ II ) )
76 42 43 75 mp2an ( ( 1 / 2 ) [,] 1 ) ∈ ( Clsd ‘ II )
77 cnclima ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( ( 1 / 2 ) [,] 1 ) ∈ ( Clsd ‘ II ) ) → ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ∈ ( Clsd ‘ 𝐽 ) )
78 2 76 77 sylancl ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ∈ ( Clsd ‘ 𝐽 ) )
79 eqid 𝐽 = 𝐽
80 79 35 cnf ( 𝑓 ∈ ( 𝐽 Cn II ) → 𝑓 : 𝐽 ⟶ ( 0 [,] 1 ) )
81 80 ffund ( 𝑓 ∈ ( 𝐽 Cn II ) → Fun 𝑓 )
82 2 81 syl ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → Fun 𝑓 )
83 0xr 0 ∈ ℝ*
84 1xr 1 ∈ ℝ*
85 2lt3 2 < 3
86 2re 2 ∈ ℝ
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 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ ( 1 / 3 ) < ( 1 / 2 ) ) → ( ( 0 [,] ( 1 / 3 ) ) ∩ ( ( 1 / 2 ) [,] 1 ) ) = ∅ )
92 83 84 90 91 mp3an ( ( 0 [,] ( 1 / 3 ) ) ∩ ( ( 1 / 2 ) [,] 1 ) ) = ∅
93 92 a1i ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ( ( 0 [,] ( 1 / 3 ) ) ∩ ( ( 1 / 2 ) [,] 1 ) ) = ∅ )
94 ssidd ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ⊆ ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) )
95 ssidd ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ⊆ ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) )
96 82 93 94 95 predisj ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ) = ∅ )
97 eleq1 ( 𝑛 = ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) → ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∈ ( Clsd ‘ 𝐽 ) ) )
98 ineq1 ( 𝑛 = ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) → ( 𝑛𝑚 ) = ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ 𝑚 ) )
99 98 eqeq1d ( 𝑛 = ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) → ( ( 𝑛𝑚 ) = ∅ ↔ ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ 𝑚 ) = ∅ ) )
100 97 99 3anbi13d ( 𝑛 = ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) → ( ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛𝑚 ) = ∅ ) ↔ ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ 𝑚 ) = ∅ ) ) )
101 eleq1 ( 𝑚 = ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) → ( 𝑚 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ∈ ( Clsd ‘ 𝐽 ) ) )
102 ineq2 ( 𝑚 = ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ 𝑚 ) = ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ) )
103 102 eqeq1d ( 𝑚 = ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) → ( ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ 𝑚 ) = ∅ ↔ ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ) = ∅ ) )
104 101 103 3anbi23d ( 𝑚 = ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) → ( ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ 𝑚 ) = ∅ ) ↔ ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ) = ∅ ) ) )
105 100 104 rspc2ev ( ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ∧ ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( 𝑓 “ ( 0 [,] ( 1 / 3 ) ) ) ∩ ( 𝑓 “ ( ( 1 / 2 ) [,] 1 ) ) ) = ∅ ) ) → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛𝑚 ) = ∅ ) )
106 41 70 74 78 96 105 syl113anc ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) ) → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛𝑚 ) = ∅ ) )
107 106 rexlimiva ( ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 ⊆ ( 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( 𝑓 “ { 1 } ) ) → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛𝑚 ) = ∅ ) )
108 1 107 syl ( 𝜑 → ∃ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∃ 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑇 ) ( 𝑛 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑚 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑛𝑚 ) = ∅ ) )