Metamath Proof Explorer

Theorem icccmplem2

Description: Lemma for icccmp . (Contributed by Mario Carneiro, 13-Jun-2014)

Ref Expression
Hypotheses icccmp.1 ⊢ 𝐽 = ( topGen ‘ ran (,) )
icccmp.2 ⊢ 𝑇 = ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) )
icccmp.3 ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
icccmp.4 ⊢ 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 }
icccmp.5 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
icccmp.6 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
icccmp.7 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
icccmp.8 ⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
icccmp.9 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
icccmp.10 ⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
icccmp.11 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
icccmp.12 ⊢ ( 𝜑 → ( 𝐺 ( ball ‘ 𝐷 ) 𝐶 ) ⊆ 𝑉 )
icccmp.13 ⊢ 𝐺 = sup ( 𝑆 , ℝ , < )
icccmp.14 ⊢ 𝑅 = if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 )
Assertion icccmplem2 ( 𝜑 → 𝐵 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 icccmp.1 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 icccmp.2 ⊢ 𝑇 = ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) )
3 icccmp.3 ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
4 icccmp.4 ⊢ 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 }
5 icccmp.5 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6 icccmp.6 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
7 icccmp.7 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
8 icccmp.8 ⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
9 icccmp.9 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
10 icccmp.10 ⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
11 icccmp.11 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
12 icccmp.12 ⊢ ( 𝜑 → ( 𝐺 ( ball ‘ 𝐷 ) 𝐶 ) ⊆ 𝑉 )
13 icccmp.13 ⊢ 𝐺 = sup ( 𝑆 , ℝ , < )
14 icccmp.14 ⊢ 𝑅 = if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 )
15 4 ssrab3 ⊢ 𝑆 ⊆ ( 𝐴 [,] 𝐵 )
16 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
17 5 6 16 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
18 15 17 sstrid ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
19 1 2 3 4 5 6 7 8 9 icccmplem1 ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 ) )
20 19 simpld ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
21 20 ne0d ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
22 19 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 )
23 brralrspcev ⊢ ( ( 𝐵 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 ) → ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑛 )
24 6 22 23 syl2anc ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑛 )
25 18 21 24 suprcld ⊢ ( 𝜑 → sup ( 𝑆 , ℝ , < ) ∈ ℝ )
26 13 25 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ ℝ )
27 11 rphalfcld ⊢ ( 𝜑 → ( 𝐶 / 2 ) ∈ ℝ+ )
28 26 27 ltaddrpd ⊢ ( 𝜑 → 𝐺 < ( 𝐺 + ( 𝐶 / 2 ) ) )
29 27 rpred ⊢ ( 𝜑 → ( 𝐶 / 2 ) ∈ ℝ )
30 26 29 readdcld ⊢ ( 𝜑 → ( 𝐺 + ( 𝐶 / 2 ) ) ∈ ℝ )
31 26 30 ltnled ⊢ ( 𝜑 → ( 𝐺 < ( 𝐺 + ( 𝐶 / 2 ) ) ↔ ¬ ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐺 ) )
32 28 31 mpbid ⊢ ( 𝜑 → ¬ ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐺 )
33 30 6 ifcld ⊢ ( 𝜑 → if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) ∈ ℝ )
34 14 33 eqeltrid ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
35 18 21 24 20 suprubd ⊢ ( 𝜑 → 𝐴 ≤ sup ( 𝑆 , ℝ , < ) )
36 35 13 breqtrrdi ⊢ ( 𝜑 → 𝐴 ≤ 𝐺 )
37 26 30 28 ltled ⊢ ( 𝜑 → 𝐺 ≤ ( 𝐺 + ( 𝐶 / 2 ) ) )
38 5 26 30 36 37 letrd ⊢ ( 𝜑 → 𝐴 ≤ ( 𝐺 + ( 𝐶 / 2 ) ) )
39 breq2 ⊢ ( ( 𝐺 + ( 𝐶 / 2 ) ) = if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) → ( 𝐴 ≤ ( 𝐺 + ( 𝐶 / 2 ) ) ↔ 𝐴 ≤ if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) ) )
40 breq2 ⊢ ( 𝐵 = if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) → ( 𝐴 ≤ 𝐵 ↔ 𝐴 ≤ if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) ) )
41 39 40 ifboth ⊢ ( ( 𝐴 ≤ ( 𝐺 + ( 𝐶 / 2 ) ) ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) )
42 38 7 41 syl2anc ⊢ ( 𝜑 → 𝐴 ≤ if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) )
43 42 14 breqtrrdi ⊢ ( 𝜑 → 𝐴 ≤ 𝑅 )
44 min2 ⊢ ( ( ( 𝐺 + ( 𝐶 / 2 ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) ≤ 𝐵 )
45 30 6 44 syl2anc ⊢ ( 𝜑 → if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) ≤ 𝐵 )
46 14 45 eqbrtrid ⊢ ( 𝜑 → 𝑅 ≤ 𝐵 )
47 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑅 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑅 ∈ ℝ ∧ 𝐴 ≤ 𝑅 ∧ 𝑅 ≤ 𝐵 ) ) )
48 5 6 47 syl2anc ⊢ ( 𝜑 → ( 𝑅 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑅 ∈ ℝ ∧ 𝐴 ≤ 𝑅 ∧ 𝑅 ≤ 𝐵 ) ) )
49 34 43 46 48 mpbir3and ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐴 [,] 𝐵 ) )
50 26 11 ltsubrpd ⊢ ( 𝜑 → ( 𝐺 − 𝐶 ) < 𝐺 )
51 50 13 breqtrdi ⊢ ( 𝜑 → ( 𝐺 − 𝐶 ) < sup ( 𝑆 , ℝ , < ) )
52 11 rpred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
53 26 52 resubcld ⊢ ( 𝜑 → ( 𝐺 − 𝐶 ) ∈ ℝ )
54 suprlub ⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑛 ) ∧ ( 𝐺 − 𝐶 ) ∈ ℝ ) → ( ( 𝐺 − 𝐶 ) < sup ( 𝑆 , ℝ , < ) ↔ ∃ 𝑣 ∈ 𝑆 ( 𝐺 − 𝐶 ) < 𝑣 ) )
55 18 21 24 53 54 syl31anc ⊢ ( 𝜑 → ( ( 𝐺 − 𝐶 ) < sup ( 𝑆 , ℝ , < ) ↔ ∃ 𝑣 ∈ 𝑆 ( 𝐺 − 𝐶 ) < 𝑣 ) )
56 51 55 mpbid ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑆 ( 𝐺 − 𝐶 ) < 𝑣 )
57 oveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝐴 [,] 𝑥 ) = ( 𝐴 [,] 𝑣 ) )
58 57 sseq1d ⊢ ( 𝑥 = 𝑣 → ( ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 ↔ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑧 ) )
59 58 rexbidv ⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑧 ) )
60 59 4 elrab2 ⊢ ( 𝑣 ∈ 𝑆 ↔ ( 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ∧ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑧 ) )
61 unieq ⊢ ( 𝑧 = 𝑤 → ∪ 𝑧 = ∪ 𝑤 )
62 61 sseq2d ⊢ ( 𝑧 = 𝑤 → ( ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑧 ↔ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ) )
63 62 cbvrexvw ⊢ ( ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑧 ↔ ∃ 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 )
64 simpr1 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) )
65 elin ⊢ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ↔ ( 𝑤 ∈ 𝒫 𝑈 ∧ 𝑤 ∈ Fin ) )
66 64 65 sylib ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝑤 ∈ 𝒫 𝑈 ∧ 𝑤 ∈ Fin ) )
67 66 simpld ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → 𝑤 ∈ 𝒫 𝑈 )
68 67 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → 𝑤 ⊆ 𝑈 )
69 simpll ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → 𝜑 )
70 69 10 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → 𝑉 ∈ 𝑈 )
71 70 snssd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → { 𝑉 } ⊆ 𝑈 )
72 68 71 unssd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝑤 ∪ { 𝑉 } ) ⊆ 𝑈 )
73 vex ⊢ 𝑤 ∈ V
74 snex ⊢ { 𝑉 } ∈ V
75 73 74 unex ⊢ ( 𝑤 ∪ { 𝑉 } ) ∈ V
76 75 elpw ⊢ ( ( 𝑤 ∪ { 𝑉 } ) ∈ 𝒫 𝑈 ↔ ( 𝑤 ∪ { 𝑉 } ) ⊆ 𝑈 )
77 72 76 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝑤 ∪ { 𝑉 } ) ∈ 𝒫 𝑈 )
78 66 simprd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → 𝑤 ∈ Fin )
79 snfi ⊢ { 𝑉 } ∈ Fin
80 unfi ⊢ ( ( 𝑤 ∈ Fin ∧ { 𝑉 } ∈ Fin ) → ( 𝑤 ∪ { 𝑉 } ) ∈ Fin )
81 78 79 80 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝑤 ∪ { 𝑉 } ) ∈ Fin )
82 77 81 elind ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝑤 ∪ { 𝑉 } ) ∈ ( 𝒫 𝑈 ∩ Fin ) )
83 simplr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑡 ≤ 𝑣 ) ) → ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 )
84 ssun1 ⊢ ∪ 𝑤 ⊆ ( ∪ 𝑤 ∪ 𝑉 )
85 83 84 sstrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑡 ≤ 𝑣 ) ) → ( 𝐴 [,] 𝑣 ) ⊆ ( ∪ 𝑤 ∪ 𝑉 ) )
86 69 5 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → 𝐴 ∈ ℝ )
87 69 34 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → 𝑅 ∈ ℝ )
88 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
89 86 87 88 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) ) )
90 89 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ) → ( 𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅 ) )
91 90 simp1d ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ) → 𝑡 ∈ ℝ )
92 91 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑡 ≤ 𝑣 ) ) → 𝑡 ∈ ℝ )
93 90 simp2d ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ) → 𝐴 ≤ 𝑡 )
94 93 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑡 ≤ 𝑣 ) ) → 𝐴 ≤ 𝑡 )
95 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑡 ≤ 𝑣 ) ) → 𝑡 ≤ 𝑣 )
96 69 17 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
97 simplr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → 𝑣 ∈ ( 𝐴 [,] 𝐵 ) )
98 96 97 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → 𝑣 ∈ ℝ )
99 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → ( 𝑡 ∈ ( 𝐴 [,] 𝑣 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣 ) ) )
100 86 98 99 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝑡 ∈ ( 𝐴 [,] 𝑣 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣 ) ) )
101 100 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑡 ≤ 𝑣 ) ) → ( 𝑡 ∈ ( 𝐴 [,] 𝑣 ) ↔ ( 𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣 ) ) )
102 92 94 95 101 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑡 ≤ 𝑣 ) ) → 𝑡 ∈ ( 𝐴 [,] 𝑣 ) )
103 85 102 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑡 ≤ 𝑣 ) ) → 𝑡 ∈ ( ∪ 𝑤 ∪ 𝑉 ) )
104 103 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ) → ( 𝑡 ≤ 𝑣 → 𝑡 ∈ ( ∪ 𝑤 ∪ 𝑉 ) ) )
105 69 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝜑 )
106 105 12 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → ( 𝐺 ( ball ‘ 𝐷 ) 𝐶 ) ⊆ 𝑉 )
107 91 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑡 ∈ ℝ )
108 105 53 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → ( 𝐺 − 𝐶 ) ∈ ℝ )
109 98 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑣 ∈ ℝ )
110 simplr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → ( 𝐺 − 𝐶 ) < 𝑣 )
111 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑣 < 𝑡 )
112 108 109 107 110 111 lttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → ( 𝐺 − 𝐶 ) < 𝑡 )
113 105 34 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑅 ∈ ℝ )
114 26 52 readdcld ⊢ ( 𝜑 → ( 𝐺 + 𝐶 ) ∈ ℝ )
115 105 114 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → ( 𝐺 + 𝐶 ) ∈ ℝ )
116 90 simp3d ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ) → 𝑡 ≤ 𝑅 )
117 116 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑡 ≤ 𝑅 )
118 min1 ⊢ ( ( ( 𝐺 + ( 𝐶 / 2 ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) ≤ ( 𝐺 + ( 𝐶 / 2 ) ) )
119 30 6 118 syl2anc ⊢ ( 𝜑 → if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) ≤ ( 𝐺 + ( 𝐶 / 2 ) ) )
120 14 119 eqbrtrid ⊢ ( 𝜑 → 𝑅 ≤ ( 𝐺 + ( 𝐶 / 2 ) ) )
121 rphalflt ⊢ ( 𝐶 ∈ ℝ+ → ( 𝐶 / 2 ) < 𝐶 )
122 11 121 syl ⊢ ( 𝜑 → ( 𝐶 / 2 ) < 𝐶 )
123 29 52 26 122 ltadd2dd ⊢ ( 𝜑 → ( 𝐺 + ( 𝐶 / 2 ) ) < ( 𝐺 + 𝐶 ) )
124 34 30 114 120 123 lelttrd ⊢ ( 𝜑 → 𝑅 < ( 𝐺 + 𝐶 ) )
125 105 124 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑅 < ( 𝐺 + 𝐶 ) )
126 107 113 115 117 125 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑡 < ( 𝐺 + 𝐶 ) )
127 rexr ⊢ ( ( 𝐺 − 𝐶 ) ∈ ℝ → ( 𝐺 − 𝐶 ) ∈ ℝ* )
128 rexr ⊢ ( ( 𝐺 + 𝐶 ) ∈ ℝ → ( 𝐺 + 𝐶 ) ∈ ℝ* )
129 elioo2 ⊢ ( ( ( 𝐺 − 𝐶 ) ∈ ℝ* ∧ ( 𝐺 + 𝐶 ) ∈ ℝ* ) → ( 𝑡 ∈ ( ( 𝐺 − 𝐶 ) (,) ( 𝐺 + 𝐶 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐺 − 𝐶 ) < 𝑡 ∧ 𝑡 < ( 𝐺 + 𝐶 ) ) ) )
130 127 128 129 syl2an ⊢ ( ( ( 𝐺 − 𝐶 ) ∈ ℝ ∧ ( 𝐺 + 𝐶 ) ∈ ℝ ) → ( 𝑡 ∈ ( ( 𝐺 − 𝐶 ) (,) ( 𝐺 + 𝐶 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐺 − 𝐶 ) < 𝑡 ∧ 𝑡 < ( 𝐺 + 𝐶 ) ) ) )
131 108 115 130 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → ( 𝑡 ∈ ( ( 𝐺 − 𝐶 ) (,) ( 𝐺 + 𝐶 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐺 − 𝐶 ) < 𝑡 ∧ 𝑡 < ( 𝐺 + 𝐶 ) ) ) )
132 107 112 126 131 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑡 ∈ ( ( 𝐺 − 𝐶 ) (,) ( 𝐺 + 𝐶 ) ) )
133 105 26 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝐺 ∈ ℝ )
134 105 11 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝐶 ∈ ℝ+ )
135 134 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝐶 ∈ ℝ )
136 3 bl2ioo ⊢ ( ( 𝐺 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐺 ( ball ‘ 𝐷 ) 𝐶 ) = ( ( 𝐺 − 𝐶 ) (,) ( 𝐺 + 𝐶 ) ) )
137 133 135 136 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → ( 𝐺 ( ball ‘ 𝐷 ) 𝐶 ) = ( ( 𝐺 − 𝐶 ) (,) ( 𝐺 + 𝐶 ) ) )
138 132 137 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑡 ∈ ( 𝐺 ( ball ‘ 𝐷 ) 𝐶 ) )
139 106 138 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑡 ∈ 𝑉 )
140 elun2 ⊢ ( 𝑡 ∈ 𝑉 → 𝑡 ∈ ( ∪ 𝑤 ∪ 𝑉 ) )
141 139 140 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ∧ 𝑣 < 𝑡 ) ) → 𝑡 ∈ ( ∪ 𝑤 ∪ 𝑉 ) )
142 141 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ) → ( 𝑣 < 𝑡 → 𝑡 ∈ ( ∪ 𝑤 ∪ 𝑉 ) ) )
143 98 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ) → 𝑣 ∈ ℝ )
144 lelttric ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → ( 𝑡 ≤ 𝑣 ∨ 𝑣 < 𝑡 ) )
145 91 143 144 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ) → ( 𝑡 ≤ 𝑣 ∨ 𝑣 < 𝑡 ) )
146 104 142 145 mpjaod ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) ∧ 𝑡 ∈ ( 𝐴 [,] 𝑅 ) ) → 𝑡 ∈ ( ∪ 𝑤 ∪ 𝑉 ) )
147 146 ex ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝑡 ∈ ( 𝐴 [,] 𝑅 ) → 𝑡 ∈ ( ∪ 𝑤 ∪ 𝑉 ) ) )
148 147 ssrdv ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝐴 [,] 𝑅 ) ⊆ ( ∪ 𝑤 ∪ 𝑉 ) )
149 uniun ⊢ ∪ ( 𝑤 ∪ { 𝑉 } ) = ( ∪ 𝑤 ∪ ∪ { 𝑉 } )
150 unisng ⊢ ( 𝑉 ∈ 𝑈 → ∪ { 𝑉 } = 𝑉 )
151 70 150 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ∪ { 𝑉 } = 𝑉 )
152 151 uneq2d ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( ∪ 𝑤 ∪ ∪ { 𝑉 } ) = ( ∪ 𝑤 ∪ 𝑉 ) )
153 149 152 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ∪ ( 𝑤 ∪ { 𝑉 } ) = ( ∪ 𝑤 ∪ 𝑉 ) )
154 148 153 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ( 𝐴 [,] 𝑅 ) ⊆ ∪ ( 𝑤 ∪ { 𝑉 } ) )
155 unieq ⊢ ( 𝑦 = ( 𝑤 ∪ { 𝑉 } ) → ∪ 𝑦 = ∪ ( 𝑤 ∪ { 𝑉 } ) )
156 155 sseq2d ⊢ ( 𝑦 = ( 𝑤 ∪ { 𝑉 } ) → ( ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 ↔ ( 𝐴 [,] 𝑅 ) ⊆ ∪ ( 𝑤 ∪ { 𝑉 } ) ) )
157 156 rspcev ⊢ ( ( ( 𝑤 ∪ { 𝑉 } ) ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑅 ) ⊆ ∪ ( 𝑤 ∪ { 𝑉 } ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 )
158 82 154 157 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 ∧ ( 𝐺 − 𝐶 ) < 𝑣 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 )
159 158 3exp2 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 → ( ( 𝐺 − 𝐶 ) < 𝑣 → ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 ) ) ) )
160 159 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∃ 𝑤 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑤 → ( ( 𝐺 − 𝐶 ) < 𝑣 → ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 ) ) )
161 63 160 biimtrid ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑧 → ( ( 𝐺 − 𝐶 ) < 𝑣 → ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 ) ) )
162 161 expimpd ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ∧ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑧 ) → ( ( 𝐺 − 𝐶 ) < 𝑣 → ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 ) ) )
163 60 162 biimtrid ⊢ ( 𝜑 → ( 𝑣 ∈ 𝑆 → ( ( 𝐺 − 𝐶 ) < 𝑣 → ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 ) ) )
164 163 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑆 ( 𝐺 − 𝐶 ) < 𝑣 → ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 ) )
165 56 164 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 )
166 oveq2 ⊢ ( 𝑣 = 𝑅 → ( 𝐴 [,] 𝑣 ) = ( 𝐴 [,] 𝑅 ) )
167 166 sseq1d ⊢ ( 𝑣 = 𝑅 → ( ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑦 ↔ ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 ) )
168 167 rexbidv ⊢ ( 𝑣 = 𝑅 → ( ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑦 ↔ ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 ) )
169 unieq ⊢ ( 𝑧 = 𝑦 → ∪ 𝑧 = ∪ 𝑦 )
170 169 sseq2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑧 ↔ ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑦 ) )
171 170 cbvrexvw ⊢ ( ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑧 ↔ ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑦 )
172 59 171 bitrdi ⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 ↔ ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑦 ) )
173 172 cbvrabv ⊢ { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 } = { 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑦 }
174 4 173 eqtri ⊢ 𝑆 = { 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑣 ) ⊆ ∪ 𝑦 }
175 168 174 elrab2 ⊢ ( 𝑅 ∈ 𝑆 ↔ ( 𝑅 ∈ ( 𝐴 [,] 𝐵 ) ∧ ∃ 𝑦 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑅 ) ⊆ ∪ 𝑦 ) )
176 49 165 175 sylanbrc ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
177 18 21 24 176 suprubd ⊢ ( 𝜑 → 𝑅 ≤ sup ( 𝑆 , ℝ , < ) )
178 177 13 breqtrrdi ⊢ ( 𝜑 → 𝑅 ≤ 𝐺 )
179 iftrue ⊢ ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 → if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) = ( 𝐺 + ( 𝐶 / 2 ) ) )
180 14 179 eqtrid ⊢ ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 → 𝑅 = ( 𝐺 + ( 𝐶 / 2 ) ) )
181 180 breq1d ⊢ ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 → ( 𝑅 ≤ 𝐺 ↔ ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐺 ) )
182 178 181 syl5ibcom ⊢ ( 𝜑 → ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 → ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐺 ) )
183 32 182 mtod ⊢ ( 𝜑 → ¬ ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 )
184 iffalse ⊢ ( ¬ ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 → if ( ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 , ( 𝐺 + ( 𝐶 / 2 ) ) , 𝐵 ) = 𝐵 )
185 14 184 eqtrid ⊢ ( ¬ ( 𝐺 + ( 𝐶 / 2 ) ) ≤ 𝐵 → 𝑅 = 𝐵 )
186 183 185 syl ⊢ ( 𝜑 → 𝑅 = 𝐵 )
187 186 176 eqeltrrd ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )