Metamath Proof Explorer


Theorem reconnlem2

Description: Lemma for reconn . (Contributed by Jeff Hankins, 17-Aug-2009) (Proof shortened by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses reconnlem2.1 ( 𝜑𝐴 ⊆ ℝ )
reconnlem2.2 ( 𝜑𝑈 ∈ ( topGen ‘ ran (,) ) )
reconnlem2.3 ( 𝜑𝑉 ∈ ( topGen ‘ ran (,) ) )
reconnlem2.4 ( 𝜑 → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
reconnlem2.5 ( 𝜑𝐵 ∈ ( 𝑈𝐴 ) )
reconnlem2.6 ( 𝜑𝐶 ∈ ( 𝑉𝐴 ) )
reconnlem2.7 ( 𝜑 → ( 𝑈𝑉 ) ⊆ ( ℝ ∖ 𝐴 ) )
reconnlem2.8 ( 𝜑𝐵𝐶 )
reconnlem2.9 𝑆 = sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < )
Assertion reconnlem2 ( 𝜑 → ¬ 𝐴 ⊆ ( 𝑈𝑉 ) )

Proof

Step Hyp Ref Expression
1 reconnlem2.1 ( 𝜑𝐴 ⊆ ℝ )
2 reconnlem2.2 ( 𝜑𝑈 ∈ ( topGen ‘ ran (,) ) )
3 reconnlem2.3 ( 𝜑𝑉 ∈ ( topGen ‘ ran (,) ) )
4 reconnlem2.4 ( 𝜑 → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
5 reconnlem2.5 ( 𝜑𝐵 ∈ ( 𝑈𝐴 ) )
6 reconnlem2.6 ( 𝜑𝐶 ∈ ( 𝑉𝐴 ) )
7 reconnlem2.7 ( 𝜑 → ( 𝑈𝑉 ) ⊆ ( ℝ ∖ 𝐴 ) )
8 reconnlem2.8 ( 𝜑𝐵𝐶 )
9 reconnlem2.9 𝑆 = sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < )
10 inss2 ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ⊆ ( 𝐵 [,] 𝐶 )
11 5 elin2d ( 𝜑𝐵𝐴 )
12 6 elin2d ( 𝜑𝐶𝐴 )
13 oveq1 ( 𝑥 = 𝐵 → ( 𝑥 [,] 𝑦 ) = ( 𝐵 [,] 𝑦 ) )
14 13 sseq1d ( 𝑥 = 𝐵 → ( ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ↔ ( 𝐵 [,] 𝑦 ) ⊆ 𝐴 ) )
15 oveq2 ( 𝑦 = 𝐶 → ( 𝐵 [,] 𝑦 ) = ( 𝐵 [,] 𝐶 ) )
16 15 sseq1d ( 𝑦 = 𝐶 → ( ( 𝐵 [,] 𝑦 ) ⊆ 𝐴 ↔ ( 𝐵 [,] 𝐶 ) ⊆ 𝐴 ) )
17 14 16 rspc2va ( ( ( 𝐵𝐴𝐶𝐴 ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) → ( 𝐵 [,] 𝐶 ) ⊆ 𝐴 )
18 11 12 4 17 syl21anc ( 𝜑 → ( 𝐵 [,] 𝐶 ) ⊆ 𝐴 )
19 18 1 sstrd ( 𝜑 → ( 𝐵 [,] 𝐶 ) ⊆ ℝ )
20 10 19 sstrid ( 𝜑 → ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ⊆ ℝ )
21 5 elin1d ( 𝜑𝐵𝑈 )
22 1 11 sseldd ( 𝜑𝐵 ∈ ℝ )
23 22 rexrd ( 𝜑𝐵 ∈ ℝ* )
24 1 12 sseldd ( 𝜑𝐶 ∈ ℝ )
25 24 rexrd ( 𝜑𝐶 ∈ ℝ* )
26 lbicc2 ( ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ*𝐵𝐶 ) → 𝐵 ∈ ( 𝐵 [,] 𝐶 ) )
27 23 25 8 26 syl3anc ( 𝜑𝐵 ∈ ( 𝐵 [,] 𝐶 ) )
28 21 27 elind ( 𝜑𝐵 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) )
29 28 ne0d ( 𝜑 → ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ≠ ∅ )
30 elinel2 ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) → 𝑤 ∈ ( 𝐵 [,] 𝐶 ) )
31 elicc2 ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑤 ∈ ( 𝐵 [,] 𝐶 ) ↔ ( 𝑤 ∈ ℝ ∧ 𝐵𝑤𝑤𝐶 ) ) )
32 22 24 31 syl2anc ( 𝜑 → ( 𝑤 ∈ ( 𝐵 [,] 𝐶 ) ↔ ( 𝑤 ∈ ℝ ∧ 𝐵𝑤𝑤𝐶 ) ) )
33 simp3 ( ( 𝑤 ∈ ℝ ∧ 𝐵𝑤𝑤𝐶 ) → 𝑤𝐶 )
34 32 33 syl6bi ( 𝜑 → ( 𝑤 ∈ ( 𝐵 [,] 𝐶 ) → 𝑤𝐶 ) )
35 30 34 syl5 ( 𝜑 → ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) → 𝑤𝐶 ) )
36 35 ralrimiv ( 𝜑 → ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝐶 )
37 brralrspcev ( ( 𝐶 ∈ ℝ ∧ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝐶 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝑧 )
38 24 36 37 syl2anc ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝑧 )
39 20 29 38 suprcld ( 𝜑 → sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < ) ∈ ℝ )
40 9 39 eqeltrid ( 𝜑𝑆 ∈ ℝ )
41 rphalfcl ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ+ )
42 ltaddrp ( ( 𝑆 ∈ ℝ ∧ ( 𝑟 / 2 ) ∈ ℝ+ ) → 𝑆 < ( 𝑆 + ( 𝑟 / 2 ) ) )
43 40 41 42 syl2an ( ( 𝜑𝑟 ∈ ℝ+ ) → 𝑆 < ( 𝑆 + ( 𝑟 / 2 ) ) )
44 40 adantr ( ( 𝜑𝑟 ∈ ℝ+ ) → 𝑆 ∈ ℝ )
45 41 rpred ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ )
46 readdcl ( ( 𝑆 ∈ ℝ ∧ ( 𝑟 / 2 ) ∈ ℝ ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ℝ )
47 40 45 46 syl2an ( ( 𝜑𝑟 ∈ ℝ+ ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ℝ )
48 44 47 ltnled ( ( 𝜑𝑟 ∈ ℝ+ ) → ( 𝑆 < ( 𝑆 + ( 𝑟 / 2 ) ) ↔ ¬ ( 𝑆 + ( 𝑟 / 2 ) ) ≤ 𝑆 ) )
49 43 48 mpbid ( ( 𝜑𝑟 ∈ ℝ+ ) → ¬ ( 𝑆 + ( 𝑟 / 2 ) ) ≤ 𝑆 )
50 20 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ⊆ ℝ )
51 29 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ≠ ∅ )
52 38 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝑧 )
53 simpr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) )
54 53 elin1d ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ 𝑈 )
55 47 adantr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ℝ )
56 22 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → 𝐵 ∈ ℝ )
57 40 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → 𝑆 ∈ ℝ )
58 20 29 38 28 suprubd ( 𝜑𝐵 ≤ sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < ) )
59 58 9 breqtrrdi ( 𝜑𝐵𝑆 )
60 59 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → 𝐵𝑆 )
61 43 adantr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → 𝑆 < ( 𝑆 + ( 𝑟 / 2 ) ) )
62 57 55 61 ltled ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → 𝑆 ≤ ( 𝑆 + ( 𝑟 / 2 ) ) )
63 56 57 55 60 62 letrd ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → 𝐵 ≤ ( 𝑆 + ( 𝑟 / 2 ) ) )
64 24 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → 𝐶 ∈ ℝ )
65 53 elin2d ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( -∞ (,) 𝐶 ) )
66 eliooord ( ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( -∞ (,) 𝐶 ) → ( -∞ < ( 𝑆 + ( 𝑟 / 2 ) ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) < 𝐶 ) )
67 66 simprd ( ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( -∞ (,) 𝐶 ) → ( 𝑆 + ( 𝑟 / 2 ) ) < 𝐶 )
68 65 67 syl ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) < 𝐶 )
69 55 64 68 ltled ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) ≤ 𝐶 )
70 elicc2 ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝐵 [,] 𝐶 ) ↔ ( ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ℝ ∧ 𝐵 ≤ ( 𝑆 + ( 𝑟 / 2 ) ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ≤ 𝐶 ) ) )
71 56 64 70 syl2anc ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝐵 [,] 𝐶 ) ↔ ( ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ℝ ∧ 𝐵 ≤ ( 𝑆 + ( 𝑟 / 2 ) ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ≤ 𝐶 ) ) )
72 55 63 69 71 mpbir3and ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝐵 [,] 𝐶 ) )
73 54 72 elind ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) )
74 50 51 52 73 suprubd ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) ≤ sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < ) )
75 74 9 breqtrrdi ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) ≤ 𝑆 )
76 49 75 mtand ( ( 𝜑𝑟 ∈ ℝ+ ) → ¬ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) )
77 eqid ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
78 77 remetdval ( ( ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( ( 𝑆 + ( 𝑟 / 2 ) ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑆 ) = ( abs ‘ ( ( 𝑆 + ( 𝑟 / 2 ) ) − 𝑆 ) ) )
79 47 44 78 syl2anc ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( 𝑆 + ( 𝑟 / 2 ) ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑆 ) = ( abs ‘ ( ( 𝑆 + ( 𝑟 / 2 ) ) − 𝑆 ) ) )
80 44 recnd ( ( 𝜑𝑟 ∈ ℝ+ ) → 𝑆 ∈ ℂ )
81 45 adantl ( ( 𝜑𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) ∈ ℝ )
82 81 recnd ( ( 𝜑𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) ∈ ℂ )
83 80 82 pncan2d ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( 𝑆 + ( 𝑟 / 2 ) ) − 𝑆 ) = ( 𝑟 / 2 ) )
84 83 fveq2d ( ( 𝜑𝑟 ∈ ℝ+ ) → ( abs ‘ ( ( 𝑆 + ( 𝑟 / 2 ) ) − 𝑆 ) ) = ( abs ‘ ( 𝑟 / 2 ) ) )
85 41 adantl ( ( 𝜑𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) ∈ ℝ+ )
86 rpre ( ( 𝑟 / 2 ) ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ )
87 rpge0 ( ( 𝑟 / 2 ) ∈ ℝ+ → 0 ≤ ( 𝑟 / 2 ) )
88 86 87 absidd ( ( 𝑟 / 2 ) ∈ ℝ+ → ( abs ‘ ( 𝑟 / 2 ) ) = ( 𝑟 / 2 ) )
89 85 88 syl ( ( 𝜑𝑟 ∈ ℝ+ ) → ( abs ‘ ( 𝑟 / 2 ) ) = ( 𝑟 / 2 ) )
90 79 84 89 3eqtrd ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( 𝑆 + ( 𝑟 / 2 ) ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑆 ) = ( 𝑟 / 2 ) )
91 rphalflt ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) < 𝑟 )
92 91 adantl ( ( 𝜑𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) < 𝑟 )
93 90 92 eqbrtrd ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( 𝑆 + ( 𝑟 / 2 ) ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑆 ) < 𝑟 )
94 77 rexmet ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
95 94 a1i ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) )
96 rpxr ( 𝑟 ∈ ℝ+𝑟 ∈ ℝ* )
97 96 adantl ( ( 𝜑𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ* )
98 elbl3 ( ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ 𝑟 ∈ ℝ* ) ∧ ( 𝑆 ∈ ℝ ∧ ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ℝ ) ) → ( ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ↔ ( ( 𝑆 + ( 𝑟 / 2 ) ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑆 ) < 𝑟 ) )
99 95 97 44 47 98 syl22anc ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ↔ ( ( 𝑆 + ( 𝑟 / 2 ) ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝑆 ) < 𝑟 ) )
100 93 99 mpbird ( ( 𝜑𝑟 ∈ ℝ+ ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) )
101 ssel ( ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) → ( ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) )
102 100 101 syl5com ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) → ( 𝑆 + ( 𝑟 / 2 ) ) ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) )
103 76 102 mtod ( ( 𝜑𝑟 ∈ ℝ+ ) → ¬ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) )
104 103 nrexdv ( 𝜑 → ¬ ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) )
105 40 adantr ( ( 𝜑𝑆𝑈 ) → 𝑆 ∈ ℝ )
106 105 mnfltd ( ( 𝜑𝑆𝑈 ) → -∞ < 𝑆 )
107 suprleub ( ( ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ⊆ ℝ ∧ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝑧 ) ∧ 𝐶 ∈ ℝ ) → ( sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < ) ≤ 𝐶 ↔ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝐶 ) )
108 20 29 38 24 107 syl31anc ( 𝜑 → ( sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < ) ≤ 𝐶 ↔ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝐶 ) )
109 36 108 mpbird ( 𝜑 → sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < ) ≤ 𝐶 )
110 9 109 eqbrtrid ( 𝜑𝑆𝐶 )
111 40 24 leloed ( 𝜑 → ( 𝑆𝐶 ↔ ( 𝑆 < 𝐶𝑆 = 𝐶 ) ) )
112 110 111 mpbid ( 𝜑 → ( 𝑆 < 𝐶𝑆 = 𝐶 ) )
113 112 ord ( 𝜑 → ( ¬ 𝑆 < 𝐶𝑆 = 𝐶 ) )
114 elndif ( 𝐶𝐴 → ¬ 𝐶 ∈ ( ℝ ∖ 𝐴 ) )
115 12 114 syl ( 𝜑 → ¬ 𝐶 ∈ ( ℝ ∖ 𝐴 ) )
116 6 elin1d ( 𝜑𝐶𝑉 )
117 elin ( 𝐶 ∈ ( 𝑈𝑉 ) ↔ ( 𝐶𝑈𝐶𝑉 ) )
118 7 sseld ( 𝜑 → ( 𝐶 ∈ ( 𝑈𝑉 ) → 𝐶 ∈ ( ℝ ∖ 𝐴 ) ) )
119 117 118 syl5bir ( 𝜑 → ( ( 𝐶𝑈𝐶𝑉 ) → 𝐶 ∈ ( ℝ ∖ 𝐴 ) ) )
120 116 119 mpan2d ( 𝜑 → ( 𝐶𝑈𝐶 ∈ ( ℝ ∖ 𝐴 ) ) )
121 115 120 mtod ( 𝜑 → ¬ 𝐶𝑈 )
122 eleq1 ( 𝑆 = 𝐶 → ( 𝑆𝑈𝐶𝑈 ) )
123 122 notbid ( 𝑆 = 𝐶 → ( ¬ 𝑆𝑈 ↔ ¬ 𝐶𝑈 ) )
124 121 123 syl5ibrcom ( 𝜑 → ( 𝑆 = 𝐶 → ¬ 𝑆𝑈 ) )
125 113 124 syld ( 𝜑 → ( ¬ 𝑆 < 𝐶 → ¬ 𝑆𝑈 ) )
126 125 con4d ( 𝜑 → ( 𝑆𝑈𝑆 < 𝐶 ) )
127 126 imp ( ( 𝜑𝑆𝑈 ) → 𝑆 < 𝐶 )
128 mnfxr -∞ ∈ ℝ*
129 elioo2 ( ( -∞ ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝑆 ∈ ( -∞ (,) 𝐶 ) ↔ ( 𝑆 ∈ ℝ ∧ -∞ < 𝑆𝑆 < 𝐶 ) ) )
130 128 25 129 sylancr ( 𝜑 → ( 𝑆 ∈ ( -∞ (,) 𝐶 ) ↔ ( 𝑆 ∈ ℝ ∧ -∞ < 𝑆𝑆 < 𝐶 ) ) )
131 130 adantr ( ( 𝜑𝑆𝑈 ) → ( 𝑆 ∈ ( -∞ (,) 𝐶 ) ↔ ( 𝑆 ∈ ℝ ∧ -∞ < 𝑆𝑆 < 𝐶 ) ) )
132 105 106 127 131 mpbir3and ( ( 𝜑𝑆𝑈 ) → 𝑆 ∈ ( -∞ (,) 𝐶 ) )
133 132 ex ( 𝜑 → ( 𝑆𝑈𝑆 ∈ ( -∞ (,) 𝐶 ) ) )
134 133 ancld ( 𝜑 → ( 𝑆𝑈 → ( 𝑆𝑈𝑆 ∈ ( -∞ (,) 𝐶 ) ) ) )
135 elin ( 𝑆 ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ↔ ( 𝑆𝑈𝑆 ∈ ( -∞ (,) 𝐶 ) ) )
136 retop ( topGen ‘ ran (,) ) ∈ Top
137 iooretop ( -∞ (,) 𝐶 ) ∈ ( topGen ‘ ran (,) )
138 inopn ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝑈 ∈ ( topGen ‘ ran (,) ) ∧ ( -∞ (,) 𝐶 ) ∈ ( topGen ‘ ran (,) ) ) → ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ∈ ( topGen ‘ ran (,) ) )
139 136 137 138 mp3an13 ( 𝑈 ∈ ( topGen ‘ ran (,) ) → ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ∈ ( topGen ‘ ran (,) ) )
140 eqid ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
141 77 140 tgioo ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
142 141 mopni2 ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ∈ ( topGen ‘ ran (,) ) ∧ 𝑆 ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) )
143 94 142 mp3an1 ( ( ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ∈ ( topGen ‘ ran (,) ) ∧ 𝑆 ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) )
144 143 ex ( ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ∈ ( topGen ‘ ran (,) ) → ( 𝑆 ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) )
145 2 139 144 3syl ( 𝜑 → ( 𝑆 ∈ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) )
146 135 145 syl5bir ( 𝜑 → ( ( 𝑆𝑈𝑆 ∈ ( -∞ (,) 𝐶 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) )
147 134 146 syld ( 𝜑 → ( 𝑆𝑈 → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑈 ∩ ( -∞ (,) 𝐶 ) ) ) )
148 104 147 mtod ( 𝜑 → ¬ 𝑆𝑈 )
149 ltsubrp ( ( 𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ+ ) → ( 𝑆𝑟 ) < 𝑆 )
150 40 149 sylan ( ( 𝜑𝑟 ∈ ℝ+ ) → ( 𝑆𝑟 ) < 𝑆 )
151 rpre ( 𝑟 ∈ ℝ+𝑟 ∈ ℝ )
152 resubcl ( ( 𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑆𝑟 ) ∈ ℝ )
153 40 151 152 syl2an ( ( 𝜑𝑟 ∈ ℝ+ ) → ( 𝑆𝑟 ) ∈ ℝ )
154 153 44 ltnled ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( 𝑆𝑟 ) < 𝑆 ↔ ¬ 𝑆 ≤ ( 𝑆𝑟 ) ) )
155 150 154 mpbid ( ( 𝜑𝑟 ∈ ℝ+ ) → ¬ 𝑆 ≤ ( 𝑆𝑟 ) )
156 77 bl2ioo ( ( 𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) )
157 40 151 156 syl2an ( ( 𝜑𝑟 ∈ ℝ+ ) → ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) )
158 157 sseq1d ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑉 ↔ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) )
159 20 ad3antrrr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ) → ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ⊆ ℝ )
160 simpr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ) → 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) )
161 159 160 sseldd ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ) → 𝑤 ∈ ℝ )
162 153 ad2antrr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ) → ( 𝑆𝑟 ) ∈ ℝ )
163 18 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) → ( 𝐵 [,] 𝐶 ) ⊆ 𝐴 )
164 10 163 sstrid ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) → ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ⊆ 𝐴 )
165 164 sselda ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ) → 𝑤𝐴 )
166 elndif ( 𝑤𝐴 → ¬ 𝑤 ∈ ( ℝ ∖ 𝐴 ) )
167 165 166 syl ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ) → ¬ 𝑤 ∈ ( ℝ ∖ 𝐴 ) )
168 7 ad3antrrr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → ( 𝑈𝑉 ) ⊆ ( ℝ ∖ 𝐴 ) )
169 simprl ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) )
170 169 elin1d ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑤𝑈 )
171 simplr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 )
172 161 adantrr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑤 ∈ ℝ )
173 simprr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → ( 𝑆𝑟 ) < 𝑤 )
174 44 ad2antrr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑆 ∈ ℝ )
175 simpllr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑟 ∈ ℝ+ )
176 175 rpred ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑟 ∈ ℝ )
177 174 176 readdcld ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → ( 𝑆 + 𝑟 ) ∈ ℝ )
178 159 adantrr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ⊆ ℝ )
179 29 ad3antrrr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ≠ ∅ )
180 38 ad3antrrr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝑧 )
181 178 179 180 169 suprubd ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑤 ≤ sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < ) )
182 181 9 breqtrrdi ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑤𝑆 )
183 174 175 ltaddrpd ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑆 < ( 𝑆 + 𝑟 ) )
184 172 174 177 182 183 lelttrd ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑤 < ( 𝑆 + 𝑟 ) )
185 153 ad2antrr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → ( 𝑆𝑟 ) ∈ ℝ )
186 rexr ( ( 𝑆𝑟 ) ∈ ℝ → ( 𝑆𝑟 ) ∈ ℝ* )
187 rexr ( ( 𝑆 + 𝑟 ) ∈ ℝ → ( 𝑆 + 𝑟 ) ∈ ℝ* )
188 elioo2 ( ( ( 𝑆𝑟 ) ∈ ℝ* ∧ ( 𝑆 + 𝑟 ) ∈ ℝ* ) → ( 𝑤 ∈ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( 𝑆𝑟 ) < 𝑤𝑤 < ( 𝑆 + 𝑟 ) ) ) )
189 186 187 188 syl2an ( ( ( 𝑆𝑟 ) ∈ ℝ ∧ ( 𝑆 + 𝑟 ) ∈ ℝ ) → ( 𝑤 ∈ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( 𝑆𝑟 ) < 𝑤𝑤 < ( 𝑆 + 𝑟 ) ) ) )
190 185 177 189 syl2anc ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → ( 𝑤 ∈ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( 𝑆𝑟 ) < 𝑤𝑤 < ( 𝑆 + 𝑟 ) ) ) )
191 172 173 184 190 mpbir3and ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑤 ∈ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) )
192 171 191 sseldd ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑤𝑉 )
193 170 192 elind ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑤 ∈ ( 𝑈𝑉 ) )
194 168 193 sseldd ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ ( 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ∧ ( 𝑆𝑟 ) < 𝑤 ) ) → 𝑤 ∈ ( ℝ ∖ 𝐴 ) )
195 194 expr ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ) → ( ( 𝑆𝑟 ) < 𝑤𝑤 ∈ ( ℝ ∖ 𝐴 ) ) )
196 167 195 mtod ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ) → ¬ ( 𝑆𝑟 ) < 𝑤 )
197 161 162 196 nltled ( ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) ∧ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ) → 𝑤 ≤ ( 𝑆𝑟 ) )
198 197 ralrimiva ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) → ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤 ≤ ( 𝑆𝑟 ) )
199 20 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) → ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ⊆ ℝ )
200 29 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) → ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ≠ ∅ )
201 38 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝑧 )
202 153 adantr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) → ( 𝑆𝑟 ) ∈ ℝ )
203 suprleub ( ( ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ⊆ ℝ ∧ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤𝑧 ) ∧ ( 𝑆𝑟 ) ∈ ℝ ) → ( sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < ) ≤ ( 𝑆𝑟 ) ↔ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤 ≤ ( 𝑆𝑟 ) ) )
204 199 200 201 202 203 syl31anc ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) → ( sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < ) ≤ ( 𝑆𝑟 ) ↔ ∀ 𝑤 ∈ ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) 𝑤 ≤ ( 𝑆𝑟 ) ) )
205 198 204 mpbird ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) → sup ( ( 𝑈 ∩ ( 𝐵 [,] 𝐶 ) ) , ℝ , < ) ≤ ( 𝑆𝑟 ) )
206 9 205 eqbrtrid ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉 ) → 𝑆 ≤ ( 𝑆𝑟 ) )
207 206 ex ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( ( 𝑆𝑟 ) (,) ( 𝑆 + 𝑟 ) ) ⊆ 𝑉𝑆 ≤ ( 𝑆𝑟 ) ) )
208 158 207 sylbid ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑉𝑆 ≤ ( 𝑆𝑟 ) ) )
209 155 208 mtod ( ( 𝜑𝑟 ∈ ℝ+ ) → ¬ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑉 )
210 209 nrexdv ( 𝜑 → ¬ ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑉 )
211 141 mopni2 ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ 𝑉 ∈ ( topGen ‘ ran (,) ) ∧ 𝑆𝑉 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑉 )
212 94 211 mp3an1 ( ( 𝑉 ∈ ( topGen ‘ ran (,) ) ∧ 𝑆𝑉 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑉 )
213 212 ex ( 𝑉 ∈ ( topGen ‘ ran (,) ) → ( 𝑆𝑉 → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑉 ) )
214 3 213 syl ( 𝜑 → ( 𝑆𝑉 → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑉 ) )
215 210 214 mtod ( 𝜑 → ¬ 𝑆𝑉 )
216 ioran ( ¬ ( 𝑆𝑈𝑆𝑉 ) ↔ ( ¬ 𝑆𝑈 ∧ ¬ 𝑆𝑉 ) )
217 148 215 216 sylanbrc ( 𝜑 → ¬ ( 𝑆𝑈𝑆𝑉 ) )
218 elun ( 𝑆 ∈ ( 𝑈𝑉 ) ↔ ( 𝑆𝑈𝑆𝑉 ) )
219 217 218 sylnibr ( 𝜑 → ¬ 𝑆 ∈ ( 𝑈𝑉 ) )
220 elicc2 ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑆 ∈ ( 𝐵 [,] 𝐶 ) ↔ ( 𝑆 ∈ ℝ ∧ 𝐵𝑆𝑆𝐶 ) ) )
221 22 24 220 syl2anc ( 𝜑 → ( 𝑆 ∈ ( 𝐵 [,] 𝐶 ) ↔ ( 𝑆 ∈ ℝ ∧ 𝐵𝑆𝑆𝐶 ) ) )
222 40 59 110 221 mpbir3and ( 𝜑𝑆 ∈ ( 𝐵 [,] 𝐶 ) )
223 18 222 sseldd ( 𝜑𝑆𝐴 )
224 ssel ( 𝐴 ⊆ ( 𝑈𝑉 ) → ( 𝑆𝐴𝑆 ∈ ( 𝑈𝑉 ) ) )
225 223 224 syl5com ( 𝜑 → ( 𝐴 ⊆ ( 𝑈𝑉 ) → 𝑆 ∈ ( 𝑈𝑉 ) ) )
226 219 225 mtod ( 𝜑 → ¬ 𝐴 ⊆ ( 𝑈𝑉 ) )