MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  icccmplem2 Structured version   Unicode version

Theorem icccmplem2 21454
Description: Lemma for icccmp 21456. (Contributed by Mario Carneiro, 13-Jun-2014.)
Hypotheses
Ref Expression
icccmp.1  |-  J  =  ( topGen `  ran  (,) )
icccmp.2  |-  T  =  ( Jt  ( 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
Ref Expression
icccmplem2  |-  ( ph  ->  B  e.  S )
Distinct variable groups:    x, z, B    x, A, z    x, D    x, T, z    z, J    x, U, z
Allowed substitution hints:    ph( x, z)    C( x, z)    D( z)    R( x, z)    S( x, z)    G( x, z)    J( x)    V( x, z)

Proof of Theorem icccmplem2
Dummy variables  t  n  v  w  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 icccmp.13 . . . . . . 7  |-  G  =  sup ( S ,  RR ,  <  )
2 icccmp.4 . . . . . . . . . 10  |-  S  =  { x  e.  ( A [,] B )  |  E. z  e.  ( ~P U  i^i  Fin ) ( A [,] x )  C_  U. z }
3 ssrab2 3581 . . . . . . . . . 10  |-  { x  e.  ( A [,] B
)  |  E. z  e.  ( ~P U  i^i  Fin ) ( A [,] x )  C_  U. z }  C_  ( A [,] B )
42, 3eqsstri 3529 . . . . . . . . 9  |-  S  C_  ( A [,] B )
5 icccmp.5 . . . . . . . . . 10  |-  ( ph  ->  A  e.  RR )
6 icccmp.6 . . . . . . . . . 10  |-  ( ph  ->  B  e.  RR )
7 iccssre 11631 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
85, 6, 7syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( A [,] B
)  C_  RR )
94, 8syl5ss 3510 . . . . . . . 8  |-  ( ph  ->  S  C_  RR )
10 icccmp.1 . . . . . . . . . . 11  |-  J  =  ( topGen `  ran  (,) )
11 icccmp.2 . . . . . . . . . . 11  |-  T  =  ( Jt  ( A [,] B ) )
12 icccmp.3 . . . . . . . . . . 11  |-  D  =  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) )
13 icccmp.7 . . . . . . . . . . 11  |-  ( ph  ->  A  <_  B )
14 icccmp.8 . . . . . . . . . . 11  |-  ( ph  ->  U  C_  J )
15 icccmp.9 . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  U. U )
1610, 11, 12, 2, 5, 6, 13, 14, 15icccmplem1 21453 . . . . . . . . . 10  |-  ( ph  ->  ( A  e.  S  /\  A. y  e.  S  y  <_  B ) )
1716simpld 459 . . . . . . . . 9  |-  ( ph  ->  A  e.  S )
18 ne0i 3799 . . . . . . . . 9  |-  ( A  e.  S  ->  S  =/=  (/) )
1917, 18syl 16 . . . . . . . 8  |-  ( ph  ->  S  =/=  (/) )
2016simprd 463 . . . . . . . . 9  |-  ( ph  ->  A. y  e.  S  y  <_  B )
21 breq2 4460 . . . . . . . . . . 11  |-  ( n  =  B  ->  (
y  <_  n  <->  y  <_  B ) )
2221ralbidv 2896 . . . . . . . . . 10  |-  ( n  =  B  ->  ( A. y  e.  S  y  <_  n  <->  A. y  e.  S  y  <_  B ) )
2322rspcev 3210 . . . . . . . . 9  |-  ( ( B  e.  RR  /\  A. y  e.  S  y  <_  B )  ->  E. n  e.  RR  A. y  e.  S  y  <_  n )
246, 20, 23syl2anc 661 . . . . . . . 8  |-  ( ph  ->  E. n  e.  RR  A. y  e.  S  y  <_  n )
25 suprcl 10523 . . . . . . . 8  |-  ( ( S  C_  RR  /\  S  =/=  (/)  /\  E. n  e.  RR  A. y  e.  S  y  <_  n
)  ->  sup ( S ,  RR ,  <  )  e.  RR )
269, 19, 24, 25syl3anc 1228 . . . . . . 7  |-  ( ph  ->  sup ( S ,  RR ,  <  )  e.  RR )
271, 26syl5eqel 2549 . . . . . 6  |-  ( ph  ->  G  e.  RR )
28 icccmp.11 . . . . . . 7  |-  ( ph  ->  C  e.  RR+ )
2928rphalfcld 11293 . . . . . 6  |-  ( ph  ->  ( C  /  2
)  e.  RR+ )
3027, 29ltaddrpd 11310 . . . . 5  |-  ( ph  ->  G  <  ( G  +  ( C  / 
2 ) ) )
3129rpred 11281 . . . . . . 7  |-  ( ph  ->  ( C  /  2
)  e.  RR )
3227, 31readdcld 9640 . . . . . 6  |-  ( ph  ->  ( G  +  ( C  /  2 ) )  e.  RR )
3327, 32ltnled 9749 . . . . 5  |-  ( ph  ->  ( G  <  ( G  +  ( C  /  2 ) )  <->  -.  ( G  +  ( C  /  2 ) )  <_  G )
)
3430, 33mpbid 210 . . . 4  |-  ( ph  ->  -.  ( G  +  ( C  /  2
) )  <_  G
)
35 icccmp.14 . . . . . . . . . 10  |-  R  =  if ( ( G  +  ( C  / 
2 ) )  <_  B ,  ( G  +  ( C  / 
2 ) ) ,  B )
3632, 6ifcld 3987 . . . . . . . . . 10  |-  ( ph  ->  if ( ( G  +  ( C  / 
2 ) )  <_  B ,  ( G  +  ( C  / 
2 ) ) ,  B )  e.  RR )
3735, 36syl5eqel 2549 . . . . . . . . 9  |-  ( ph  ->  R  e.  RR )
38 suprub 10524 . . . . . . . . . . . . . 14  |-  ( ( ( S  C_  RR  /\  S  =/=  (/)  /\  E. n  e.  RR  A. y  e.  S  y  <_  n )  /\  A  e.  S )  ->  A  <_  sup ( S ,  RR ,  <  ) )
399, 19, 24, 17, 38syl31anc 1231 . . . . . . . . . . . . 13  |-  ( ph  ->  A  <_  sup ( S ,  RR ,  <  ) )
4039, 1syl6breqr 4496 . . . . . . . . . . . 12  |-  ( ph  ->  A  <_  G )
4127, 32, 30ltled 9750 . . . . . . . . . . . 12  |-  ( ph  ->  G  <_  ( G  +  ( C  / 
2 ) ) )
425, 27, 32, 40, 41letrd 9756 . . . . . . . . . . 11  |-  ( ph  ->  A  <_  ( G  +  ( C  / 
2 ) ) )
43 breq2 4460 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
44 breq2 4460 . . . . . . . . . . . 12  |-  ( B  =  if ( ( G  +  ( C  /  2 ) )  <_  B ,  ( G  +  ( C  /  2 ) ) ,  B )  -> 
( A  <_  B  <->  A  <_  if ( ( G  +  ( C  /  2 ) )  <_  B ,  ( G  +  ( C  /  2 ) ) ,  B ) ) )
4543, 44ifboth 3980 . . . . . . . . . . 11  |-  ( ( A  <_  ( G  +  ( C  / 
2 ) )  /\  A  <_  B )  ->  A  <_  if ( ( G  +  ( C  /  2 ) )  <_  B ,  ( G  +  ( C  /  2 ) ) ,  B ) )
4642, 13, 45syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  A  <_  if (
( G  +  ( C  /  2 ) )  <_  B , 
( G  +  ( C  /  2 ) ) ,  B ) )
4746, 35syl6breqr 4496 . . . . . . . . 9  |-  ( ph  ->  A  <_  R )
48 min2 11415 . . . . . . . . . . 11  |-  ( ( ( G  +  ( C  /  2 ) )  e.  RR  /\  B  e.  RR )  ->  if ( ( G  +  ( C  / 
2 ) )  <_  B ,  ( G  +  ( C  / 
2 ) ) ,  B )  <_  B
)
4932, 6, 48syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  if ( ( G  +  ( C  / 
2 ) )  <_  B ,  ( G  +  ( C  / 
2 ) ) ,  B )  <_  B
)
5035, 49syl5eqbr 4489 . . . . . . . . 9  |-  ( ph  ->  R  <_  B )
51 elicc2 11614 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( R  e.  ( A [,] B )  <-> 
( R  e.  RR  /\  A  <_  R  /\  R  <_  B ) ) )
525, 6, 51syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( R  e.  ( A [,] B )  <-> 
( R  e.  RR  /\  A  <_  R  /\  R  <_  B ) ) )
5337, 47, 50, 52mpbir3and 1179 . . . . . . . 8  |-  ( ph  ->  R  e.  ( A [,] B ) )
5427, 28ltsubrpd 11309 . . . . . . . . . . 11  |-  ( ph  ->  ( G  -  C
)  <  G )
5554, 1syl6breq 4495 . . . . . . . . . 10  |-  ( ph  ->  ( G  -  C
)  <  sup ( S ,  RR ,  <  ) )
5628rpred 11281 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  RR )
5727, 56resubcld 10008 . . . . . . . . . . 11  |-  ( ph  ->  ( G  -  C
)  e.  RR )
58 suprlub 10525 . . . . . . . . . . 11  |-  ( ( ( 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 )
)
599, 19, 24, 57, 58syl31anc 1231 . . . . . . . . . 10  |-  ( ph  ->  ( ( G  -  C )  <  sup ( S ,  RR ,  <  )  <->  E. v  e.  S  ( G  -  C
)  <  v )
)
6055, 59mpbid 210 . . . . . . . . 9  |-  ( ph  ->  E. v  e.  S  ( G  -  C
)  <  v )
61 oveq2 6304 . . . . . . . . . . . . . 14  |-  ( x  =  v  ->  ( A [,] x )  =  ( A [,] v
) )
6261sseq1d 3526 . . . . . . . . . . . . 13  |-  ( x  =  v  ->  (
( A [,] x
)  C_  U. z  <->  ( A [,] v ) 
C_  U. z ) )
6362rexbidv 2968 . . . . . . . . . . . 12  |-  ( 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
) )
6463, 2elrab2 3259 . . . . . . . . . . 11  |-  ( v  e.  S  <->  ( v  e.  ( A [,] B
)  /\  E. z  e.  ( ~P U  i^i  Fin ) ( A [,] v )  C_  U. z
) )
65 unieq 4259 . . . . . . . . . . . . . . 15  |-  ( z  =  w  ->  U. z  =  U. w )
6665sseq2d 3527 . . . . . . . . . . . . . 14  |-  ( z  =  w  ->  (
( A [,] v
)  C_  U. z  <->  ( A [,] v ) 
C_  U. w ) )
6766cbvrexv 3085 . . . . . . . . . . . . 13  |-  ( 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
)
68 simpr1 1002 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) )
69 elin 3683 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  ( ~P U  i^i  Fin )  <->  ( w  e.  ~P U  /\  w  e.  Fin ) )
7068, 69sylib 196 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 ) )
7170simpld 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  w  e.  ~P U )
7271elpwid 4025 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  w  C_  U
)
73 simpll 753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  ph )
74 icccmp.10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  V  e.  U )
7573, 74syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  V  e.  U )
7675snssd 4177 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  { V }  C_  U )
7772, 76unssd 3676 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
78 vex 3112 . . . . . . . . . . . . . . . . . . . 20  |-  w  e. 
_V
79 snex 4697 . . . . . . . . . . . . . . . . . . . 20  |-  { V }  e.  _V
8078, 79unex 6597 . . . . . . . . . . . . . . . . . . 19  |-  ( w  u.  { V }
)  e.  _V
8180elpw 4021 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  u.  { V } )  e.  ~P U 
<->  ( w  u.  { V } )  C_  U
)
8277, 81sylibr 212 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
8370simprd 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  w  e.  Fin )
84 snfi 7615 . . . . . . . . . . . . . . . . . 18  |-  { V }  e.  Fin
85 unfi 7805 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  e.  Fin  /\  { V }  e.  Fin )  ->  ( w  u. 
{ V } )  e.  Fin )
8683, 84, 85sylancl 662 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
8782, 86elind 3684 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) )
88 simplr2 1039 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 )
89 ssun1 3663 . . . . . . . . . . . . . . . . . . . . . . 23  |-  U. w  C_  ( U. w  u.  V )
9088, 89syl6ss 3511 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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
) )
9173, 5syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  A  e.  RR )
9273, 37syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  R  e.  RR )
93 elicc2 11614 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( A  e.  RR  /\  R  e.  RR )  ->  ( t  e.  ( A [,] R )  <-> 
( t  e.  RR  /\  A  <_  t  /\  t  <_  R ) ) )
9491, 92, 93syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 ) ) )
9594biimpa 484 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) )
9695simp1d 1008 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )
9796adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 )
9895simp2d 1009 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )
9998adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 )
100 simprr 757 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 )
10173, 8syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  ( A [,] B )  C_  RR )
102 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  v  e.  ( A [,] B ) )
103101, 102sseldd 3500 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  v  e.  RR )
104 elicc2 11614 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  e.  RR  /\  v  e.  RR )  ->  ( t  e.  ( A [,] v )  <-> 
( t  e.  RR  /\  A  <_  t  /\  t  <_  v ) ) )
10591, 103, 104syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) ) )
106105adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) ) )
10797, 99, 100, 106mpbir3and 1179 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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
) )
10890, 107sseldd 3500 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 ) )
109108expr 615 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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
) ) )
11073adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )
111 icccmp.12 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( G ( ball `  D ) C ) 
C_  V )
112110, 111syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 )
11396adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 )
114110, 57syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
115103adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
116 simplr3 1040 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
117 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
118114, 115, 113, 116, 117lttrd 9760 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 )
119110, 37syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
12027, 56readdcld 9640 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( G  +  C
)  e.  RR )
121110, 120syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
12295simp3d 1010 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 )
123122adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
124 min1 11414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( G  +  ( C  /  2 ) )  e.  RR  /\  B  e.  RR )  ->  if ( ( G  +  ( C  / 
2 ) )  <_  B ,  ( G  +  ( C  / 
2 ) ) ,  B )  <_  ( G  +  ( C  /  2 ) ) )
12532, 6, 124syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  if ( ( G  +  ( C  / 
2 ) )  <_  B ,  ( G  +  ( C  / 
2 ) ) ,  B )  <_  ( G  +  ( C  /  2 ) ) )
12635, 125syl5eqbr 4489 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  R  <_  ( G  +  ( C  / 
2 ) ) )
127 rphalflt 11271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( C  e.  RR+  ->  ( C  /  2 )  < 
C )
12828, 127syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( C  /  2
)  <  C )
12931, 56, 27, 128ltadd2dd 9758 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( G  +  ( C  /  2 ) )  <  ( G  +  C ) )
13037, 32, 120, 126, 129lelttrd 9757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  R  <  ( G  +  C ) )
131110, 130syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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
) )
132113, 119, 121, 123, 131lelttrd 9757 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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
) )
133 rexr 9656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( G  -  C )  e.  RR  ->  ( G  -  C )  e.  RR* )
134 rexr 9656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( G  +  C )  e.  RR  ->  ( G  +  C )  e.  RR* )
135 elioo2 11595 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( G  -  C
)  e.  RR*  /\  ( G  +  C )  e.  RR* )  ->  (
t  e.  ( ( G  -  C ) (,) ( G  +  C ) )  <->  ( t  e.  RR  /\  ( G  -  C )  < 
t  /\  t  <  ( G  +  C ) ) ) )
136133, 134, 135syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( G  -  C
)  e.  RR  /\  ( G  +  C
)  e.  RR )  ->  ( t  e.  ( ( G  -  C ) (,) ( G  +  C )
)  <->  ( t  e.  RR  /\  ( G  -  C )  < 
t  /\  t  <  ( G  +  C ) ) ) )
137114, 121, 136syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) ) ) )
138113, 118, 132, 137mpbir3and 1179 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )
) )
139110, 27syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 )
140110, 28syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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+ )
141140rpred 11281 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 )
14212bl2ioo 21423 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( G  e.  RR  /\  C  e.  RR )  ->  ( G ( ball `  D ) C )  =  ( ( G  -  C ) (,) ( G  +  C
) ) )
143139, 141, 142syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )
) )
144138, 143eleqtrrd 2548 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) )
145112, 144sseldd 3500 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 )
146 elun2 3668 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  e.  V  ->  t  e.  ( U. w  u.  V ) )
147145, 146syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 ) )
148147expr 615 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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
) ) )
149103adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 )
150 lelttric 9708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( t  e.  RR  /\  v  e.  RR )  ->  ( t  <_  v  \/  v  <  t ) )
15196, 149, 150syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) )
152109, 148, 151mpjaod 381 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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
) )
153152ex 434 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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
) ) )
154153ssrdv 3505 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 uniun 4270 . . . . . . . . . . . . . . . . . 18  |-  U. (
w  u.  { V } )  =  ( U. w  u.  U. { V } )
156 unisng 4267 . . . . . . . . . . . . . . . . . . . 20  |-  ( V  e.  U  ->  U. { V }  =  V
)
15775, 156syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  v  e.  ( A [,] B
) )  /\  (
w  e.  ( ~P U  i^i  Fin )  /\  ( A [,] v
)  C_  U. w  /\  ( G  -  C
)  <  v )
)  ->  U. { V }  =  V )
158157uneq2d 3654 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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
) )
159155, 158syl5eq 2510 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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
) )
160154, 159sseqtr4d 3536 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 } ) )
161 unieq 4259 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( w  u. 
{ V } )  ->  U. y  =  U. ( w  u.  { V } ) )
162161sseq2d 3527 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( w  u. 
{ V } )  ->  ( ( A [,] R )  C_  U. y  <->  ( A [,] R )  C_  U. (
w  u.  { V } ) ) )
163162rspcev 3210 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
)
16487, 160, 163syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
)
1651643exp2 1214 . . . . . . . . . . . . . 14  |-  ( (
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
) ) ) )
166165rexlimdv 2947 . . . . . . . . . . . . 13  |-  ( (
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
) ) )
16767, 166syl5bi 217 . . . . . . . . . . . 12  |-  ( (
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
) ) )
168167expimpd 603 . . . . . . . . . . 11  |-  ( 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
) ) )
16964, 168syl5bi 217 . . . . . . . . . 10  |-  ( ph  ->  ( v  e.  S  ->  ( ( G  -  C )  <  v  ->  E. y  e.  ( ~P U  i^i  Fin ) ( A [,] R )  C_  U. y
) ) )
170169rexlimdv 2947 . . . . . . . . 9  |-  ( ph  ->  ( E. v  e.  S  ( G  -  C )  <  v  ->  E. y  e.  ( ~P U  i^i  Fin ) ( A [,] R )  C_  U. y
) )
17160, 170mpd 15 . . . . . . . 8  |-  ( ph  ->  E. y  e.  ( ~P U  i^i  Fin ) ( A [,] R )  C_  U. y
)
172 oveq2 6304 . . . . . . . . . . 11  |-  ( v  =  R  ->  ( A [,] v )  =  ( A [,] R
) )
173172sseq1d 3526 . . . . . . . . . 10  |-  ( v  =  R  ->  (
( A [,] v
)  C_  U. y  <->  ( A [,] R ) 
C_  U. y ) )
174173rexbidv 2968 . . . . . . . . 9  |-  ( 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
) )
175 unieq 4259 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  U. z  =  U. y )
176175sseq2d 3527 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  (
( A [,] v
)  C_  U. z  <->  ( A [,] v ) 
C_  U. y ) )
177176cbvrexv 3085 . . . . . . . . . . . 12  |-  ( 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
)
17863, 177syl6bb 261 . . . . . . . . . . 11  |-  ( 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
) )
179178cbvrabv 3108 . . . . . . . . . 10  |-  { 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 }
1802, 179eqtri 2486 . . . . . . . . 9  |-  S  =  { v  e.  ( A [,] B )  |  E. y  e.  ( ~P U  i^i  Fin ) ( A [,] v )  C_  U. y }
181174, 180elrab2 3259 . . . . . . . 8  |-  ( R  e.  S  <->  ( R  e.  ( A [,] B
)  /\  E. y  e.  ( ~P U  i^i  Fin ) ( A [,] R )  C_  U. y
) )
18253, 171, 181sylanbrc 664 . . . . . . 7  |-  ( ph  ->  R  e.  S )
183 suprub 10524 . . . . . . 7  |-  ( ( ( S  C_  RR  /\  S  =/=  (/)  /\  E. n  e.  RR  A. y  e.  S  y  <_  n )  /\  R  e.  S )  ->  R  <_  sup ( S ,  RR ,  <  ) )
1849, 19, 24, 182, 183syl31anc 1231 . . . . . 6  |-  ( ph  ->  R  <_  sup ( S ,  RR ,  <  ) )
185184, 1syl6breqr 4496 . . . . 5  |-  ( ph  ->  R  <_  G )
186 iftrue 3950 . . . . . . 7  |-  ( ( G  +  ( C  /  2 ) )  <_  B  ->  if ( ( G  +  ( C  /  2
) )  <_  B ,  ( G  +  ( C  /  2
) ) ,  B
)  =  ( G  +  ( C  / 
2 ) ) )
18735, 186syl5eq 2510 . . . . . 6  |-  ( ( G  +  ( C  /  2 ) )  <_  B  ->  R  =  ( G  +  ( C  /  2
) ) )
188187breq1d 4466 . . . . 5  |-  ( ( G  +  ( C  /  2 ) )  <_  B  ->  ( R  <_  G  <->  ( G  +  ( C  / 
2 ) )  <_  G ) )
189185, 188syl5ibcom 220 . . . 4  |-  ( ph  ->  ( ( G  +  ( C  /  2
) )  <_  B  ->  ( G  +  ( C  /  2 ) )  <_  G )
)
19034, 189mtod 177 . . 3  |-  ( ph  ->  -.  ( G  +  ( C  /  2
) )  <_  B
)
191 iffalse 3953 . . . 4  |-  ( -.  ( G  +  ( C  /  2 ) )  <_  B  ->  if ( ( G  +  ( C  /  2
) )  <_  B ,  ( G  +  ( C  /  2
) ) ,  B
)  =  B )
19235, 191syl5eq 2510 . . 3  |-  ( -.  ( G  +  ( C  /  2 ) )  <_  B  ->  R  =  B )
193190, 192syl 16 . 2  |-  ( ph  ->  R  =  B )
194193, 182eqeltrrd 2546 1  |-  ( ph  ->  B  e.  S )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 973    = wceq 1395    e. wcel 1819    =/= wne 2652   A.wral 2807   E.wrex 2808   {crab 2811    u. cun 3469    i^i cin 3470    C_ wss 3471   (/)c0 3793   ifcif 3944   ~Pcpw 4015   {csn 4032   U.cuni 4251   class class class wbr 4456    X. cxp 5006   ran crn 5009    |` cres 5010    o. ccom 5012   ` cfv 5594  (class class class)co 6296   Fincfn 7535   supcsup 7918   RRcr 9508    + caddc 9512   RR*cxr 9644    < clt 9645    <_ cle 9646    - cmin 9824    / cdiv 10227   2c2 10606   RR+crp 11245   (,)cioo 11554   [,]cicc 11557   abscabs 13079   ↾t crest 14838   topGenctg 14855   ballcbl 18532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586  ax-pre-sup 9587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-1o 7148  df-oadd 7152  df-er 7329  df-map 7440  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-sup 7919  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-div 10228  df-nn 10557  df-2 10615  df-3 10616  df-n0 10817  df-z 10886  df-uz 11107  df-rp 11246  df-xadd 11344  df-ioo 11558  df-icc 11561  df-seq 12111  df-exp 12170  df-cj 12944  df-re 12945  df-im 12946  df-sqrt 13080  df-abs 13081  df-psmet 18538  df-xmet 18539  df-met 18540  df-bl 18541
This theorem is referenced by:  icccmplem3  21455
  Copyright terms: Public domain W3C validator