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

Theorem mblfinlem4 30294
Description: Backward direction of ismblfin 30295. (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 9654 . . . 4  |-  <  Or  RR
21a1i 11 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  <  Or  RR )
3 simplr 753 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( vol* `  A )  e.  RR )
4 vex 3109 . . . . . . 7  |-  u  e. 
_V
5 eqeq1 2458 . . . . . . . . 9  |-  ( y  =  u  ->  (
y  =  ( vol `  b )  <->  u  =  ( vol `  b ) ) )
65anbi2d 701 . . . . . . . 8  |-  ( y  =  u  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  u  =  ( vol `  b ) ) ) )
76rexbidv 2965 . . . . . . 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 3243 . . . . . 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 754 . . . . . . . . 9  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) )  -> 
b  C_  A )
10 ovolss 22062 . . . . . . . . . . 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 22055 . . . . . . . . . . . . 13  |-  ( b 
C_  RR  ->  ( vol* `  b )  e.  RR* )
1311, 12syl 16 . . . . . . . . . . . 12  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  b )  e.  RR* )
14 ovolcl 22055 . . . . . . . . . . . . 13  |-  ( A 
C_  RR  ->  ( vol* `  A )  e.  RR* )
1514adantl 464 . . . . . . . . . . . 12  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  A )  e.  RR* )
16 xrlenlt 9641 . . . . . . . . . . . 12  |-  ( ( ( vol* `  b )  e.  RR*  /\  ( vol* `  A )  e.  RR* )  ->  ( ( vol* `  b )  <_  ( vol* `  A )  <->  -.  ( vol* `  A )  <  ( vol* `  b ) ) )
1713, 15, 16syl2anc 659 . . . . . . . . . . 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 451 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  b  C_  A )  ->  -.  ( vol* `  A
)  <  ( vol* `  b ) )
209, 19sylan2 472 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  -.  ( vol* `  A )  < 
( vol* `  b ) )
21 simprrr 764 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  u  =  ( vol `  b ) )
22 uniretop 21435 . . . . . . . . . . . . . . 15  |-  RR  =  U. ( topGen `  ran  (,) )
2322cldss 19697 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
24 dfss4 3729 . . . . . . . . . . . . . 14  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
2523, 24sylib 196 . . . . . . . . . . . . 13  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
26 rembl 22117 . . . . . . . . . . . . . 14  |-  RR  e.  dom  vol
2722cldopn 19699 . . . . . . . . . . . . . . 15  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
28 opnmbl 22177 . . . . . . . . . . . . . . 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 22119 . . . . . . . . . . . . . 14  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  b
)  e.  dom  vol )  ->  ( RR  \ 
( RR  \  b
) )  e.  dom  vol )
3126, 29, 30sylancr 661 . . . . . . . . . . . . 13  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  e.  dom  vol )
3225, 31eqeltrrd 2543 . . . . . . . . . . . 12  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
33 mblvol 22107 . . . . . . . . . . . 12  |-  ( b  e.  dom  vol  ->  ( vol `  b )  =  ( vol* `  b ) )
3432, 33syl 16 . . . . . . . . . . 11  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  b )  =  ( vol* `  b
) )
3534ad2antrl 725 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  ( vol `  b
)  =  ( vol* `  b )
)
3621, 35eqtrd 2495 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  u  =  ( vol* `  b
) )
3736breq2d 4451 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  ( ( vol* `  A )  <  u  <->  ( vol* `  A )  <  ( vol* `  b ) ) )
3820, 37mtbird 299 . . . . . . 7  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  -.  ( vol* `  A )  < 
u )
3938rexlimdvaa 2947 . . . . . 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 723 . . . 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 427 . . 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 11225 . . . . . . . . 9  |-  1  e.  RR+
44 eqid 2454 . . . . . . . . . 10  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
4544ovolgelb 22057 . . . . . . . . 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 1311 . . . . . . . 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 7433 . . . . . . . . . . 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 22056 . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . 14  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  ) )
5150adantl 464 . . . . . . . . . . . . 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 2454 . . . . . . . . . . . . . . . 16  |-  ( ( abs  o.  -  )  o.  f )  =  ( ( abs  o.  -  )  o.  f )
5352, 44ovolsf 22050 . . . . . . . . . . . . . . 15  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo ) )
54 frn 5719 . . . . . . . . . . . . . . . 16  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  ( 0 [,) +oo ) )
55 icossxr 11612 . . . . . . . . . . . . . . . 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 11509 . . . . . . . . . . . . . . 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 9742 . . . . . . . . . . . . . . 15  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  A )  +  1 )  e.  RR )
6059rexrd 9632 . . . . . . . . . . . . . 14  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  A )  +  1 )  e.  RR* )
61 rncoss 5252 . . . . . . . . . . . . . . . . . 18  |-  ran  ( (,)  o.  f )  C_  ran  (,)
6261unissi 4258 . . . . . . . . . . . . . . . . 17  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  (,)
63 unirnioo 11627 . . . . . . . . . . . . . . . . 17  |-  RR  =  U. ran  (,)
6462, 63sseqtr4i 3522 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  f ) 
C_  RR
65 ovolcl 22055 . . . . . . . . . . . . . . . 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 11364 . . . . . . . . . . . . . . 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 1309 . . . . . . . . . . . . . 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 476 . . . . . . . . . . . . 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 673 . . . . . . . . . . . 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 711 . . . . . . . . . . 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 472 . . . . . . . . . 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 563 . . . . . . . . 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 2929 . . . . . . . 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 2911 . . . . . . 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 723 . . . . 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 3617 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  f )
8079, 64sstri 3498 . . . . . . . . . . . . 13  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_  RR
81 ovolcl 22055 . . . . . . . . . . . . 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 535 . . . . . . . . . . 11  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR ) )
8483ad4antlr 730 . . . . . . . . . 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 22062 . . . . . . . . . . . . . . 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 670 . . . . . . . . . . . . . 14  |-  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( vol* `  U. ran  ( (,)  o.  f ) )
87 xrletr 11364 . . . . . . . . . . . . . . . 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 1312 . . . . . . . . . . . . . . 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 674 . . . . . . . . . . . . 13  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  U. ran  ( (,)  o.  f ) )  <_ 
( ( vol* `  A )  +  1 )  ->  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) )  <_  ( ( vol* `  A )  +  1 ) ) )
9190ad4antlr 730 . . . . . . . . . . . 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 617 . . . . . . . . . . 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 22058 . . . . . . . . . . . 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 535 . . . . . . . . . 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 11378 . . . . . . . . . 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 659 . . . . . . . . 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 9874 . . . . . . . . . . . . . 14  |-  ( ( ( vol* `  A )  e.  RR  /\  u  e.  RR )  ->  ( ( vol* `  A )  -  u )  e.  RR )
9998adantrr 714 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( vol* `  A )  -  u
)  e.  RR )
100 posdif 10041 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  RR  /\  ( vol* `  A
)  e.  RR )  ->  ( u  < 
( vol* `  A )  <->  0  <  ( ( vol* `  A )  -  u
) ) )
101100ancoms 451 . . . . . . . . . . . . . . 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 617 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  0  <  ( ( vol* `  A )  -  u
) )
10499, 103elrpd 11256 . . . . . . . . . . . 12  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( vol* `  A )  -  u
)  e.  RR+ )
105104rphalfcld 11271 . . . . . . . . . . 11  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( ( vol* `  A )  -  u
)  /  2 )  e.  RR+ )
1063, 105sylan 469 . . . . . . . . . 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 463 . . . . . . . . 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 2454 . . . . . . . . . . 11  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)
109108ovolgelb 22057 . . . . . . . . . 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 1309 . . . . . . . . 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 659 . . . . . . . 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 7433 . . . . . . . . . . 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 22056 . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . 13  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  ) )
116115adantl 464 . . . . . . . . . . . 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 2454 . . . . . . . . . . . . . . 15  |-  ( ( abs  o.  -  )  o.  g )  =  ( ( abs  o.  -  )  o.  g )
118117, 108ovolsf 22050 . . . . . . . . . . . . . 14  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,) +oo ) )
119 frn 5719 . . . . . . . . . . . . . . 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 11509 . . . . . . . . . . . . . 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 10781 . . . . . . . . . . . . . . . . 17  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( ( vol* `  A )  -  u
)  /  2 )  e.  RR )
1243, 123sylan 469 . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . 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 9612 . . . . . . . . . . . . . 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 9632 . . . . . . . . . . . . 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 5252 . . . . . . . . . . . . . . . . 17  |-  ran  ( (,)  o.  g )  C_  ran  (,)
129128unissi 4258 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  g ) 
C_  U. ran  (,)
130129, 63sseqtr4i 3522 . . . . . . . . . . . . . . 15  |-  U. ran  ( (,)  o.  g ) 
C_  RR
131 ovolcl 22055 . . . . . . . . . . . . . . 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 11364 . . . . . . . . . . . . . 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 1309 . . . . . . . . . . . . 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 476 . . . . . . . . . . . 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 673 . . . . . . . . . . 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 472 . . . . . . . . . 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 563 . . . . . . . . 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 2929 . . . . . . . 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 2911 . . . . . . 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 535 . . . . . . . . . . . 12  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  U. ran  ( (,)  o.  f ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR ) )
144143ad3antlr 728 . . . . . . . . . . 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 22058 . . . . . . . . . . . . . 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 539 . . . . . . . . . . . 12  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 )  ->  ( 0  <_  ( vol* `  U. ran  ( (,) 
o.  f ) )  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
148147adantl 464 . . . . . . . . . . 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 11378 . . . . . . . . . . 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 475 . . . . . . . . . 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 9983 . . . . . . . . 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 11287 . . . . . . . . 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 21434 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  e.  Top
154 retopbas 21433 . . . . . . . . . . . . 13  |-  ran  (,)  e. 
TopBases
155 bastg 19634 . . . . . . . . . . . . 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 19573 . . . . . . . . . . 11  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
)
159153, 157, 158mp2an 670 . . . . . . . . . 10  |-  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
160 mblfinlem2 30292 . . . . . . . . . 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 1309 . . . . . . . . 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 659 . . . . . . . 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 463 . . . . . . 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 3738 . . . . . . . . . . . . . . 15  |-  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g ) ) )  =  ( ( s  i^i  RR )  \  U. ran  ( (,)  o.  g ) )
16522cldss 19697 . . . . . . . . . . . . . . . . 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 3607 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( (
s  i^i  RR )  \  U. ran  ( (,) 
o.  g ) )  =  ( s  \  U. ran  ( (,)  o.  g ) ) )
169164, 168syl5eq 2507 . . . . . . . . . . . . . 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 19573 . . . . . . . . . . . . . . . . 17  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  g )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) )
)
172153, 170, 171mp2an 670 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) )
17322opncld 19701 . . . . . . . . . . . . . . . 16  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) ) )  ->  ( RR  \  U. ran  ( (,)  o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
174153, 172, 173mp2an 670 . . . . . . . . . . . . . . 15  |-  ( RR 
\  U. ran  ( (,) 
o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
)
175 incld 19711 . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . 14  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g
) ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
177169, 176eqeltrrd 2543 . . . . . . . . . . . . 13  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  \  U. ran  ( (,) 
o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
178 simpr 459 . . . . . . . . . . . . . . 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 455 . . . . . . . . . . . . . . 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 3629 . . . . . . . . . . . . . 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 3735 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  =  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) )
182 inss2 3705 . . . . . . . . . . . . . . 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 702 . . . . . . . . . . . . . . 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 5848 . . . . . . . . . . . . . . . . 17  |-  ( ( s  \  U. ran  ( (,)  o.  g ) )  =  b  -> 
( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )
188187eqcoms 2466 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )
189188biantrud 505 . . . . . . . . . . . . . . 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 3207 . . . . . . . . . . . . 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 475 . . . . . . . . . . . 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 799 . . . . . . . . . . 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 722 . . . . . . . . . 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 712 . . . . . . . . 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 711 . . . . . . . 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 3617 . . . . . . . . . . . 12  |-  ( A 
\  ( s  \  U. ran  ( (,)  o.  g ) ) ) 
C_  A
198 ovolsscl 22063 . . . . . . . . . . . 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 1309 . . . . . . . . . . 11  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  (
s  \  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
200199ad5antr 731 . . . . . . . . . 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 770 . . . . . . . . . 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 455 . . . . . . . . . . 11  |-  ( ( u  e.  RR  /\  u  <  ( vol* `  A ) )  ->  u  e.  RR )
203202ad4antlr 730 . . . . . . . . . 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 3752 . . . . . . . . . . . 12  |-  ( A 
\  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) )
205204fveq2i 5851 . . . . . . . . . . 11  |-  ( vol* `  ( A  \  ( s  \  U. ran  ( (,)  o.  g
) ) ) )  =  ( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )
206 difss 3617 . . . . . . . . . . . . . . 15  |-  ( A 
\  s )  C_  A
207 inss1 3704 . . . . . . . . . . . . . . 15  |-  ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  A
208206, 207unssi 3665 . . . . . . . . . . . . . 14  |-  ( ( A  \  s )  u.  ( A  i^i  U.
ran  ( (,)  o.  g ) ) ) 
C_  A
209 ovolsscl 22063 . . . . . . . . . . . . . 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 1309 . . . . . . . . . . . . 13  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
211210ad5antr 731 . . . . . . . . . . . 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 22063 . . . . . . . . . . . . . . 15  |-  ( ( ( A  \  s
)  C_  A  /\  A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  s
) )  e.  RR )
213206, 212mp3an1 1309 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  s
) )  e.  RR )
214213ad5antr 731 . . . . . . . . . . . . 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 22063 . . . . . . . . . . . . . . 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 1309 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  i^i  U. ran  ( (,)  o.  g ) ) )  e.  RR )
217216ad5antr 731 . . . . . . . . . . . . 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 9612 . . . . . . . . . . . 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 475 . . . . . . . . . . . . 13  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  ( ( vol* `  A )  -  u )  e.  RR )
220219ad3antrrr 727 . . . . . . . . . . . 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 3621 . . . . . . . . . . . . . . 15  |-  ( A 
C_  RR  ->  ( A 
\  s )  C_  RR )
222221adantr 463 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( A  \  s
)  C_  RR )
223 ssinss1 3712 . . . . . . . . . . . . . . 15  |-  ( A 
C_  RR  ->  ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  RR )
224223adantr 463 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( A  i^i  U. ran  ( (,)  o.  g
) )  C_  RR )
225 ovolun 22076 . . . . . . . . . . . . . 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 1227 . . . . . . . . . . . . 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 731 . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . 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 22063 . . . . . . . . . . . . . . . . . 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 1310 . . . . . . . . . . . . . . . . 17  |-  ( ( s  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol* `  s )  e.  RR )
235231, 232, 234syl2anr 476 . . . . . . . . . . . . . . . 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 ) )