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

Theorem mblfinlem4 28457
Description: Backward direction of ismblfin 28458. (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 9476 . . . 4  |-  <  Or  RR
21a1i 11 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  <  Or  RR )
3 simplr 754 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( vol* `  A )  e.  RR )
4 vex 2996 . . . . . . 7  |-  u  e. 
_V
5 eqeq1 2449 . . . . . . . . 9  |-  ( y  =  u  ->  (
y  =  ( vol `  b )  <->  u  =  ( vol `  b ) ) )
65anbi2d 703 . . . . . . . 8  |-  ( y  =  u  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  u  =  ( vol `  b ) ) ) )
76rexbidv 2757 . . . . . . 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 3127 . . . . . 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 755 . . . . . . . . 9  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) )  -> 
b  C_  A )
10 ovolss 20990 . . . . . . . . . . 11  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  b )  <_  ( vol* `  A ) )
11 sstr 3385 . . . . . . . . . . . . 13  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
b  C_  RR )
12 ovolcl 20983 . . . . . . . . . . . . 13  |-  ( b 
C_  RR  ->  ( vol* `  b )  e.  RR* )
1311, 12syl 16 . . . . . . . . . . . 12  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  b )  e.  RR* )
14 ovolcl 20983 . . . . . . . . . . . . 13  |-  ( A 
C_  RR  ->  ( vol* `  A )  e.  RR* )
1514adantl 466 . . . . . . . . . . . 12  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( vol* `  A )  e.  RR* )
16 xrlenlt 9463 . . . . . . . . . . . 12  |-  ( ( ( vol* `  b )  e.  RR*  /\  ( vol* `  A )  e.  RR* )  ->  ( ( vol* `  b )  <_  ( vol* `  A )  <->  -.  ( vol* `  A )  <  ( vol* `  b ) ) )
1713, 15, 16syl2anc 661 . . . . . . . . . . 11  |-  ( ( b  C_  A  /\  A  C_  RR )  -> 
( ( vol* `  b )  <_  ( vol* `  A )  <->  -.  ( vol* `  A )  <  ( vol* `  b ) ) )
1810, 17mpbid 210 . . . . . . . . . 10  |-  ( ( b  C_  A  /\  A  C_  RR )  ->  -.  ( vol* `  A )  <  ( vol* `  b ) )
1918ancoms 453 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  b  C_  A )  ->  -.  ( vol* `  A
)  <  ( vol* `  b ) )
209, 19sylan2 474 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  -.  ( vol* `  A )  < 
( vol* `  b ) )
21 simprrr 764 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  u  =  ( vol `  b ) )
22 uniretop 20363 . . . . . . . . . . . . . . 15  |-  RR  =  U. ( topGen `  ran  (,) )
2322cldss 18655 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
24 dfss4 3605 . . . . . . . . . . . . . 14  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
2523, 24sylib 196 . . . . . . . . . . . . 13  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
26 rembl 21044 . . . . . . . . . . . . . 14  |-  RR  e.  dom  vol
2722cldopn 18657 . . . . . . . . . . . . . . 15  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
28 opnmbl 21104 . . . . . . . . . . . . . . 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 21046 . . . . . . . . . . . . . 14  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  b
)  e.  dom  vol )  ->  ( RR  \ 
( RR  \  b
) )  e.  dom  vol )
3126, 29, 30sylancr 663 . . . . . . . . . . . . 13  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  e.  dom  vol )
3225, 31eqeltrrd 2518 . . . . . . . . . . . 12  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
33 mblvol 21035 . . . . . . . . . . . 12  |-  ( b  e.  dom  vol  ->  ( vol `  b )  =  ( vol* `  b ) )
3432, 33syl 16 . . . . . . . . . . 11  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  b )  =  ( vol* `  b
) )
3534ad2antrl 727 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  ( vol `  b
)  =  ( vol* `  b )
)
3621, 35eqtrd 2475 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  u  =  ( vol* `  b
) )
3736breq2d 4325 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  ( ( vol* `  A )  <  u  <->  ( vol* `  A )  <  ( vol* `  b ) ) )
3820, 37mtbird 301 . . . . . . 7  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  u  =  ( vol `  b
) ) ) )  ->  -.  ( vol* `  A )  < 
u )
3938rexlimdvaa 2863 . . . . . 6  |-  ( A 
C_  RR  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  u  =  ( vol `  b ) )  ->  -.  ( vol* `  A )  <  u ) )
408, 39syl5bi 217 . . . . 5  |-  ( A 
C_  RR  ->  ( u  e.  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ->  -.  ( vol* `  A )  < 
u ) )
4140ad2antrr 725 . . . 4  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( u  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ->  -.  ( vol* `  A
)  <  u )
)
4241imp 429 . . 3  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  u  e. 
{ y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } )  ->  -.  ( vol* `  A )  <  u
)
43 1rp 11016 . . . . . . . . 9  |-  1  e.  RR+
44 eqid 2443 . . . . . . . . . 10  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
4544ovolgelb 20985 . . . . . . . . 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 1303 . . . . . . . 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 7255 . . . . . . . . . . 11  |-  ( f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
48 ssid 3396 . . . . . . . . . . . . . . 15  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  ( (,) 
o.  f )
4944ovollb 20984 . . . . . . . . . . . . . . 15  |-  ( ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  U. ran  ( (,)  o.  f
)  C_  U. ran  ( (,)  o.  f ) )  ->  ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  ) )
5048, 49mpan2 671 . . . . . . . . . . . . . 14  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  ) )
5150adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( vol* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
) ,  RR* ,  <  ) )
52 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ( ( abs  o.  -  )  o.  f )  =  ( ( abs  o.  -  )  o.  f )
5352, 44ovolsf 20978 . . . . . . . . . . . . . . 15  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo ) )
54 frn 5586 . . . . . . . . . . . . . . . 16  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  ( 0 [,) +oo ) )
55 icossxr 11401 . . . . . . . . . . . . . . . 16  |-  ( 0 [,) +oo )  C_  RR*
5654, 55syl6ss 3389 . . . . . . . . . . . . . . 15  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  RR* )
57 supxrcl 11298 . . . . . . . . . . . . . . 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 9563 . . . . . . . . . . . . . . 15  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  A )  +  1 )  e.  RR )
6059rexrd 9454 . . . . . . . . . . . . . 14  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  A )  +  1 )  e.  RR* )
61 rncoss 5121 . . . . . . . . . . . . . . . . . 18  |-  ran  ( (,)  o.  f )  C_  ran  (,)
6261unissi 4135 . . . . . . . . . . . . . . . . 17  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  (,)
63 unirnioo 11410 . . . . . . . . . . . . . . . . 17  |-  RR  =  U. ran  (,)
6462, 63sseqtr4i 3410 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  f ) 
C_  RR
65 ovolcl 20983 . . . . . . . . . . . . . . . 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 11153 . . . . . . . . . . . . . . 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 1301 . . . . . . . . . . . . . 14  |-  ( ( sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  e.  RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR* )  ->  ( ( ( vol* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
6958, 60, 68syl2anr 478 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( ( ( vol* `  U. ran  ( (,)  o.  f ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
7051, 69mpand 675 . . . . . . . . . . . 12  |-  ( ( ( vol* `  A )  e.  RR  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( sup ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
7170adantll 713 . . . . . . . . . . 11  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  ->  ( sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
7247, 71sylan2 474 . . . . . . . . . 10  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  ( sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  A )  +  1 )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
7372anim2d 565 . . . . . . . . 9  |-  ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  ( ( A 
C_  U. ran  ( (,) 
o.  f )  /\  sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
) ,  RR* ,  <  )  <_  ( ( vol* `  A )  +  1 ) )  ->  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) ) )
7473reximdva 2849 . . . . . . . 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 2796 . . . . . . 7  |-  ( E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) )  ->  E. f ( A 
C_  U. ran  ( (,) 
o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )
7775, 76syl 16 . . . . . 6  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  ->  E. f ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
7877ad2antrr 725 . . . . 5  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  E. f ( A 
C_  U. ran  ( (,) 
o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )
79 difss 3504 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  f )
8079, 64sstri 3386 . . . . . . . . . . . . 13  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_  RR
81 ovolcl 20983 . . . . . . . . . . . . 13  |-  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  RR  ->  ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e. 
RR* )
8280, 81ax-mp 5 . . . . . . . . . . . 12  |-  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  e.  RR*
8359, 82jctil 537 . . . . . . . . . . 11  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR ) )
8483ad4antlr 732 . . . . . . . . . 10  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR ) )
85 ovolss 20990 . . . . . . . . . . . . . . 15  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  f )  /\  U. ran  ( (,)  o.  f )  C_  RR )  ->  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
8679, 64, 85mp2an 672 . . . . . . . . . . . . . 14  |-  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( vol* `  U. ran  ( (,)  o.  f ) )
87 xrletr 11153 . . . . . . . . . . . . . . . 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 1304 . . . . . . . . . . . . . . 15  |-  ( ( ( vol* `  A )  +  1 )  e.  RR*  ->  ( ( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) )  ->  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( ( vol* `  A )  +  1 ) ) )
8960, 88syl 16 . . . . . . . . . . . . . 14  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) )  ->  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  <_  ( ( vol* `  A )  +  1 ) ) )
9086, 89mpani 676 . . . . . . . . . . . . 13  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  U. ran  ( (,)  o.  f ) )  <_ 
( ( vol* `  A )  +  1 )  ->  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) )  <_  ( ( vol* `  A )  +  1 ) ) )
9190ad4antlr 732 . . . . . . . . . . . 12  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  A  C_ 
U. ran  ( (,)  o.  f ) )  -> 
( ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol* `  A )  +  1 )  -> 
( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  <_ 
( ( vol* `  A )  +  1 ) ) )
9291impr 619 . . . . . . . . . . 11  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  <_ 
( ( vol* `  A )  +  1 ) )
93 ovolge0 20986 . . . . . . . . . . . 12  |-  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  RR  ->  0  <_  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
9480, 93ax-mp 5 . . . . . . . . . . 11  |-  0  <_  ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )
9592, 94jctil 537 . . . . . . . . . 10  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( 0  <_  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  /\  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) )  <_  ( ( vol* `  A )  +  1 ) ) )
96 xrrege0 11167 . . . . . . . . . 10  |-  ( ( ( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR )  /\  (
0  <_  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) )  /\  ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  <_ 
( ( vol* `  A )  +  1 ) ) )  -> 
( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
9784, 95, 96syl2anc 661 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
98 resubcl 9694 . . . . . . . . . . . . . 14  |-  ( ( ( vol* `  A )  e.  RR  /\  u  e.  RR )  ->  ( ( vol* `  A )  -  u )  e.  RR )
9998adantrr 716 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( vol* `  A )  -  u
)  e.  RR )
100 posdif 9853 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  RR  /\  ( vol* `  A
)  e.  RR )  ->  ( u  < 
( vol* `  A )  <->  0  <  ( ( vol* `  A )  -  u
) ) )
101100ancoms 453 . . . . . . . . . . . . . . 15  |-  ( ( ( vol* `  A )  e.  RR  /\  u  e.  RR )  ->  ( u  < 
( vol* `  A )  <->  0  <  ( ( vol* `  A )  -  u
) ) )
102101biimpd 207 . . . . . . . . . . . . . 14  |-  ( ( ( vol* `  A )  e.  RR  /\  u  e.  RR )  ->  ( u  < 
( vol* `  A )  ->  0  <  ( ( vol* `  A )  -  u
) ) )
103102impr 619 . . . . . . . . . . . . 13  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  0  <  ( ( vol* `  A )  -  u
) )
10499, 103elrpd 11046 . . . . . . . . . . . 12  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( vol* `  A )  -  u
)  e.  RR+ )
105104rphalfcld 11060 . . . . . . . . . . 11  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( ( vol* `  A )  -  u
)  /  2 )  e.  RR+ )
1063, 105sylan 471 . . . . . . . . . 10  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  ( ( ( vol* `  A
)  -  u )  /  2 )  e.  RR+ )
107106adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( ( ( vol* `  A )  -  u )  /  2
)  e.  RR+ )
108 eqid 2443 . . . . . . . . . . 11  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)
109108ovolgelb 20985 . . . . . . . . . 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 1301 . . . . . . . . 9  |-  ( ( ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR  /\  ( ( ( vol* `  A )  -  u
)  /  2 )  e.  RR+ )  ->  E. g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) ) )
11197, 107, 110syl2anc 661 . . . . . . . 8  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  ->  E. g  e.  (
(  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  sup ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) ) )
112 elmapi 7255 . . . . . . . . . . 11  |-  ( g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
113 ssid 3396 . . . . . . . . . . . . . 14  |-  U. ran  ( (,)  o.  g ) 
C_  U. ran  ( (,) 
o.  g )
114108ovollb 20984 . . . . . . . . . . . . . 14  |-  ( ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  U. ran  ( (,)  o.  g
)  C_  U. ran  ( (,)  o.  g ) )  ->  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  ) )
115113, 114mpan2 671 . . . . . . . . . . . . 13  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  ) )
116115adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( vol* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
) ,  RR* ,  <  ) )
117 eqid 2443 . . . . . . . . . . . . . . 15  |-  ( ( abs  o.  -  )  o.  g )  =  ( ( abs  o.  -  )  o.  g )
118117, 108ovolsf 20978 . . . . . . . . . . . . . 14  |-  ( g : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,) +oo ) )
119 frn 5586 . . . . . . . . . . . . . . 15  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  C_  ( 0 [,) +oo ) )
120119, 55syl6ss 3389 . . . . . . . . . . . . . 14  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
)  C_  RR* )
121 supxrcl 11298 . . . . . . . . . . . . . 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 10592 . . . . . . . . . . . . . . . . 17  |-  ( ( ( vol* `  A )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  ->  (
( ( vol* `  A )  -  u
)  /  2 )  e.  RR )
1243, 123sylan 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  ( ( ( vol* `  A
)  -  u )  /  2 )  e.  RR )
125124adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( ( ( vol* `  A )  -  u )  /  2
)  e.  RR )
12697, 125readdcld 9434 . . . . . . . . . . . . . 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 9454 . . . . . . . . . . . . 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 5121 . . . . . . . . . . . . . . . . 17  |-  ran  ( (,)  o.  g )  C_  ran  (,)
129128unissi 4135 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  g ) 
C_  U. ran  (,)
130129, 63sseqtr4i 3410 . . . . . . . . . . . . . . 15  |-  U. ran  ( (,)  o.  g ) 
C_  RR
131 ovolcl 20983 . . . . . . . . . . . . . . 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 11153 . . . . . . . . . . . . . 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 1301 . . . . . . . . . . . . 13  |-  ( ( sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  e.  RR*  /\  ( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) )  e.  RR* )  ->  ( ( ( vol* `  U. ran  ( (,)  o.  g
) )  <_  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  /\  sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
) ,  RR* ,  <  )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) )  ->  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
135122, 127, 134syl2anr 478 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( ( ( vol* `  U. ran  ( (,)  o.  g ) )  <_  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  g
) ) ,  RR* ,  <  )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) )  -> 
( vol* `  U. ran  ( (,)  o.  g ) )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) ) )
136116, 135mpand 675 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  g : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  -> 
( sup ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) )  ->  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
137112, 136sylan2 474 . . . . . . . . . 10  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  ( sup ( ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  g )
) ,  RR* ,  <  )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) )  ->  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
138137anim2d 565 . . . . . . . . 9  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )  ->  (
( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  g ) ) , 
RR* ,  <  )  <_ 
( ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  +  ( ( ( vol* `  A )  -  u )  /  2
) ) )  -> 
( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) ) )
139138reximdva 2849 . . . . . . . 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 2796 . . . . . . 7  |-  ( E. g  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) )  ->  E. g
( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
142140, 141syl 16 . . . . . 6  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  ->  E. g ( ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )
14359, 66jctil 537 . . . . . . . . . . . 12  |-  ( ( vol* `  A
)  e.  RR  ->  ( ( vol* `  U. ran  ( (,)  o.  f ) )  e. 
RR*  /\  ( ( vol* `  A )  +  1 )  e.  RR ) )
144143ad3antlr 730 . . . . . . . . . . 11  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  ( ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR*  /\  (
( vol* `  A )  +  1 )  e.  RR ) )
145 ovolge0 20986 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  C_  RR  ->  0  <_  ( vol* `  U. ran  ( (,) 
o.  f ) ) )
14664, 145ax-mp 5 . . . . . . . . . . . . 13  |-  0  <_  ( vol* `  U. ran  ( (,)  o.  f ) )
147146jctl 541 . . . . . . . . . . . 12  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 )  ->  ( 0  <_  ( vol* `  U. ran  ( (,) 
o.  f ) )  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
148147adantl 466 . . . . . . . . . . 11  |-  ( ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) )  ->  (
0  <_  ( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )
149 xrrege0 11167 . . . . . . . . . . 11  |-  ( ( ( ( vol* `  U. ran  ( (,) 
o.  f ) )  e.  RR*  /\  (
( vol* `  A )  +  1 )  e.  RR )  /\  ( 0  <_ 
( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
150144, 148, 149syl2an 477 . . . . . . . . . 10  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  -> 
( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
151150, 125resubcld 9797 . . . . . . . . 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 11076 . . . . . . . . 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 20362 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  e.  Top
154 retopbas 20361 . . . . . . . . . . . . 13  |-  ran  (,)  e. 
TopBases
155 bastg 18593 . . . . . . . . . . . . 13  |-  ( ran 
(,)  e.  TopBases  ->  ran  (,)  C_  ( topGen `  ran  (,) )
)
156154, 155ax-mp 5 . . . . . . . . . . . 12  |-  ran  (,)  C_  ( topGen `  ran  (,) )
15761, 156sstri 3386 . . . . . . . . . . 11  |-  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
158 uniopn 18532 . . . . . . . . . . 11  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
)
159153, 157, 158mp2an 672 . . . . . . . . . 10  |-  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
160 mblfinlem2 28455 . . . . . . . . . 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 1301 . . . . . . . . 9  |-  ( ( ( ( vol* `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  e.  RR  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  U. ran  ( (,)  o.  f ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  U.
ran  ( (,)  o.  f )  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  s ) ) )
162151, 152, 161syl2anc 661 . . . . . . . 8  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  U. ran  ( (,) 
o.  f )  /\  ( ( vol* `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) )
163162adantr 465 . . . . . . 7  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  U. ran  ( (,) 
o.  f )  /\  ( ( vol* `  U. ran  ( (,) 
o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) )
164 indif2 3614 . . . . . . . . . . . . . . 15  |-  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g ) ) )  =  ( ( s  i^i  RR )  \  U. ran  ( (,)  o.  g ) )
16522cldss 18655 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  s  C_  RR )
166 df-ss 3363 . . . . . . . . . . . . . . . . 17  |-  ( s 
C_  RR  <->  ( s  i^i 
RR )  =  s )
167165, 166sylib 196 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  RR )  =  s )
168167difeq1d 3494 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( (
s  i^i  RR )  \  U. ran  ( (,) 
o.  g ) )  =  ( s  \  U. ran  ( (,)  o.  g ) ) )
169164, 168syl5eq 2487 . . . . . . . . . . . . . 14  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g
) ) )  =  ( s  \  U. ran  ( (,)  o.  g
) ) )
170128, 156sstri 3386 . . . . . . . . . . . . . . . . 17  |-  ran  ( (,)  o.  g )  C_  ( topGen `  ran  (,) )
171 uniopn 18532 . . . . . . . . . . . . . . . . 17  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  g )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) )
)
172153, 170, 171mp2an 672 . . . . . . . . . . . . . . . 16  |-  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) )
17322opncld 18659 . . . . . . . . . . . . . . . 16  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  U. ran  ( (,)  o.  g )  e.  ( topGen `  ran  (,) ) )  ->  ( RR  \  U. ran  ( (,)  o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
174153, 172, 173mp2an 672 . . . . . . . . . . . . . . 15  |-  ( RR 
\  U. ran  ( (,) 
o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
)
175 incld 18669 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( RR  \ 
U. ran  ( (,)  o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )  ->  (
s  i^i  ( RR  \ 
U. ran  ( (,)  o.  g ) ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
176174, 175mpan2 671 . . . . . . . . . . . . . 14  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  i^i  ( RR  \  U. ran  ( (,)  o.  g
) ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
177169, 176eqeltrrd 2518 . . . . . . . . . . . . 13  |-  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( s  \  U. ran  ( (,) 
o.  g ) )  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )
178 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) )  ->  s  C_  U.
ran  ( (,)  o.  f ) )
179 simpl 457 . . . . . . . . . . . . . . 15  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) )  ->  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  g ) )
180178, 179ssdif2d 3516 . . . . . . . . . . . . . 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 3611 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  =  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) )
182 inss2 3592 . . . . . . . . . . . . . . 15  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  C_  A
183181, 182eqsstr3i 3408 . . . . . . . . . . . . . 14  |-  ( U. ran  ( (,)  o.  f
)  \  ( U. ran  ( (,)  o.  f
)  \  A )
)  C_  A
184180, 183syl6ss 3389 . . . . . . . . . . . . 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 3398 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( b  C_  A  <->  ( s  \  U. ran  ( (,)  o.  g ) )  C_  A )
)
186185anbi1d 704 . . . . . . . . . . . . . . 15  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )  <->  ( (
s  \  U. ran  ( (,)  o.  g ) ) 
C_  A  /\  ( vol `  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b
) ) ) )
187 fveq2 5712 . . . . . . . . . . . . . . . . 17  |-  ( ( s  \  U. ran  ( (,)  o.  g ) )  =  b  -> 
( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )
188187eqcoms 2446 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )
189188biantrud 507 . . . . . . . . . . . . . . 15  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( ( s  \  U. ran  ( (,)  o.  g ) )  C_  A 
<->  ( ( s  \  U. ran  ( (,)  o.  g ) )  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) ) )
190186, 189bitr4d 256 . . . . . . . . . . . . . 14  |-  ( b  =  ( s  \  U. ran  ( (,)  o.  g ) )  -> 
( ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) )  <->  ( s  \  U. ran  ( (,) 
o.  g ) ) 
C_  A ) )
191190rspcev 3094 . . . . . . . . . . . . 13  |-  ( ( ( s  \  U. ran  ( (,)  o.  g
) )  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  \  U. ran  ( (,)  o.  g
) )  C_  A
)  ->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) )
192177, 184, 191syl2an 477 . . . . . . . . . . . 12  |-  ( ( s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( ( U. ran  ( (,)  o.  f )  \  A
)  C_  U. ran  ( (,)  o.  g )  /\  s  C_  U. ran  ( (,)  o.  f ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) )
193192an12s 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 724 . . . . . . . . . 10  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( s  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( s  C_ 
U. ran  ( (,)  o.  f )  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  s ) ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  ( vol `  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b
) ) )
195194adantlr 714 . . . . . . . . 9  |-  ( ( ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) )  /\  (
s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( s  C_ 
U. ran  ( (,)  o.  f )  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  s ) ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  ( vol `  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b
) ) )
196195adantll 713 . . . . . . . 8  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  ( vol `  (
s  \  U. ran  ( (,)  o.  g ) ) )  =  ( vol `  b ) ) )
197 difss 3504 . . . . . . . . . . . 12  |-  ( A 
\  ( s  \  U. ran  ( (,)  o.  g ) ) ) 
C_  A
198 ovolsscl 20991 . . . . . . . . . . . 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 1301 . . . . . . . . . . 11  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  (
s  \  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
200199ad5antr 733 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  ( A  \ 
( s  \  U. ran  ( (,)  o.  g
) ) ) )  e.  RR )
201 simp-6r 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 457 . . . . . . . . . . 11  |-  ( ( u  e.  RR  /\  u  <  ( vol* `  A ) )  ->  u  e.  RR )
203202ad4antlr 732 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  u  e.  RR )
204 difdif2 3628 . . . . . . . . . . . 12  |-  ( A 
\  ( s  \  U. ran  ( (,)  o.  g ) ) )  =  ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) )
205204fveq2i 5715 . . . . . . . . . . 11  |-  ( vol* `  ( A  \  ( s  \  U. ran  ( (,)  o.  g
) ) ) )  =  ( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )
206 difss 3504 . . . . . . . . . . . . . . 15  |-  ( A 
\  s )  C_  A
207 inss1 3591 . . . . . . . . . . . . . . 15  |-  ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  A
208206, 207unssi 3552 . . . . . . . . . . . . . 14  |-  ( ( A  \  s )  u.  ( A  i^i  U.
ran  ( (,)  o.  g ) ) ) 
C_  A
209 ovolsscl 20991 . . . . . . . . . . . . . 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 1301 . . . . . . . . . . . . 13  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )  e.  RR )
211210ad5antr 733 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  e.  RR )
212 ovolsscl 20991 . . . . . . . . . . . . . . 15  |-  ( ( ( A  \  s
)  C_  A  /\  A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  s
) )  e.  RR )
213206, 212mp3an1 1301 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  \  s
) )  e.  RR )
214213ad5antr 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  ( A  \ 
s ) )  e.  RR )
215 ovolsscl 20991 . . . . . . . . . . . . . . 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 1301 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( A  i^i  U. ran  ( (,)  o.  g ) ) )  e.  RR )
217216ad5antr 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  ( A  i^i  U.
ran  ( (,)  o.  g ) ) )  e.  RR )
218214, 217readdcld 9434 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( ( vol* `  ( A 
\  s ) )  +  ( vol* `  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  e.  RR )
2193, 202, 98syl2an 477 . . . . . . . . . . . . 13  |-  ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  ->  ( ( vol* `  A )  -  u )  e.  RR )
220219ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( ( vol* `  A )  -  u )  e.  RR )
221 ssdifss 3508 . . . . . . . . . . . . . . 15  |-  ( A 
C_  RR  ->  ( A 
\  s )  C_  RR )
222221adantr 465 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( A  \  s
)  C_  RR )
223 ssinss1 3599 . . . . . . . . . . . . . . 15  |-  ( A 
C_  RR  ->  ( A  i^i  U. ran  ( (,)  o.  g ) ) 
C_  RR )
224223adantr 465 . . . . . . . . . . . . . 14  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( A  i^i  U. ran  ( (,)  o.  g
) )  C_  RR )
225 ovolun 21004 . . . . . . . . . . . . . 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 1219 . . . . . . . . . . . . 13  |-  ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  -> 
( vol* `  ( ( A  \ 
s )  u.  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) )  <_  (
( vol* `  ( A  \  s
) )  +  ( vol* `  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) ) )
227226ad5antr 733 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  ( ( A 
\  s )  u.  ( A  i^i  U. ran  ( (,)  o.  g
) ) ) )  <_  ( ( vol* `  ( A  \  s ) )  +  ( vol* `  ( A  i^i  U. ran  ( (,)  o.  g ) ) ) ) )
228124ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  -> 
( ( ( vol* `  A )  -  u )  /  2
)  e.  RR )
229228adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( (
( vol* `  A )  -  u
)  /  2 )  e.  RR )
230150ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )  <  ( vol* `  s ) ) ) )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
231 simprl 755 . . . . . . . . . . . . . . . . 17  |-  ( ( s  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( s  C_ 
U. ran  ( (,)  o.  f )  /\  (
( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A )  -  u )  /  2
) )  <  ( vol* `  s ) ) )  ->  s  C_ 
U. ran  ( (,)  o.  f ) )
232150adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A )
) )  /\  ( A  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  <_  (
( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  U.
ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,)  o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  -> 
( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
233 ovolsscl 20991 . . . . . . . . . . . . . . . . . 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 1302 . . . . . . . . . . . . . . . . 17  |-  ( ( s  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol* `  s )  e.  RR )
235231, 232, 234syl2anr 478 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( A  C_  RR  /\  ( vol* `  A )  e.  RR )  /\  A  e.  dom  vol )  /\  ( u  e.  RR  /\  u  <  ( vol* `  A ) ) )  /\  ( A  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  <_  ( ( vol* `  A )  +  1 ) ) )  /\  ( ( U. ran  ( (,) 
o.  f )  \  A )  C_  U. ran  ( (,)  o.  g )  /\  ( vol* `  U. ran  ( (,) 
o.  g ) )  <_  ( ( vol* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  +  ( ( ( vol* `  A )  -  u
)  /  2 ) ) ) )  /\  ( s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )  /\  ( s  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol* `  U. ran  ( (,)  o.  f ) )  -  ( ( ( vol* `  A
)  -  u )  /  2 ) )