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 ‘ 𝐽 ) ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )