Metamath Proof Explorer

Theorem icccmplem2

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

Ref Expression
Hypotheses icccmp.1 
|- J = ( topGen ` ran (,) )
icccmp.2 
|- T = ( J |`t ( A [,] B ) )
icccmp.3 
|- D = ( ( abs o. - ) |` ( RR X. RR ) )
icccmp.4 
|- S = { x e. ( A [,] B ) | E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z }
icccmp.5 
|- ( ph -> A e. RR )
icccmp.6 
|- ( ph -> B e. RR )
icccmp.7 
|- ( ph -> A <_ B )
icccmp.8 
|- ( ph -> U C_ J )
icccmp.9 
|- ( ph -> ( A [,] B ) C_ U. U )
icccmp.10 
|- ( ph -> V e. U )
icccmp.11 
|- ( ph -> C e. RR+ )
icccmp.12 
|- ( ph -> ( G ( ball ` D ) C ) C_ V )
icccmp.13 
|- G = sup ( S , RR , < )
icccmp.14 
|- R = if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B )
Assertion icccmplem2 
|- ( ph -> B e. S )

Proof

Step Hyp Ref Expression
1 icccmp.1 
 |-  J = ( topGen ` ran (,) )
2 icccmp.2 
 |-  T = ( J |`t ( A [,] B ) )
3 icccmp.3 
 |-  D = ( ( abs o. - ) |` ( RR X. RR ) )
4 icccmp.4 
 |-  S = { x e. ( A [,] B ) | E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z }
5 icccmp.5 
 |-  ( ph -> A e. RR )
6 icccmp.6 
 |-  ( ph -> B e. RR )
7 icccmp.7 
 |-  ( ph -> A <_ B )
8 icccmp.8 
 |-  ( ph -> U C_ J )
9 icccmp.9 
 |-  ( ph -> ( A [,] B ) C_ U. U )
10 icccmp.10 
 |-  ( ph -> V e. U )
11 icccmp.11 
 |-  ( ph -> C e. RR+ )
12 icccmp.12 
 |-  ( ph -> ( G ( ball ` D ) C ) C_ V )
13 icccmp.13 
 |-  G = sup ( S , RR , < )
14 icccmp.14 
 |-  R = if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B )
15 4 ssrab3 
 |-  S C_ ( A [,] B )
16 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
17 5 6 16 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
18 15 17 sstrid 
 |-  ( ph -> S C_ RR )
19 1 2 3 4 5 6 7 8 9 icccmplem1 
 |-  ( ph -> ( A e. S /\ A. y e. S y <_ B ) )
20 19 simpld 
 |-  ( ph -> A e. S )
21 20 ne0d 
 |-  ( ph -> S =/= (/) )
22 19 simprd 
 |-  ( ph -> A. y e. S y <_ B )
23 brralrspcev 
 |-  ( ( B e. RR /\ A. y e. S y <_ B ) -> E. n e. RR A. y e. S y <_ n )
24 6 22 23 syl2anc 
 |-  ( ph -> E. n e. RR A. y e. S y <_ n )
25 18 21 24 suprcld 
 |-  ( ph -> sup ( S , RR , < ) e. RR )
26 13 25 eqeltrid 
 |-  ( ph -> G e. RR )
27 11 rphalfcld 
 |-  ( ph -> ( C / 2 ) e. RR+ )
28 26 27 ltaddrpd 
 |-  ( ph -> G < ( G + ( C / 2 ) ) )
29 27 rpred 
 |-  ( ph -> ( C / 2 ) e. RR )
30 26 29 readdcld 
 |-  ( ph -> ( G + ( C / 2 ) ) e. RR )
31 26 30 ltnled 
 |-  ( ph -> ( G < ( G + ( C / 2 ) ) <-> -. ( G + ( C / 2 ) ) <_ G ) )
32 28 31 mpbid 
 |-  ( ph -> -. ( G + ( C / 2 ) ) <_ G )
33 30 6 ifcld 
 |-  ( ph -> if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) e. RR )
34 14 33 eqeltrid 
 |-  ( ph -> R e. RR )
35 18 21 24 20 suprubd 
 |-  ( ph -> A <_ sup ( S , RR , < ) )
36 35 13 breqtrrdi 
 |-  ( ph -> A <_ G )
37 26 30 28 ltled 
 |-  ( ph -> G <_ ( G + ( C / 2 ) ) )
38 5 26 30 36 37 letrd 
 |-  ( ph -> A <_ ( G + ( C / 2 ) ) )
39 breq2 
 |-  ( ( G + ( C / 2 ) ) = if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) -> ( A <_ ( G + ( C / 2 ) ) <-> A <_ if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) ) )
40 breq2 
 |-  ( B = if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) -> ( A <_ B <-> A <_ if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) ) )
41 39 40 ifboth 
 |-  ( ( A <_ ( G + ( C / 2 ) ) /\ A <_ B ) -> A <_ if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) )
42 38 7 41 syl2anc 
 |-  ( ph -> A <_ if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) )
43 42 14 breqtrrdi 
 |-  ( ph -> A <_ R )
44 min2 
 |-  ( ( ( G + ( C / 2 ) ) e. RR /\ B e. RR ) -> if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) <_ B )
45 30 6 44 syl2anc 
 |-  ( ph -> if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) <_ B )
46 14 45 eqbrtrid 
 |-  ( ph -> R <_ B )
47 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( R e. ( A [,] B ) <-> ( R e. RR /\ A <_ R /\ R <_ B ) ) )
48 5 6 47 syl2anc 
 |-  ( ph -> ( R e. ( A [,] B ) <-> ( R e. RR /\ A <_ R /\ R <_ B ) ) )
49 34 43 46 48 mpbir3and 
 |-  ( ph -> R e. ( A [,] B ) )
50 26 11 ltsubrpd 
 |-  ( ph -> ( G - C ) < G )
51 50 13 breqtrdi 
 |-  ( ph -> ( G - C ) < sup ( S , RR , < ) )
52 11 rpred 
 |-  ( ph -> C e. RR )
53 26 52 resubcld 
 |-  ( ph -> ( G - C ) e. RR )
54 suprlub 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. n e. RR A. y e. S y <_ n ) /\ ( G - C ) e. RR ) -> ( ( G - C ) < sup ( S , RR , < ) <-> E. v e. S ( G - C ) < v ) )
55 18 21 24 53 54 syl31anc 
 |-  ( ph -> ( ( G - C ) < sup ( S , RR , < ) <-> E. v e. S ( G - C ) < v ) )
56 51 55 mpbid 
 |-  ( ph -> E. v e. S ( G - C ) < v )
57 oveq2 
 |-  ( x = v -> ( A [,] x ) = ( A [,] v ) )
58 57 sseq1d 
 |-  ( x = v -> ( ( A [,] x ) C_ U. z <-> ( A [,] v ) C_ U. z ) )
59 58 rexbidv 
 |-  ( x = v -> ( E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z <-> E. z e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. z ) )
60 59 4 elrab2 
 |-  ( v e. S <-> ( v e. ( A [,] B ) /\ E. z e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. z ) )
61 unieq 
 |-  ( z = w -> U. z = U. w )
62 61 sseq2d 
 |-  ( z = w -> ( ( A [,] v ) C_ U. z <-> ( A [,] v ) C_ U. w ) )
63 62 cbvrexvw 
 |-  ( E. z e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. z <-> E. w e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. w )
64 simpr1 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> w e. ( ~P U i^i Fin ) )
65 elin 
 |-  ( w e. ( ~P U i^i Fin ) <-> ( w e. ~P U /\ w e. Fin ) )
66 64 65 sylib 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( w e. ~P U /\ w e. Fin ) )
67 66 simpld 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> w e. ~P U )
68 67 elpwid 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> w C_ U )
69 simpll 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ph )
70 69 10 syl 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> V e. U )
71 70 snssd 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> { V } C_ U )
72 68 71 unssd 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( w u. { V } ) C_ U )
73 vex 
 |-  w e. _V
74 snex 
 |-  { V } e. _V
75 73 74 unex 
 |-  ( w u. { V } ) e. _V
76 75 elpw 
 |-  ( ( w u. { V } ) e. ~P U <-> ( w u. { V } ) C_ U )
77 72 76 sylibr 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( w u. { V } ) e. ~P U )
78 66 simprd 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> w e. Fin )
79 snfi 
 |-  { V } e. Fin
80 unfi 
 |-  ( ( w e. Fin /\ { V } e. Fin ) -> ( w u. { V } ) e. Fin )
81 78 79 80 sylancl 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( w u. { V } ) e. Fin )
82 77 81 elind 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( w u. { V } ) e. ( ~P U i^i Fin ) )
83 simplr2 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ t <_ v ) ) -> ( A [,] v ) C_ U. w )
84 ssun1 
 |-  U. w C_ ( U. w u. V )
85 83 84 sstrdi 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ t <_ v ) ) -> ( A [,] v ) C_ ( U. w u. V ) )
86 69 5 syl 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> A e. RR )
87 69 34 syl 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> R e. RR )
88 elicc2 
 |-  ( ( A e. RR /\ R e. RR ) -> ( t e. ( A [,] R ) <-> ( t e. RR /\ A <_ t /\ t <_ R ) ) )
89 86 87 88 syl2anc 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( t e. ( A [,] R ) <-> ( t e. RR /\ A <_ t /\ t <_ R ) ) )
90 89 biimpa 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ t e. ( A [,] R ) ) -> ( t e. RR /\ A <_ t /\ t <_ R ) )
91 90 simp1d 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ t e. ( A [,] R ) ) -> t e. RR )
92 91 adantrr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ t <_ v ) ) -> t e. RR )
93 90 simp2d 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ t e. ( A [,] R ) ) -> A <_ t )
94 93 adantrr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ t <_ v ) ) -> A <_ t )
95 simprr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ t <_ v ) ) -> t <_ v )
96 69 17 syl 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( A [,] B ) C_ RR )
97 simplr 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> v e. ( A [,] B ) )
98 96 97 sseldd 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> v e. RR )
99 elicc2 
 |-  ( ( A e. RR /\ v e. RR ) -> ( t e. ( A [,] v ) <-> ( t e. RR /\ A <_ t /\ t <_ v ) ) )
100 86 98 99 syl2anc 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( t e. ( A [,] v ) <-> ( t e. RR /\ A <_ t /\ t <_ v ) ) )
101 100 adantr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ t <_ v ) ) -> ( t e. ( A [,] v ) <-> ( t e. RR /\ A <_ t /\ t <_ v ) ) )
102 92 94 95 101 mpbir3and 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ t <_ v ) ) -> t e. ( A [,] v ) )
103 85 102 sseldd 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ t <_ v ) ) -> t e. ( U. w u. V ) )
104 103 expr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ t e. ( A [,] R ) ) -> ( t <_ v -> t e. ( U. w u. V ) ) )
105 69 adantr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> ph )
106 105 12 syl 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> ( G ( ball ` D ) C ) C_ V )
107 91 adantrr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> t e. RR )
108 105 53 syl 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> ( G - C ) e. RR )
109 98 adantr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> v e. RR )
110 simplr3 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> ( G - C ) < v )
111 simprr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> v < t )
112 108 109 107 110 111 lttrd 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> ( G - C ) < t )
113 105 34 syl 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> R e. RR )
114 26 52 readdcld 
 |-  ( ph -> ( G + C ) e. RR )
115 105 114 syl 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> ( G + C ) e. RR )
116 90 simp3d 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ t e. ( A [,] R ) ) -> t <_ R )
117 116 adantrr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> t <_ R )
118 min1 
 |-  ( ( ( G + ( C / 2 ) ) e. RR /\ B e. RR ) -> if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) <_ ( G + ( C / 2 ) ) )
119 30 6 118 syl2anc 
 |-  ( ph -> if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) <_ ( G + ( C / 2 ) ) )
120 14 119 eqbrtrid 
 |-  ( ph -> R <_ ( G + ( C / 2 ) ) )
121 rphalflt 
 |-  ( C e. RR+ -> ( C / 2 ) < C )
122 11 121 syl 
 |-  ( ph -> ( C / 2 ) < C )
123 29 52 26 122 ltadd2dd 
 |-  ( ph -> ( G + ( C / 2 ) ) < ( G + C ) )
124 34 30 114 120 123 lelttrd 
 |-  ( ph -> R < ( G + C ) )
125 105 124 syl 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> R < ( G + C ) )
126 107 113 115 117 125 lelttrd 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> t < ( G + C ) )
127 rexr 
 |-  ( ( G - C ) e. RR -> ( G - C ) e. RR* )
128 rexr 
 |-  ( ( G + C ) e. RR -> ( G + C ) e. RR* )
129 elioo2 
 |-  ( ( ( G - C ) e. RR* /\ ( G + C ) e. RR* ) -> ( t e. ( ( G - C ) (,) ( G + C ) ) <-> ( t e. RR /\ ( G - C ) < t /\ t < ( G + C ) ) ) )
130 127 128 129 syl2an 
 |-  ( ( ( G - C ) e. RR /\ ( G + C ) e. RR ) -> ( t e. ( ( G - C ) (,) ( G + C ) ) <-> ( t e. RR /\ ( G - C ) < t /\ t < ( G + C ) ) ) )
131 108 115 130 syl2anc 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> ( t e. ( ( G - C ) (,) ( G + C ) ) <-> ( t e. RR /\ ( G - C ) < t /\ t < ( G + C ) ) ) )
132 107 112 126 131 mpbir3and 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> t e. ( ( G - C ) (,) ( G + C ) ) )
133 105 26 syl 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> G e. RR )
134 105 11 syl 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> C e. RR+ )
135 134 rpred 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> C e. RR )
136 3 bl2ioo 
 |-  ( ( G e. RR /\ C e. RR ) -> ( G ( ball ` D ) C ) = ( ( G - C ) (,) ( G + C ) ) )
137 133 135 136 syl2anc 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> ( G ( ball ` D ) C ) = ( ( G - C ) (,) ( G + C ) ) )
138 132 137 eleqtrrd 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> t e. ( G ( ball ` D ) C ) )
139 106 138 sseldd 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> t e. V )
140 elun2 
 |-  ( t e. V -> t e. ( U. w u. V ) )
141 139 140 syl 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ ( t e. ( A [,] R ) /\ v < t ) ) -> t e. ( U. w u. V ) )
142 141 expr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ t e. ( A [,] R ) ) -> ( v < t -> t e. ( U. w u. V ) ) )
143 98 adantr 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ t e. ( A [,] R ) ) -> v e. RR )
144 lelttric 
 |-  ( ( t e. RR /\ v e. RR ) -> ( t <_ v \/ v < t ) )
145 91 143 144 syl2anc 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ t e. ( A [,] R ) ) -> ( t <_ v \/ v < t ) )
146 104 142 145 mpjaod 
 |-  ( ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) /\ t e. ( A [,] R ) ) -> t e. ( U. w u. V ) )
147 146 ex 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( t e. ( A [,] R ) -> t e. ( U. w u. V ) ) )
148 147 ssrdv 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( A [,] R ) C_ ( U. w u. V ) )
149 uniun 
 |-  U. ( w u. { V } ) = ( U. w u. U. { V } )
150 unisng 
 |-  ( V e. U -> U. { V } = V )
151 70 150 syl 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> U. { V } = V )
152 151 uneq2d 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( U. w u. U. { V } ) = ( U. w u. V ) )
153 149 152 syl5eq 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> U. ( w u. { V } ) = ( U. w u. V ) )
154 148 153 sseqtrrd 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> ( A [,] R ) C_ U. ( w u. { V } ) )
155 unieq 
 |-  ( y = ( w u. { V } ) -> U. y = U. ( w u. { V } ) )
156 155 sseq2d 
 |-  ( y = ( w u. { V } ) -> ( ( A [,] R ) C_ U. y <-> ( A [,] R ) C_ U. ( w u. { V } ) ) )
157 156 rspcev 
 |-  ( ( ( w u. { V } ) e. ( ~P U i^i Fin ) /\ ( A [,] R ) C_ U. ( w u. { V } ) ) -> E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y )
158 82 154 157 syl2anc 
 |-  ( ( ( ph /\ v e. ( A [,] B ) ) /\ ( w e. ( ~P U i^i Fin ) /\ ( A [,] v ) C_ U. w /\ ( G - C ) < v ) ) -> E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y )
159 158 3exp2 
 |-  ( ( ph /\ v e. ( A [,] B ) ) -> ( w e. ( ~P U i^i Fin ) -> ( ( A [,] v ) C_ U. w -> ( ( G - C ) < v -> E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y ) ) ) )
160 159 rexlimdv 
 |-  ( ( ph /\ v e. ( A [,] B ) ) -> ( E. w e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. w -> ( ( G - C ) < v -> E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y ) ) )
161 63 160 syl5bi 
 |-  ( ( ph /\ v e. ( A [,] B ) ) -> ( E. z e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. z -> ( ( G - C ) < v -> E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y ) ) )
162 161 expimpd 
 |-  ( ph -> ( ( v e. ( A [,] B ) /\ E. z e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. z ) -> ( ( G - C ) < v -> E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y ) ) )
163 60 162 syl5bi 
 |-  ( ph -> ( v e. S -> ( ( G - C ) < v -> E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y ) ) )
164 163 rexlimdv 
 |-  ( ph -> ( E. v e. S ( G - C ) < v -> E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y ) )
165 56 164 mpd 
 |-  ( ph -> E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y )
166 oveq2 
 |-  ( v = R -> ( A [,] v ) = ( A [,] R ) )
167 166 sseq1d 
 |-  ( v = R -> ( ( A [,] v ) C_ U. y <-> ( A [,] R ) C_ U. y ) )
168 167 rexbidv 
 |-  ( v = R -> ( E. y e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. y <-> E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y ) )
169 unieq 
 |-  ( z = y -> U. z = U. y )
170 169 sseq2d 
 |-  ( z = y -> ( ( A [,] v ) C_ U. z <-> ( A [,] v ) C_ U. y ) )
171 170 cbvrexvw 
 |-  ( E. z e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. z <-> E. y e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. y )
172 59 171 bitrdi 
 |-  ( x = v -> ( E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z <-> E. y e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. y ) )
173 172 cbvrabv 
 |-  { x e. ( A [,] B ) | E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z } = { v e. ( A [,] B ) | E. y e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. y }
174 4 173 eqtri 
 |-  S = { v e. ( A [,] B ) | E. y e. ( ~P U i^i Fin ) ( A [,] v ) C_ U. y }
175 168 174 elrab2 
 |-  ( R e. S <-> ( R e. ( A [,] B ) /\ E. y e. ( ~P U i^i Fin ) ( A [,] R ) C_ U. y ) )
176 49 165 175 sylanbrc 
 |-  ( ph -> R e. S )
177 18 21 24 176 suprubd 
 |-  ( ph -> R <_ sup ( S , RR , < ) )
178 177 13 breqtrrdi 
 |-  ( ph -> R <_ G )
179 iftrue 
 |-  ( ( G + ( C / 2 ) ) <_ B -> if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) = ( G + ( C / 2 ) ) )
180 14 179 syl5eq 
 |-  ( ( G + ( C / 2 ) ) <_ B -> R = ( G + ( C / 2 ) ) )
181 180 breq1d 
 |-  ( ( G + ( C / 2 ) ) <_ B -> ( R <_ G <-> ( G + ( C / 2 ) ) <_ G ) )
182 178 181 syl5ibcom 
 |-  ( ph -> ( ( G + ( C / 2 ) ) <_ B -> ( G + ( C / 2 ) ) <_ G ) )
183 32 182 mtod 
 |-  ( ph -> -. ( G + ( C / 2 ) ) <_ B )
184 iffalse 
 |-  ( -. ( G + ( C / 2 ) ) <_ B -> if ( ( G + ( C / 2 ) ) <_ B , ( G + ( C / 2 ) ) , B ) = B )
185 14 184 syl5eq 
 |-  ( -. ( G + ( C / 2 ) ) <_ B -> R = B )
186 183 185 syl 
 |-  ( ph -> R = B )
187 186 176 eqeltrrd 
 |-  ( ph -> B e. S )