This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐵 [,] 𝐶 ) → 𝑤 ≤ 𝐶 ) )
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 biimtrrid ⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ ( ℝ ∖ 𝐴 ) ) )
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 biimtrrid ⊢ ( 𝜑 → ( ( 𝑆 ∈ 𝑈 ∧ 𝑆 ∈ ( -∞ (,) 𝐶 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑆 ( 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 ⊢ ( 𝜑 → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) )