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

Theorem mblfinlem4 31980
Description: Backward direction of ismblfin 31981. (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 9714 . . . 4  |-  <  Or  RR
21a1i 11 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  <  Or  RR )
3 simplr 762 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( vol* `  A )  e.  RR )
4 vex 3048 . . . . . . 7  |-  u  e. 
_V
5 eqeq1 2455 . . . . . . . . 9  |-  ( y  =  u  ->  (
y  =  ( vol `  b )  <->  u  =  ( vol `  b ) ) )
65anbi2d 710 . . . . . . . 8  |-  ( y  =  u  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  u  =  ( vol `  b ) ) ) )
76rexbidv 2901 . . . . . . 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 3185 . . . . . 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 764 . . . . . . . . 9  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) )  -> 
b  C_  A )
10 ovolss 22438 . . . . . . . . . . 11  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  b )  <_  ( vol* `  A ) )
11 sstr 3440 . . . . . . . . . . . . 13  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
b  C_  RR )
12 ovolcl 22431 . . . . . . . . . . . . 13  |-  ( b 
C_  RR  ->  ( vol* `  b )  e.  RR* )
1311, 12syl 17 . . . . . . . . . . . 12  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  b )  e.  RR* )
14 ovolcl 22431 . . . . . . . . . . . . 13  |-  ( A 
C_  RR  ->  ( vol* `  A )  e.  RR* )
1514adantl 468 . . . . . . . . . . . 12  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  A )  e.  RR* )
16 xrlenlt 9699 . . . . . . . . . . . 12  |-  ( ( ( vol* `  b )  e.  RR*  /\  ( vol* `  A )  e.  RR* )  ->  ( ( vol* `  b )  <_  ( vol* `  A )  <->  -.  ( vol* `  A )  <  ( vol* `  b ) ) )
1713, 15, 16syl2anc 667 . . . . . . . . . . 11  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( ( vol* `  b )  <_  ( vol* `  A )  <->  -.  ( vol* `  A )  <  ( vol* `  b ) ) )
1810, 17mpbid 214 . . . . . . . . . 10  |-  ( ( b  C_  A  /\  A  C_  RR )  ->  -.  ( vol* `  A )  <  ( vol* `  b ) )
1918ancoms 455 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  b  C_  A )  ->  -.  ( vol* `  A
)  <  ( vol* `  b ) )
209, 19sylan2 477 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  -.  ( vol* `  A )  < 
( vol* `  b ) )
21 simprrr 775 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  u  =  ( vol `  b ) )
22 uniretop 21783 . . . . . . . . . . . . . . 15  |-  RR  =  U. ( topGen `  ran  (,) )
2322cldss 20044 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
24 dfss4 3677 . . . . . . . . . . . . . 14  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
2523, 24sylib 200 . . . . . . . . . . . . 13  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
26 rembl 22494 . . . . . . . . . . . . . 14  |-  RR  e.  dom  vol
2722cldopn 20046 . . . . . . . . . . . . . . 15  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
28 opnmbl 22560 . . . . . . . . . . . . . . 15  |-  ( ( RR  \  b )  e.  ( topGen `  ran  (,) )  ->  ( RR  \  b )  e.  dom  vol )
2927, 28syl 17 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  dom  vol )
30 difmbl 22496 . . . . . . . . . . . . . 14  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  b
)  e.  dom  vol )  ->  ( RR  \ 
( RR  \  b
) )  e.  dom  vol )
3126, 29, 30sylancr 669 . . . . . . . . . . . . 13  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  e.  dom  vol )
3225, 31eqeltrrd 2530 . . . . . . . . . . . 12  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
33 mblvol 22484 . . . . . . . . . . . 12  |-  ( b  e.  dom  vol  ->  ( vol `  b )  =  ( vol* `  b ) )
3432, 33syl 17 . . . . . . . . . . 11  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  b )  =  ( vol* `  b
) )
3534ad2antrl 734 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  ( vol `  b
)  =  ( vol* `  b )
)
3621, 35eqtrd 2485 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  u  =  ( vol* `  b
) )
3736breq2d 4414 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  ( ( vol* `  A )  <  u  <->  ( vol* `  A )  <  ( vol* `  b ) ) )
3820, 37mtbird 303 . . . . . . 7  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  -.  ( vol* `  A )  < 
u )
3938rexlimdvaa 2880 . . . . . 6  |-  ( A 
C_  RR  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  u  =  ( vol `  b ) )  ->  -.  ( vol* `  A )  <  u ) )
408, 39syl5bi 221 . . . . 5  |-  ( A 
C_  RR  ->  ( u  e.  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ->  -.  ( vol* `  A )  < 
u ) )
4140ad2antrr 732 . . . 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 431 . . 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 11306 . . . . . . . . 9  |-  1  e.  RR+
44 eqid 2451 . . . . . . . . . 10  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
4544ovolgelb 22433 . . . . . . . . 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 1353 . . . . . . . 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 7493 . . . . . . . . . . 11  |-  ( f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
48 ssid 3451 . . . . . . . . . . . . . . 15  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  ( (,) 
o.  f )
4944ovollb 22432 . . . . . . . . . . . . . . 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 677 . . . . . . . . . . . . . 14  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  ) )
5150adantl 468 . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . 16  |-  ( ( abs  o.  -  )  o.  f )  =  ( ( abs  o.  -  )  o.  f )
5352, 44ovolsf 22425 . . . . . . . . . . . . . . 15  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo ) )
54 frn 5735 . . . . . . . . . . . . . . . 16  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  ( 0 [,) +oo ) )
55 icossxr 11719 . . . . . . . . . . . . . . . 16  |-  ( 0 [,) +oo )  C_  RR*
5654, 55syl6ss 3444 . . . . . . . . . . . . . . 15  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  RR* )
57 supxrcl 11600 . . . . . . . . . . . . . . 15  |-  ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) )  C_  RR* 
->  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  e.  RR* )
5853, 56, 573syl 18 . . . . . . . . . . . . . 14  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  e. 
RR* )
59 peano2re 9806 . . . . . . . . . . . . . . 15  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  A )  +  1 )  e.  RR )
6059rexrd 9690 . . . . . . . . . . . . . 14  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  A )  +  1 )  e.  RR* )
61 rncoss 5095 . . . . . . . . . . . . . . . . . 18  |-  ran  ( (,)  o.  f )  C_  ran  (,)
6261unissi 4221 . . . . . . . . . . . . . . . . 17  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  (,)
63 unirnioo 11734 . . . . . . . . . . . . . . . . 17  |-  RR  =  U. ran  (,)
6462, 63sseqtr4i 3465 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  f ) 
C_  RR
65 ovolcl 22431 . . . . . . . . . . . . . . . 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 11455 . . . . . . . . . . . . . . 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 1351 . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . 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 681 . . . . . . . . . . . 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 720 . . . . . . . . . . 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 477 . . . . . . . . . 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 569 . . . . . . . . 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 2862 . . . . . . . 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 2844 . . . . . . 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 17 . . . . . 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 732 . . . . 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 3560 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  f )
8079, 64sstri 3441 . . . . . . . . . . . . 13  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_  RR
81 ovolcl 22431 . . . . . . . . . . . . 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 540 . . . . . . . . . . 11  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR ) )
8483ad4antlr 739 . . . . . . . . . 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 22438 . . . . . . . . . . . . . . 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 678 . . . . . . . . . . . . . 14  |-  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( vol* `  U. ran  ( (,)  o.  f ) )
87 xrletr 11455 . . . . . . . . . . . . . . . 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 1354 . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . 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 682 . . . . . . . . . . . . 13  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  U. ran  ( (,)  o.  f ) )  <_ 
( ( vol* `  A )  +  1 )  ->  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) )  <_  ( ( vol* `  A )  +  1 ) ) )
9190ad4antlr 739 . . . . . . . . . . . 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 625 . . . . . . . . . . 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 22434 . . . . . . . . . . . 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 540 . . . . . . . . . 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 11469 . . . . . . . . . 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 667 . . . . . . . . 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 9938 . . . . . . . . . . . . . 14  |-  ( ( ( vol* `  A )  e.  RR  /\  u  e.  RR )  ->  ( ( vol* `  A )  -  u )  e.  RR )
9998adantrr 723 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( vol* `  A )  -  u
)  e.  RR )
100 posdif 10107 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  RR  /\  ( vol* `  A
)  e.  RR )  ->  ( u  < 
( vol* `  A )  <->  0  <  ( ( vol* `  A )  -  u
) ) )
101100ancoms 455 . . . . . . . . . . . . . . 15  |-  ( ( ( vol* `  A )  e.  RR  /\  u  e.  RR )  ->  ( u  < 
( vol* `  A )  <->  0  <  ( ( vol* `  A )  -  u
) ) )
102101biimpd 211 . . . . . . . . . . . . . 14  |-  ( ( ( vol* `  A )  e.  RR  /\  u  e.  RR )  ->  ( u  < 
( vol* `  A )  ->  0  <  ( ( vol* `  A )  -  u
) ) )
103102impr 625 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  0  <  ( ( vol* `  A )  -  u
) )
10499, 103elrpd 11338 . . . . . . . . . . . 12  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( vol* `  A )  -  u
)  e.  RR+ )
105104rphalfcld 11353 . . . . . . . . . . 11  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( ( vol* `  A )  -  u
)  /  2 )  e.  RR+ )
1063, 105sylan 474 . . . . . . . . . 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 467 . . . . . . . . 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 2451 . . . . . . . . . . 11  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)
109108ovolgelb 22433 . . . . . . . . . 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 1351 . . . . . . . . 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 667 . . . . . . . 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 7493 . . . . . . . . . . 11  |-  ( g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
113 ssid 3451 . . . . . . . . . . . . . 14  |-  U. ran  ( (,)  o.  g ) 
C_  U. ran  ( (,) 
o.  g )
114108ovollb 22432 . . . . . . . . . . . . . 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 677 . . . . . . . . . . . . 13  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  ) )
116115adantl 468 . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . 15  |-  ( ( abs  o.  -  )  o.  g )  =  ( ( abs  o.  -  )  o.  g )
118117, 108ovolsf 22425 . . . . . . . . . . . . . 14  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,) +oo ) )
119 frn 5735 . . . . . . . . . . . . . . 15  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  C_  ( 0 [,) +oo ) )
120119, 55syl6ss 3444 . . . . . . . . . . . . . 14  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  C_  RR* )
121 supxrcl 11600 . . . . . . . . . . . . . 14  |-  ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) )  C_  RR* 
->  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  e.  RR* )
122118, 120, 1213syl 18 . . . . . . . . . . . . 13  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  e. 
RR* )
12399rehalfcld 10859 . . . . . . . . . . . . . . . . 17  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( ( vol* `  A )  -  u
)  /  2 )  e.  RR )
1243, 123sylan 474 . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . 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 9670 . . . . . . . . . . . . . 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 9690 . . . . . . . . . . . . 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 5095 . . . . . . . . . . . . . . . . 17  |-  ran  ( (,)  o.  g )  C_  ran  (,)
129128unissi 4221 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  g ) 
C_  U. ran  (,)
130129, 63sseqtr4i 3465 . . . . . . . . . . . . . . 15  |-  U. ran  ( (,)  o.  g ) 
C_  RR
131 ovolcl 22431 . . . . . . . . . . . . . . 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 11455 . . . . . . . . . . . . . 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 1351 . . . . . . . . . . . . 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 481 . . . . . . . . . . . 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 681 . . . . . . . . . . 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 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 ) ) )  /\  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 569 . . . . . . . . 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 2862 . . . . . . . 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 2844 . . . . . . 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 17 . . . . . 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 540 . . . . . . . . . . . 12  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  U. ran  ( (,)  o.  f ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR ) )
144143ad3antlr 737 . . . . . . . . . . 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 22434 . . . . . . . . . . . . . 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 544 . . . . . . . . . . . 12  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 )  ->  ( 0  <_  ( vol* `  U. ran  ( (,) 
o.  f ) )  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
148147adantl 468 . . . . . . . . . . 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 11469 . . . . . . . . . . 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 480 . . . . . . . . . 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 10047 . . . . . . . . 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 11370 . . . . . . . . 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 21782 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  e.  Top
154 retopbas 21781 . . . . . . . . . . . . 13  |-  ran  (,)  e. 
TopBases
155 bastg 19981 . . . . . . . . . . . . 13  |-  ( ran 
(,)  e.  TopBases  ->  ran  (,)  C_  ( topGen `  ran  (,) )
)
156154, 155ax-mp 5 . . . . . . . . . . . 12  |-  ran  (,)  C_  ( topGen `  ran  (,) )
15761, 156sstri 3441 . . . . . . . . . . 11  |-  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
158 uniopn 19927 . . . . . . . . . . 11  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
)
159153, 157, 158mp2an 678 . . . . . . . . . 10  |-  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
160 mblfinlem2 31978 . . . . . . . . . 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 1351 . . . . . . . . 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 667 . . . . . . . 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 467 . . . . . . 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 3686 . . . . . . . . . . . . . . 15  |-  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g ) ) )  =  ( ( s  i^i  RR )  \  U. ran  ( (,)  o.  g ) )
16522cldss 20044 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  s  C_  RR )
166 df-ss 3418 . . . . . . . . . . . . . . . . 17  |-  ( s 
C_  RR  <->  ( s  i^i 
RR )  =  s )
167165, 166sylib 200 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  RR )  =  s )
168167difeq1d 3550 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( (
s  i^i  RR )  \  U. ran  ( (,) 
o.  g ) )  =  ( s  \  U. ran  ( (,)  o.  g ) ) )
169164, 168syl5eq 2497 . . . . . . . . . . . . . 14  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g
) ) )  =  ( s  \  U. ran  ( (,)  o.  g
) ) )
170128, 156sstri 3441 . . . . . . . . . . . . . . . . 17  |-  ran  ( (,)  o.  g )  C_  ( topGen `  ran  (,) )
171 uniopn 19927 . . . . . . . . . . . . . . . . 17  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  g )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) )
)
172153, 170, 171mp2an 678 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) )
17322opncld 20048 . . . . . . . . . . . . . . . 16  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) ) )  ->  ( RR  \  U. ran  ( (,)  o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
174153, 172, 173mp2an 678 . . . . . . . . . . . . . . 15  |-  ( RR 
\  U. ran  ( (,) 
o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
)
175 incld 20058 . . . . . . . . . . . . . . 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 677 . . . . . . . . . . . . . 14  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g
) ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
177169, 176eqeltrrd 2530 . . . . . . . . . . . . 13  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  \  U. ran  ( (,) 
o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
178 simpr 463 . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . 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 3572 . . . . . . . . . . . . . 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 3683 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  =  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) )
182 inss2 3653 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  C_  A
183181, 182eqsstr3i 3463 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  \  ( U. ran  ( (,)  o.  f
)  \  A )
)  C_  A
184180, 183syl6ss 3444 . . . . . . . . . . . . 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 3453 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( b  C_  A  <->  ( s  \  U. ran  ( (,)  o.  g ) )  C_  A )
)
186185anbi1d 711 . . . . . . . . . . . . . . 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 5865 . . . . . . . . . . . . . . . . 17  |-  ( ( s  \  U. ran  ( (,)  o.  g ) )  =  b  -> 
( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )
188187eqcoms 2459 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )
189188biantrud 510 . . . . . . . . . . . . . . 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 260 . . . . . . . . . . . . . 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 3150 . . . . . . . . . . . . 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 480 . . . . . . . . . . . 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 810 . . . . . . . . . . 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 731 . . . . . . . . . 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 721 . . . . . . . . 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 720 . . . . . . . 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 3560 . . . . . . . . . . . 12  |-  ( A 
\  ( s  \  U. ran  ( (,)  o.  g ) ) ) 
C_  A
198 ovolsscl 22439 . . . . . . . . . . . 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 1351 . . . . . . . . . . 11  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  (
s  \  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
200199ad5antr 740 . . . . . . . . . 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 781 . . . . . . . . . 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 459 . . . . . . . . . . 11  |-  ( ( u  e.  RR  /\  u  <  ( vol* `  A ) )  ->  u  e.  RR )
203202ad4antlr 739 . . . . . . . . . 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 3700 . . . . . . . . . . . 12  |-  ( A 
\  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) )
205204fveq2i 5868 . . . . . . . . . . 11  |-  ( vol* `  ( A  \  ( s  \  U. ran  ( (,)  o.  g
) ) ) )  =  ( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )
206 difss 3560 . . . . . . . . . . . . . . 15  |-  ( A 
\  s )  C_  A
207 inss1 3652 . . . . . . . . . . . . . . 15  |-  ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  A
208206, 207unssi 3609 . . . . . . . . . . . . . 14  |-  ( ( A  \  s )  u.  ( A  i^i  U.
ran  ( (,)  o.  g ) ) ) 
C_  A
209 ovolsscl 22439 . . . . . . . . . . . . . 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 1351 . . . . . . . . . . . . 13  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
211210ad5antr 740 . . . . . . . . . . . 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 22439 . . . . . . . . . . . . . . 15  |-  ( ( ( A  \  s
)  C_  A  /\  A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  s
) )  e.  RR )
213206, 212mp3an1 1351 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  s
) )  e.  RR )
214213ad5antr 740 . . . . . . . . . . . . 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 22439 . . . . . . . . . . . . . . 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 1351 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  i^i  U. ran  ( (,)  o.  g ) ) )  e.  RR )
217216ad5antr 740 . . . . . . . . . . . . 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 9670 . . . . . . . . . . . 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 480 . . . . . . . . . . . . 13  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  ( ( vol* `  A )  -  u )  e.  RR )
220219ad3antrrr 736 . . . . . . . . . . . 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 3564 . . . . . . . . . . . . . . 15  |-  ( A 
C_  RR  ->  ( A 
\  s )  C_  RR )
222221adantr 467 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( A  \  s
)  C_  RR )
223 ssinss1 3660 . . . . . . . . . . . . . . 15  |-  ( A 
C_  RR  ->  ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  RR )
224223adantr 467 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( A  i^i  U. ran  ( (,)  o.  g
) )  C_  RR )
225 ovolun 22452 . . . . . . . . . . . . . 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 1269 . . . . . . . . . . . . 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 740 . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . 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 764 . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . 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 22439 . . . . . . . . . . . . . . . . . 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 1352 . . . . . . . . . . . . . . . . 17  |-  ( ( s  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol* `  s )  e.  RR )
235231, 232, 234syl2anr 481 . . . . . . . . . . . . . . . 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 )  /