Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mblfinlem4 Structured version   Unicode version

Theorem mblfinlem4 30029
Description: Backward direction of ismblfin 30030. (Contributed by Brendan Leahy, 28-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
Assertion
Ref Expression
mblfinlem4  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( vol* `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )
Distinct variable group:    y, b, A

Proof of Theorem mblfinlem4
Dummy variables  f 
g  s  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltso 9668 . . . 4  |-  <  Or  RR
21a1i 11 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  <  Or  RR )
3 simplr 755 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( vol* `  A )  e.  RR )
4 vex 3098 . . . . . . 7  |-  u  e. 
_V
5 eqeq1 2447 . . . . . . . . 9  |-  ( y  =  u  ->  (
y  =  ( vol `  b )  <->  u  =  ( vol `  b ) ) )
65anbi2d 703 . . . . . . . 8  |-  ( y  =  u  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  u  =  ( vol `  b ) ) ) )
76rexbidv 2954 . . . . . . 7  |-  ( y  =  u  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  y  =  ( vol `  b
) )  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  u  =  ( vol `  b ) ) ) )
84, 7elab 3232 . . . . . 6  |-  ( u  e.  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  <->  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  u  =  ( vol `  b
) ) )
9 simprl 756 . . . . . . . . 9  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) )  -> 
b  C_  A )
10 ovolss 21769 . . . . . . . . . . 11  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  b )  <_  ( vol* `  A ) )
11 sstr 3497 . . . . . . . . . . . . 13  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
b  C_  RR )
12 ovolcl 21762 . . . . . . . . . . . . 13  |-  ( b 
C_  RR  ->  ( vol* `  b )  e.  RR* )
1311, 12syl 16 . . . . . . . . . . . 12  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  b )  e.  RR* )
14 ovolcl 21762 . . . . . . . . . . . . 13  |-  ( A 
C_  RR  ->  ( vol* `  A )  e.  RR* )
1514adantl 466 . . . . . . . . . . . 12  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  A )  e.  RR* )
16 xrlenlt 9655 . . . . . . . . . . . 12  |-  ( ( ( vol* `  b )  e.  RR*  /\  ( vol* `  A )  e.  RR* )  ->  ( ( vol* `  b )  <_  ( vol* `  A )  <->  -.  ( vol* `  A )  <  ( vol* `  b ) ) )
1713, 15, 16syl2anc 661 . . . . . . . . . . 11  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( ( vol* `  b )  <_  ( vol* `  A )  <->  -.  ( vol* `  A )  <  ( vol* `  b ) ) )
1810, 17mpbid 210 . . . . . . . . . 10  |-  ( ( b  C_  A  /\  A  C_  RR )  ->  -.  ( vol* `  A )  <  ( vol* `  b ) )
1918ancoms 453 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  b  C_  A )  ->  -.  ( vol* `  A
)  <  ( vol* `  b ) )
209, 19sylan2 474 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  -.  ( vol* `  A )  < 
( vol* `  b ) )
21 simprrr 766 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  u  =  ( vol `  b ) )
22 uniretop 21142 . . . . . . . . . . . . . . 15  |-  RR  =  U. ( topGen `  ran  (,) )
2322cldss 19403 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
24 dfss4 3717 . . . . . . . . . . . . . 14  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
2523, 24sylib 196 . . . . . . . . . . . . 13  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
26 rembl 21824 . . . . . . . . . . . . . 14  |-  RR  e.  dom  vol
2722cldopn 19405 . . . . . . . . . . . . . . 15  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
28 opnmbl 21884 . . . . . . . . . . . . . . 15  |-  ( ( RR  \  b )  e.  ( topGen `  ran  (,) )  ->  ( RR  \  b )  e.  dom  vol )
2927, 28syl 16 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  dom  vol )
30 difmbl 21826 . . . . . . . . . . . . . 14  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  b
)  e.  dom  vol )  ->  ( RR  \ 
( RR  \  b
) )  e.  dom  vol )
3126, 29, 30sylancr 663 . . . . . . . . . . . . 13  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  e.  dom  vol )
3225, 31eqeltrrd 2532 . . . . . . . . . . . 12  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
33 mblvol 21814 . . . . . . . . . . . 12  |-  ( b  e.  dom  vol  ->  ( vol `  b )  =  ( vol* `  b ) )
3432, 33syl 16 . . . . . . . . . . 11  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  b )  =  ( vol* `  b
) )
3534ad2antrl 727 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  ( vol `  b
)  =  ( vol* `  b )
)
3621, 35eqtrd 2484 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  u  =  ( vol* `  b
) )
3736breq2d 4449 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  ( ( vol* `  A )  <  u  <->  ( vol* `  A )  <  ( vol* `  b ) ) )
3820, 37mtbird 301 . . . . . . 7  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  -.  ( vol* `  A )  < 
u )
3938rexlimdvaa 2936 . . . . . 6  |-  ( A 
C_  RR  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  u  =  ( vol `  b ) )  ->  -.  ( vol* `  A )  <  u ) )
408, 39syl5bi 217 . . . . 5  |-  ( A 
C_  RR  ->  ( u  e.  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ->  -.  ( vol* `  A )  < 
u ) )
4140ad2antrr 725 . . . 4  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( u  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ->  -.  ( vol* `  A
)  <  u )
)
4241imp 429 . . 3  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  u  e. 
{ y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } )  ->  -.  ( vol* `  A )  <  u
)
43 1rp 11233 . . . . . . . . 9  |-  1  e.  RR+
44 eqid 2443 . . . . . . . . . 10  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
4544ovolgelb 21764 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR  /\  1  e.  RR+ )  ->  E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U.
ran  ( (,)  o.  f )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 ) ) )
4643, 45mp3an3 1314 . . . . . . . 8  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  ->  E. f  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U. ran  ( (,)  o.  f )  /\  sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
) ,  RR* ,  <  )  <_  ( ( vol* `  A )  +  1 ) ) )
47 elmapi 7442 . . . . . . . . . . 11  |-  ( f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
48 ssid 3508 . . . . . . . . . . . . . . 15  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  ( (,) 
o.  f )
4944ovollb 21763 . . . . . . . . . . . . . . 15  |-  ( ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  U. ran  ( (,)  o.  f
)  C_  U. ran  ( (,)  o.  f ) )  ->  ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  ) )
5048, 49mpan2 671 . . . . . . . . . . . . . 14  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  ) )
5150adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( vol* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
) ,  RR* ,  <  ) )
52 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ( ( abs  o.  -  )  o.  f )  =  ( ( abs  o.  -  )  o.  f )
5352, 44ovolsf 21757 . . . . . . . . . . . . . . 15  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo ) )
54 frn 5727 . . . . . . . . . . . . . . . 16  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  ( 0 [,) +oo ) )
55 icossxr 11618 . . . . . . . . . . . . . . . 16  |-  ( 0 [,) +oo )  C_  RR*
5654, 55syl6ss 3501 . . . . . . . . . . . . . . 15  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  RR* )
57 supxrcl 11515 . . . . . . . . . . . . . . 15  |-  ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) )  C_  RR* 
->  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  e.  RR* )
5853, 56, 573syl 20 . . . . . . . . . . . . . 14  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  e. 
RR* )
59 peano2re 9756 . . . . . . . . . . . . . . 15  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  A )  +  1 )  e.  RR )
6059rexrd 9646 . . . . . . . . . . . . . 14  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  A )  +  1 )  e.  RR* )
61 rncoss 5253 . . . . . . . . . . . . . . . . . 18  |-  ran  ( (,)  o.  f )  C_  ran  (,)
6261unissi 4257 . . . . . . . . . . . . . . . . 17  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  (,)
63 unirnioo 11633 . . . . . . . . . . . . . . . . 17  |-  RR  =  U. ran  (,)
6462, 63sseqtr4i 3522 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  f ) 
C_  RR
65 ovolcl 21762 . . . . . . . . . . . . . . . 16  |-  ( U. ran  ( (,)  o.  f
)  C_  RR  ->  ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR* )
6664, 65ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR*
67 xrletr 11370 . . . . . . . . . . . . . . 15  |-  ( ( ( vol* `  U. ran  ( (,)  o.  f ) )  e. 
RR*  /\  sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e. 
RR* )  ->  (
( ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
6866, 67mp3an1 1312 . . . . . . . . . . . . . 14  |-  ( ( sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  e.  RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR* )  ->  ( ( ( vol* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
6958, 60, 68syl2anr 478 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( ( ( vol* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
7051, 69mpand 675 . . . . . . . . . . . 12  |-  ( ( ( vol* `  A )  e.  RR  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( sup ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
7170adantll 713 . . . . . . . . . . 11  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  ->  ( sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
7247, 71sylan2 474 . . . . . . . . . 10  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  ( sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
7372anim2d 565 . . . . . . . . 9  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  ( ( A 
C_  U. ran  ( (,) 
o.  f )  /\  sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
) ,  RR* ,  <  )  <_  ( ( vol* `  A )  +  1 ) )  ->  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) ) )
7473reximdva 2918 . . . . . . . 8  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U.
ran  ( (,)  o.  f )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 ) )  ->  E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) ) )
7546, 74mpd 15 . . . . . . 7  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  ->  E. f  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )
76 rexex 2900 . . . . . . 7  |-  ( E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) )  ->  E. f ( A 
C_  U. ran  ( (,) 
o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )
7775, 76syl 16 . . . . . 6  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  ->  E. f ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
7877ad2antrr 725 . . . . 5  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  E. f ( A 
C_  U. ran  ( (,) 
o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )
79 difss 3616 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  f )
8079, 64sstri 3498 . . . . . . . . . . . . 13  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_  RR
81 ovolcl 21762 . . . . . . . . . . . . 13  |-  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  RR  ->  ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e. 
RR* )
8280, 81ax-mp 5 . . . . . . . . . . . 12  |-  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  e.  RR*
8359, 82jctil 537 . . . . . . . . . . 11  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR ) )
8483ad4antlr 732 . . . . . . . . . 10  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR ) )
85 ovolss 21769 . . . . . . . . . . . . . . 15  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  f )  /\  U. ran  ( (,)  o.  f )  C_  RR )  ->  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
8679, 64, 85mp2an 672 . . . . . . . . . . . . . 14  |-  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( vol* `  U. ran  ( (,)  o.  f ) )
87 xrletr 11370 . . . . . . . . . . . . . . . 16  |-  ( ( ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e. 
RR*  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR*  /\  (
( vol* `  A )  +  1 )  e.  RR* )  ->  ( ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol* `  A )  +  1 ) )  ->  ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( ( vol* `  A )  +  1 ) ) )
8882, 66, 87mp3an12 1315 . . . . . . . . . . . . . . 15  |-  ( ( ( vol* `  A )  +  1 )  e.  RR*  ->  ( ( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) )  ->  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( ( vol* `  A )  +  1 ) ) )
8960, 88syl 16 . . . . . . . . . . . . . 14  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) )  ->  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( ( vol* `  A )  +  1 ) ) )
9086, 89mpani 676 . . . . . . . . . . . . 13  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  U. ran  ( (,)  o.  f ) )  <_ 
( ( vol* `  A )  +  1 )  ->  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) )  <_  ( ( vol* `  A )  +  1 ) ) )
9190ad4antlr 732 . . . . . . . . . . . 12  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  A  C_ 
U. ran  ( (,)  o.  f ) )  -> 
( ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol* `  A )  +  1 )  -> 
( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  <_ 
( ( vol* `  A )  +  1 ) ) )
9291impr 619 . . . . . . . . . . 11  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  <_ 
( ( vol* `  A )  +  1 ) )
93 ovolge0 21765 . . . . . . . . . . . 12  |-  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  RR  ->  0  <_  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
9480, 93ax-mp 5 . . . . . . . . . . 11  |-  0  <_  ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )
9592, 94jctil 537 . . . . . . . . . 10  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( 0  <_  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  /\  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) )  <_  ( ( vol* `  A )  +  1 ) ) )
96 xrrege0 11384 . . . . . . . . . 10  |-  ( ( ( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR )  /\  (
0  <_  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) )  /\  ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( ( vol* `  A )  +  1 ) ) )  -> 
( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
9784, 95, 96syl2anc 661 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
98 resubcl 9888 . . . . . . . . . . . . . 14  |-  ( ( ( vol* `  A )  e.  RR  /\  u  e.  RR )  ->  ( ( vol* `  A )  -  u )  e.  RR )
9998adantrr 716 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( vol* `  A )  -  u
)  e.  RR )
100 posdif 10051 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  RR  /\  ( vol* `  A
)  e.  RR )  ->  ( u  < 
( vol* `  A )  <->  0  <  ( ( vol* `  A )  -  u
) ) )
101100ancoms 453 . . . . . . . . . . . . . . 15  |-  ( ( ( vol* `  A )  e.  RR  /\  u  e.  RR )  ->  ( u  < 
( vol* `  A )  <->  0  <  ( ( vol* `  A )  -  u
) ) )
102101biimpd 207 . . . . . . . . . . . . . 14  |-  ( ( ( vol* `  A )  e.  RR  /\  u  e.  RR )  ->  ( u  < 
( vol* `  A )  ->  0  <  ( ( vol* `  A )  -  u
) ) )
103102impr 619 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  0  <  ( ( vol* `  A )  -  u
) )
10499, 103elrpd 11263 . . . . . . . . . . . 12  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( vol* `  A )  -  u
)  e.  RR+ )
105104rphalfcld 11277 . . . . . . . . . . 11  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( ( vol* `  A )  -  u
)  /  2 )  e.  RR+ )
1063, 105sylan 471 . . . . . . . . . 10  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  ( ( ( vol* `  A
)  -  u )  /  2 )  e.  RR+ )
107106adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( ( ( vol* `  A )  -  u )  /  2
)  e.  RR+ )
108 eqid 2443 . . . . . . . . . . 11  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)
109108ovolgelb 21764 . . . . . . . . . 10  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  RR  /\  ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR  /\  ( ( ( vol* `  A )  -  u
)  /  2 )  e.  RR+ )  ->  E. g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) ) )
11080, 109mp3an1 1312 . . . . . . . . 9  |-  ( ( ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR  /\  ( ( ( vol* `  A )  -  u
)  /  2 )  e.  RR+ )  ->  E. g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) ) )
11197, 107, 110syl2anc 661 . . . . . . . 8  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  ->  E. g  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  sup ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) ) )
112 elmapi 7442 . . . . . . . . . . 11  |-  ( g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
113 ssid 3508 . . . . . . . . . . . . . 14  |-  U. ran  ( (,)  o.  g ) 
C_  U. ran  ( (,) 
o.  g )
114108ovollb 21763 . . . . . . . . . . . . . 14  |-  ( ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  U. ran  ( (,)  o.  g
)  C_  U. ran  ( (,)  o.  g ) )  ->  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  ) )
115113, 114mpan2 671 . . . . . . . . . . . . 13  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  ) )
116115adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( vol* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
) ,  RR* ,  <  ) )
117 eqid 2443 . . . . . . . . . . . . . . 15  |-  ( ( abs  o.  -  )  o.  g )  =  ( ( abs  o.  -  )  o.  g )
118117, 108ovolsf 21757 . . . . . . . . . . . . . 14  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,) +oo ) )
119 frn 5727 . . . . . . . . . . . . . . 15  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  C_  ( 0 [,) +oo ) )
120119, 55syl6ss 3501 . . . . . . . . . . . . . 14  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  C_  RR* )
121 supxrcl 11515 . . . . . . . . . . . . . 14  |-  ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) )  C_  RR* 
->  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  e.  RR* )
122118, 120, 1213syl 20 . . . . . . . . . . . . 13  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  e. 
RR* )
12399rehalfcld 10791 . . . . . . . . . . . . . . . . 17  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( ( vol* `  A )  -  u
)  /  2 )  e.  RR )
1243, 123sylan 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  ( ( ( vol* `  A
)  -  u )  /  2 )  e.  RR )
125124adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( ( ( vol* `  A )  -  u )  /  2
)  e.  RR )
12697, 125readdcld 9626 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) )  e.  RR )
127126rexrd 9646 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) )  e.  RR* )
128 rncoss 5253 . . . . . . . . . . . . . . . . 17  |-  ran  ( (,)  o.  g )  C_  ran  (,)
129128unissi 4257 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  g ) 
C_  U. ran  (,)
130129, 63sseqtr4i 3522 . . . . . . . . . . . . . . 15  |-  U. ran  ( (,)  o.  g ) 
C_  RR
131 ovolcl 21762 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  g
)  C_  RR  ->  ( vol* `  U. ran  ( (,)  o.  g
) )  e.  RR* )
132130, 131ax-mp 5 . . . . . . . . . . . . . 14  |-  ( vol* `  U. ran  ( (,)  o.  g ) )  e.  RR*
133 xrletr 11370 . . . . . . . . . . . . . 14  |-  ( ( ( vol* `  U. ran  ( (,)  o.  g ) )  e. 
RR*  /\  sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  )  e. 
RR*  /\  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) )  e.  RR* )  ->  ( ( ( vol* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) )  -> 
( vol* `  U. ran  ( (,)  o.  g ) )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) ) )
134132, 133mp3an1 1312 . . . . . . . . . . . . 13  |-  ( ( sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  e.  RR*  /\  ( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) )  e.  RR* )  ->  ( ( ( vol* `  U. ran  ( (,)  o.  g
) )  <_  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  /\  sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
) ,  RR* ,  <  )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) )  ->  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
135122, 127, 134syl2anr 478 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( ( ( vol* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) )  -> 
( vol* `  U. ran  ( (,)  o.  g ) )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) ) )
136116, 135mpand 675 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( sup ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) )  ->  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
137112, 136sylan2 474 . . . . . . . . . 10  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  ( sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
) ,  RR* ,  <  )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) )  ->  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
138137anim2d 565 . . . . . . . . 9  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  (
( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) )  -> 
( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) ) )
139138reximdva 2918 . . . . . . . 8  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( E. g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) )  ->  E. g  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) ) )
140111, 139mpd 15 . . . . . . 7  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  ->  E. g  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
141 rexex 2900 . . . . . . 7  |-  ( E. g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) )  ->  E. g
( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
142140, 141syl 16 . . . . . 6  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  ->  E. g ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
14359, 66jctil 537 . . . . . . . . . . . 12  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  U. ran  ( (,)  o.  f ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR ) )
144143ad3antlr 730 . . . . . . . . . . 11  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  ( ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR*  /\  (
( vol* `  A )  +  1 )  e.  RR ) )
145 ovolge0 21765 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  C_  RR  ->  0  <_  ( vol* `  U. ran  ( (,) 
o.  f ) ) )
14664, 145ax-mp 5 . . . . . . . . . . . . 13  |-  0  <_  ( vol* `  U. ran  ( (,)  o.  f ) )
147146jctl 541 . . . . . . . . . . . 12  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 )  ->  ( 0  <_  ( vol* `  U. ran  ( (,) 
o.  f ) )  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
148147adantl 466 . . . . . . . . . . 11  |-  ( ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) )  ->  (
0  <_  ( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
149 xrrege0 11384 . . . . . . . . . . 11  |-  ( ( ( ( vol* `  U. ran  ( (,) 
o.  f ) )  e.  RR*  /\  (
( vol* `  A )  +  1 )  e.  RR )  /\  ( 0  <_ 
( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
150144, 148, 149syl2an 477 . . . . . . . . . 10  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
151150, 125resubcld 9993 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( ( vol* `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  e.  RR )
152150, 107ltsubrpd 11293 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( ( vol* `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  U. ran  ( (,) 
o.  f ) ) )
153 retop 21141 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  e.  Top
154 retopbas 21140 . . . . . . . . . . . . 13  |-  ran  (,)  e. 
TopBases
155 bastg 19340 . . . . . . . . . . . . 13  |-  ( ran 
(,)  e.  TopBases  ->  ran  (,)  C_  ( topGen `  ran  (,) )
)
156154, 155ax-mp 5 . . . . . . . . . . . 12  |-  ran  (,)  C_  ( topGen `  ran  (,) )
15761, 156sstri 3498 . . . . . . . . . . 11  |-  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
158 uniopn 19279 . . . . . . . . . . 11  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
)
159153, 157, 158mp2an 672 . . . . . . . . . 10  |-  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
160 mblfinlem2 30027 . . . . . . . . . 10  |-  ( ( U. ran  ( (,) 
o.  f )  e.  ( topGen `  ran  (,) )  /\  ( ( vol* `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  e.  RR  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  U. ran  ( (,)  o.  f ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  U.
ran  ( (,)  o.  f )  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  s ) ) )
161159, 160mp3an1 1312 . . . . . . . . 9  |-  ( ( ( ( vol* `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  e.  RR  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  U. ran  ( (,)  o.  f ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  U.
ran  ( (,)  o.  f )  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  s ) ) )
162151, 152, 161syl2anc 661 . . . . . . . 8  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  U. ran  ( (,) 
o.  f )  /\  ( ( vol* `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) )
163162adantr 465 . . . . . . 7  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  U. ran  ( (,) 
o.  f )  /\  ( ( vol* `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) )
164 indif2 3726 . . . . . . . . . . . . . . 15  |-  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g ) ) )  =  ( ( s  i^i  RR )  \  U. ran  ( (,)  o.  g ) )
16522cldss 19403 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  s  C_  RR )
166 df-ss 3475 . . . . . . . . . . . . . . . . 17  |-  ( s 
C_  RR  <->  ( s  i^i 
RR )  =  s )
167165, 166sylib 196 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  RR )  =  s )
168167difeq1d 3606 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( (
s  i^i  RR )  \  U. ran  ( (,) 
o.  g ) )  =  ( s  \  U. ran  ( (,)  o.  g ) ) )
169164, 168syl5eq 2496 . . . . . . . . . . . . . 14  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g
) ) )  =  ( s  \  U. ran  ( (,)  o.  g
) ) )
170128, 156sstri 3498 . . . . . . . . . . . . . . . . 17  |-  ran  ( (,)  o.  g )  C_  ( topGen `  ran  (,) )
171 uniopn 19279 . . . . . . . . . . . . . . . . 17  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  g )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) )
)
172153, 170, 171mp2an 672 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) )
17322opncld 19407 . . . . . . . . . . . . . . . 16  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) ) )  ->  ( RR  \  U. ran  ( (,)  o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
174153, 172, 173mp2an 672 . . . . . . . . . . . . . . 15  |-  ( RR 
\  U. ran  ( (,) 
o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
)
175 incld 19417 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( RR  \ 
U. ran  ( (,)  o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )  ->  (
s  i^i  ( RR  \ 
U. ran  ( (,)  o.  g ) ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
176174, 175mpan2 671 . . . . . . . . . . . . . 14  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g
) ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
177169, 176eqeltrrd 2532 . . . . . . . . . . . . 13  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  \  U. ran  ( (,) 
o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
178 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) )  ->  s  C_  U.
ran  ( (,)  o.  f ) )
179 simpl 457 . . . . . . . . . . . . . . 15  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) )  ->  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g ) )
180178, 179ssdif2d 3628 . . . . . . . . . . . . . 14  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) )  ->  ( s  \  U. ran  ( (,) 
o.  g ) ) 
C_  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
181 dfin4 3723 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  =  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) )
182 inss2 3704 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  C_  A
183181, 182eqsstr3i 3520 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  \  ( U. ran  ( (,)  o.  f
)  \  A )
)  C_  A
184180, 183syl6ss 3501 . . . . . . . . . . . . 13  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) )  ->  ( s  \  U. ran  ( (,) 
o.  g ) ) 
C_  A )
185 sseq1 3510 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( b  C_  A  <->  ( s  \  U. ran  ( (,)  o.  g ) )  C_  A )
)
186185anbi1d 704 . . . . . . . . . . . . . . 15  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )  <->  ( (
s  \  U. ran  ( (,)  o.  g ) ) 
C_  A  /\  ( vol `  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b
) ) ) )
187 fveq2 5856 . . . . . . . . . . . . . . . . 17  |-  ( ( s  \  U. ran  ( (,)  o.  g ) )  =  b  -> 
( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )
188187eqcoms 2455 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )
189188biantrud 507 . . . . . . . . . . . . . . 15  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( ( s  \  U. ran  ( (,)  o.  g ) )  C_  A 
<->  ( ( s  \  U. ran  ( (,)  o.  g ) )  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) ) )
190186, 189bitr4d 256 . . . . . . . . . . . . . 14  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )  <->  ( s  \  U. ran  ( (,) 
o.  g ) ) 
C_  A ) )
191190rspcev 3196 . . . . . . . . . . . . 13  |-  ( ( ( s  \  U. ran  ( (,)  o.  g
) )  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  \  U. ran  ( (,)  o.  g
) )  C_  A
)  ->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) )
192177, 184, 191syl2an 477 . . . . . . . . . . . 12  |-  ( ( s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( ( U. ran  ( (,)  o.  f )  \  A
)  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) )
193192an12s 801 . . . . . . . . . . 11  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  s  C_  U.
ran  ( (,)  o.  f ) ) )  ->  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  ( vol `  ( s 
\  U. ran  ( (,) 
o.  g ) ) )  =  ( vol `  b ) ) )
194193adantrrr 724 . . . . . . . . . 10  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( s  C_ 
U. ran  ( (,)  o.  f )  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  s ) ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  ( vol `  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b
) ) )
195194adantlr 714 . . . . . . . . 9  |-  ( ( ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) )  /\  (
s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( s  C_ 
U. ran  ( (,)  o.  f )  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  s ) ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  ( vol `  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b
) ) )
196195adantll 713 . . . . . . . 8  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) )
197 difss 3616 . . . . . . . . . . . 12  |-  ( A 
\  ( s  \  U. ran  ( (,)  o.  g ) ) ) 
C_  A
198 ovolsscl 21770 . . . . . . . . . . . 12  |-  ( ( ( A  \  (
s  \  U. ran  ( (,)  o.  g ) ) )  C_  A  /\  A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  (
s  \  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
199197, 198mp3an1 1312 . . . . . . . . . . 11  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  (
s  \  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
200199ad5antr 733 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  ( A  \ 
( s  \  U. ran  ( (,)  o.  g
) ) ) )  e.  RR )
201 simp-6r 772 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  A )  e.  RR )
202 simpl 457 . . . . . . . . . . 11  |-  ( ( u  e.  RR  /\  u  <  ( vol* `  A ) )  ->  u  e.  RR )
203202ad4antlr 732 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  u  e.  RR )
204 difdif2 3740 . . . . . . . . . . . 12  |-  ( A 
\  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) )
205204fveq2i 5859 . . . . . . . . . . 11  |-  ( vol* `  ( A  \  ( s  \  U. ran  ( (,)  o.  g
) ) ) )  =  ( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )
206 difss 3616 . . . . . . . . . . . . . . 15  |-  ( A 
\  s )  C_  A
207 inss1 3703 . . . . . . . . . . . . . . 15  |-  ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  A
208206, 207unssi 3664 . . . . . . . . . . . . . 14  |-  ( ( A  \  s )  u.  ( A  i^i  U.
ran  ( (,)  o.  g ) ) ) 
C_  A
209 ovolsscl 21770 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) )  C_  A  /\  A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
210208, 209mp3an1 1312 . . . . . . . . . . . . 13  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
211210ad5antr 733 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  e.  RR )
212 ovolsscl 21770 . . . . . . . . . . . . . . 15  |-  ( ( ( A  \  s
)  C_  A  /\  A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  s
) )  e.  RR )
213206, 212mp3an1 1312 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  s
) )  e.  RR )
214213ad5antr 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  ( A  \ 
s ) )  e.  RR )
215 ovolsscl 21770 . . . . . . . . . . . . . . 15  |-  ( ( ( A  i^i  U. ran  ( (,)  o.  g
) )  C_  A  /\  A  C_  RR  /\  ( vol* `  A
)  e.  RR )  ->  ( vol* `  ( A  i^i  U. ran  ( (,)  o.  g
) ) )  e.  RR )
216207, 215mp3an1 1312 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  i^i  U. ran  ( (,)  o.  g ) ) )  e.  RR )
217216ad5antr 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  ( A  i^i  U.
ran  ( (,)  o.  g ) ) )  e.  RR )
218214, 217readdcld 9626 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( ( vol* `  ( A 
\  s ) )  +  ( vol* `  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  e.  RR )
2193, 202, 98syl2an 477 . . . . . . . . . . . . 13  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  ( ( vol* `  A )  -  u )  e.  RR )
220219ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( ( vol* `  A )  -  u )  e.  RR )
221 ssdifss 3620 . . . . . . . . . . . . . . 15  |-  ( A 
C_  RR  ->  ( A 
\  s )  C_  RR )
222221adantr 465 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( A  \  s
)  C_  RR )
223 ssinss1 3711 . . . . . . . . . . . . . . 15  |-  ( A 
C_  RR  ->  ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  RR )
224223adantr 465 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( A  i^i  U. ran  ( (,)  o.  g
) )  C_  RR )
225 ovolun 21783 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  \ 
s )  C_  RR  /\  ( vol* `  ( A  \  s
) )  e.  RR )  /\  ( ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  RR  /\  ( vol* `  ( A  i^i  U. ran  ( (,)  o.  g ) ) )  e.  RR ) )  ->  ( vol* `  ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  <_  ( ( vol* `  ( A  \  s ) )  +  ( vol* `  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) ) )
226222, 213, 224, 216, 225syl22anc 1230 . . . . . . . . . . . . 13  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )  <_  (
( vol* `  ( A  \  s
) )  +  ( vol* `  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) ) )
227226ad5antr 733 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  <_  ( ( vol* `  ( A  \  s ) )  +  ( vol* `  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) ) )
228124ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  -> 
( ( ( vol* `  A )  -  u )  /  2
)  e.  RR )
229228adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( (
( vol* `  A )  -  u
)  /  2 )  e.  RR )
230150ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
231 simprl 756 . . . . . . . . . . . . . . . . 17  |-  ( ( s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( s  C_ 
U. ran  ( (,)  o.  f )  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  s ) ) )  ->  s  C_ 
U. ran  ( (,)  o.  f ) )
232150adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  -> 
( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
233 ovolsscl 21770 . . . . . . . . . . . . . . . . . 18  |-  ( ( s  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )  ->  ( vol* `  s )  e.  RR )
23464, 233mp3an2 1313 . . . . . . . . . . . . . . . . 17  |-  ( ( s  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol* `  s )  e.  RR )
235231, 232, 234syl2anr 478 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )