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

Theorem mblfinlem3 26247
Description: The difference between two sets measurable by the criterion in ismblfin 26249 is itself measurable by the same. Corollary 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
Assertion
Ref Expression
mblfinlem3  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  /\  ( ( vol
* `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  /\  ( vol * `  B )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) ) )  ->  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  ( A  \  B )  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  =  ( vol * `  ( A  \  B ) ) )
Distinct variable groups:    y, b, A    B, b, y

Proof of Theorem mblfinlem3
Dummy variables  f 
s  u  v  w  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltso 9158 . . 3  |-  <  Or  RR
21a1i 11 . 2  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  /\  ( ( vol
* `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  /\  ( vol * `  B )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) ) )  ->  <  Or  RR )
3 difss 3476 . . . 4  |-  ( A 
\  B )  C_  A
4 ovolsscl 19384 . . . 4  |-  ( ( ( A  \  B
)  C_  A  /\  A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( A  \  B ) )  e.  RR )
53, 4mp3an1 1267 . . 3  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( vol * `  ( A  \  B ) )  e.  RR )
653ad2ant1 979 . 2  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  /\  ( ( vol
* `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  /\  ( vol * `  B )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) ) )  ->  ( vol * `  ( A  \  B
) )  e.  RR )
7 vex 2961 . . . . . 6  |-  u  e. 
_V
8 eqeq1 2444 . . . . . . . 8  |-  ( y  =  u  ->  (
y  =  ( vol `  b )  <->  u  =  ( vol `  b ) ) )
98anbi2d 686 . . . . . . 7  |-  ( y  =  u  ->  (
( b  C_  ( A  \  B )  /\  y  =  ( vol `  b ) )  <->  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )
109rexbidv 2728 . . . . . 6  |-  ( y  =  u  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  ( A  \  B )  /\  y  =  ( vol `  b
) )  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  ( A  \  B )  /\  u  =  ( vol `  b ) ) ) )
117, 10elab 3084 . . . . 5  |-  ( u  e.  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  ( A  \  B )  /\  y  =  ( vol `  b
) ) }  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  ( A  \  B )  /\  u  =  ( vol `  b ) ) )
12 simprl 734 . . . . . . . . 9  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) )  ->  b  C_  ( A  \  B
) )
13 ssdifss 3480 . . . . . . . . 9  |-  ( A 
C_  RR  ->  ( A 
\  B )  C_  RR )
14 ovolss 19383 . . . . . . . . 9  |-  ( ( b  C_  ( A  \  B )  /\  ( A  \  B )  C_  RR )  ->  ( vol
* `  b )  <_  ( vol * `  ( A  \  B ) ) )
1512, 13, 14syl2anr 466 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )  -> 
( vol * `  b )  <_  ( vol * `  ( A 
\  B ) ) )
16 uniretop 18798 . . . . . . . . . . . . 13  |-  RR  =  U. ( topGen `  ran  (,) )
1716cldss 17095 . . . . . . . . . . . 12  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
18 ovolcl 19376 . . . . . . . . . . . 12  |-  ( b 
C_  RR  ->  ( vol
* `  b )  e.  RR* )
1917, 18syl 16 . . . . . . . . . . 11  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol * `
 b )  e. 
RR* )
20 ovolcl 19376 . . . . . . . . . . . 12  |-  ( ( A  \  B ) 
C_  RR  ->  ( vol
* `  ( A  \  B ) )  e. 
RR* )
2113, 20syl 16 . . . . . . . . . . 11  |-  ( A 
C_  RR  ->  ( vol
* `  ( A  \  B ) )  e. 
RR* )
22 xrlenlt 9145 . . . . . . . . . . 11  |-  ( ( ( vol * `  b )  e.  RR*  /\  ( vol * `  ( A  \  B ) )  e.  RR* )  ->  ( ( vol * `  b )  <_  ( vol * `  ( A 
\  B ) )  <->  -.  ( vol * `  ( A  \  B ) )  <  ( vol
* `  b )
) )
2319, 21, 22syl2anr 466 . . . . . . . . . 10  |-  ( ( A  C_  RR  /\  b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) )  ->  (
( vol * `  b )  <_  ( vol * `  ( A 
\  B ) )  <->  -.  ( vol * `  ( A  \  B ) )  <  ( vol
* `  b )
) )
2423adantrr 699 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )  -> 
( ( vol * `  b )  <_  ( vol * `  ( A 
\  B ) )  <->  -.  ( vol * `  ( A  \  B ) )  <  ( vol
* `  b )
) )
25 id 21 . . . . . . . . . . . . . 14  |-  ( u  =  ( vol `  b
)  ->  u  =  ( vol `  b ) )
26 dfss4 3577 . . . . . . . . . . . . . . . . 17  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
2717, 26sylib 190 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
28 rembl 19437 . . . . . . . . . . . . . . . . 17  |-  RR  e.  dom  vol
2916cldopn 17097 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
30 opnmbl 19496 . . . . . . . . . . . . . . . . . 18  |-  ( ( RR  \  b )  e.  ( topGen `  ran  (,) )  ->  ( RR  \  b )  e.  dom  vol )
3129, 30syl 16 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  dom  vol )
32 difmbl 19439 . . . . . . . . . . . . . . . . 17  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  b
)  e.  dom  vol )  ->  ( RR  \ 
( RR  \  b
) )  e.  dom  vol )
3328, 31, 32sylancr 646 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  e.  dom  vol )
3427, 33eqeltrrd 2513 . . . . . . . . . . . . . . 15  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
35 mblvol 19428 . . . . . . . . . . . . . . 15  |-  ( b  e.  dom  vol  ->  ( vol `  b )  =  ( vol * `  b ) )
3634, 35syl 16 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  b )  =  ( vol * `  b
) )
3725, 36sylan9eqr 2492 . . . . . . . . . . . . 13  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  u  =  ( vol `  b ) )  ->  u  =  ( vol * `  b
) )
3837breq2d 4226 . . . . . . . . . . . 12  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  u  =  ( vol `  b ) )  ->  ( ( vol * `  ( A 
\  B ) )  <  u  <->  ( vol * `
 ( A  \  B ) )  < 
( vol * `  b ) ) )
3938notbid 287 . . . . . . . . . . 11  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  u  =  ( vol `  b ) )  ->  ( -.  ( vol * `  ( A  \  B ) )  <  u  <->  -.  ( vol * `  ( A 
\  B ) )  <  ( vol * `  b ) ) )
4039adantrl 698 . . . . . . . . . 10  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) )  ->  ( -.  ( vol * `  ( A  \  B ) )  <  u  <->  -.  ( vol * `  ( A 
\  B ) )  <  ( vol * `  b ) ) )
4140adantl 454 . . . . . . . . 9  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )  -> 
( -.  ( vol
* `  ( A  \  B ) )  < 
u  <->  -.  ( vol * `
 ( A  \  B ) )  < 
( vol * `  b ) ) )
4224, 41bitr4d 249 . . . . . . . 8  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )  -> 
( ( vol * `  b )  <_  ( vol * `  ( A 
\  B ) )  <->  -.  ( vol * `  ( A  \  B ) )  <  u ) )
4315, 42mpbid 203 . . . . . . 7  |-  ( ( A  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  ( A  \  B
)  /\  u  =  ( vol `  b ) ) ) )  ->  -.  ( vol * `  ( A  \  B ) )  <  u )
4443rexlimdvaa 2833 . . . . . 6  |-  ( A 
C_  RR  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  ( A  \  B )  /\  u  =  ( vol `  b ) )  ->  -.  ( vol * `  ( A 
\  B ) )  <  u ) )
4544imp 420 . . . . 5  |-  ( ( A  C_  RR  /\  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  ( A  \  B )  /\  u  =  ( vol `  b ) ) )  ->  -.  ( vol * `  ( A  \  B ) )  <  u )
4611, 45sylan2b 463 . . . 4  |-  ( ( A  C_  RR  /\  u  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  ( A  \  B )  /\  y  =  ( vol `  b ) ) } )  ->  -.  ( vol * `  ( A  \  B ) )  <  u )
4746adantlr 697 . . 3  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  u  e.  {
y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  ( A  \  B )  /\  y  =  ( vol `  b ) ) } )  ->  -.  ( vol * `  ( A  \  B ) )  <  u )
48473ad2antl1 1120 . 2  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  /\  ( ( vol
* `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  /\  ( vol * `  B )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) ) )  /\  u  e.  {
y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  ( A  \  B )  /\  y  =  ( vol `  b ) ) } )  ->  -.  ( vol * `  ( A  \  B ) )  <  u )
49 simplr 733 . . . . . . . . . . . . . . 15  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( vol * `  A )  e.  RR )
50 resubcl 9367 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  u  e.  RR )  ->  ( ( vol * `  ( A  \  B
) )  -  u
)  e.  RR )
5150adantrr 699 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  ( A  \  B ) ) ) )  ->  ( ( vol * `  ( A 
\  B ) )  -  u )  e.  RR )
52 posdif 9523 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( u  e.  RR  /\  ( vol * `  ( A  \  B ) )  e.  RR )  -> 
( u  <  ( vol * `  ( A 
\  B ) )  <->  0  <  ( ( vol * `  ( A  \  B ) )  -  u ) ) )
5352ancoms 441 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  u  e.  RR )  ->  ( u  <  ( vol * `  ( A 
\  B ) )  <->  0  <  ( ( vol * `  ( A  \  B ) )  -  u ) ) )
5453biimpd 200 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  u  e.  RR )  ->  ( u  <  ( vol * `  ( A 
\  B ) )  ->  0  <  (
( vol * `  ( A  \  B ) )  -  u ) ) )
5554impr 604 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  ( A  \  B ) ) ) )  ->  0  <  ( ( vol * `  ( A  \  B ) )  -  u ) )
5651, 55elrpd 10648 . . . . . . . . . . . . . . . . 17  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  ( A  \  B ) ) ) )  ->  ( ( vol * `  ( A 
\  B ) )  -  u )  e.  RR+ )
57 3nn 10136 . . . . . . . . . . . . . . . . . 18  |-  3  e.  NN
58 nnrp 10623 . . . . . . . . . . . . . . . . . 18  |-  ( 3  e.  NN  ->  3  e.  RR+ )
5957, 58ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  3  e.  RR+
60 rpdivcl 10636 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( vol * `  ( A  \  B
) )  -  u
)  e.  RR+  /\  3  e.  RR+ )  ->  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 )  e.  RR+ )
6156, 59, 60sylancl 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( vol * `  ( A  \  B ) )  e.  RR  /\  ( u  e.  RR  /\  u  <  ( vol
* `  ( A  \  B ) ) ) )  ->  ( (
( vol * `  ( A  \  B ) )  -  u )  /  3 )  e.  RR+ )
625, 61sylan 459 . . . . . . . . . . . . . . 15  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( ( ( vol
* `  ( A  \  B ) )  -  u )  /  3
)  e.  RR+ )
6349, 62ltsubrpd 10678 . . . . . . . . . . . . . 14  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol
* `  A )
)
6463adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  -> 
( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol
* `  A )
)
65 simpr 449 . . . . . . . . . . . . 13  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  -> 
( vol * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )
6664, 65breqtrd 4238 . . . . . . . . . . . 12  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  -> 
( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )
67 reex 9083 . . . . . . . . . . . . . . . . . 18  |-  RR  e.  _V
6867ssex 4349 . . . . . . . . . . . . . . . . 17  |-  ( A 
C_  RR  ->  A  e. 
_V )
6968adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  ->  A  e.  _V )
70 sseq1 3371 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  A  ->  (
v  C_  RR  <->  A  C_  RR ) )
71 fveq2 5730 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  =  A  ->  ( vol * `  v )  =  ( vol * `  A ) )
7271eleq1d 2504 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  A  ->  (
( vol * `  v )  e.  RR  <->  ( vol * `  A
)  e.  RR ) )
7370, 72anbi12d 693 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  A  ->  (
( v  C_  RR  /\  ( vol * `  v )  e.  RR ) 
<->  ( A  C_  RR  /\  ( vol * `  A )  e.  RR ) ) )
74 sseq2 3372 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  =  A  ->  (
b  C_  v  <->  b  C_  A ) )
7574anbi1d 687 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  =  A  ->  (
( b  C_  v  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  y  =  ( vol `  b ) ) ) )
7675rexbidv 2728 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  =  A  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  v  /\  y  =  ( vol `  b
) )  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) ) )
7776abbidv 2552 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  =  A  ->  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =  {
y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } )
7877sseq1d 3377 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  A  ->  ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  C_  RR  <->  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  C_  RR ) )
7977neeq1d 2616 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  A  ->  ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/)  <->  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  =/=  (/) ) )
8077raleqdv 2912 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  =  A  ->  ( A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x 
<-> 
A. z  e.  {
y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } z  <_  x ) )
8180rexbidv 2728 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  A  ->  ( E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x 
<->  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } z  <_  x ) )
8278, 79, 813anbi123d 1255 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  A  ->  (
( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  v  /\  y  =  ( vol `  b ) ) } 
C_  RR  /\  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x )  <->  ( {
y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  C_  RR  /\ 
{ y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } z  <_  x ) ) )
8373, 82imbi12d 313 . . . . . . . . . . . . . . . . 17  |-  ( v  =  A  ->  (
( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  ->  ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  C_  RR  /\ 
{ y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x ) )  <->  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) } 
C_  RR  /\  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } z  <_  x ) ) ) )
84 simpr 449 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  C_  v  /\  y  =  ( vol `  b ) )  -> 
y  =  ( vol `  b ) )
8584, 36sylan9eqr 2492 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  y  =  ( vol `  b
) ) )  -> 
y  =  ( vol
* `  b )
)
8685adantl 454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  /\  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( b  C_  v  /\  y  =  ( vol `  b
) ) ) )  ->  y  =  ( vol * `  b
) )
87 simprl 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  y  =  ( vol `  b
) ) )  -> 
b  C_  v )
88 ovolsscl 19384 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( b  C_  v  /\  v  C_  RR  /\  ( vol * `  v )  e.  RR )  -> 
( vol * `  b )  e.  RR )
89883expb 1155 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  C_  v  /\  ( v  C_  RR  /\  ( vol * `  v )  e.  RR ) )  ->  ( vol * `  b )  e.  RR )
9089ancoms 441 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  /\  b  C_  v
)  ->  ( vol * `
 b )  e.  RR )
9187, 90sylan2 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  /\  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( b  C_  v  /\  y  =  ( vol `  b
) ) ) )  ->  ( vol * `  b )  e.  RR )
9286, 91eqeltrd 2512 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  /\  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( b  C_  v  /\  y  =  ( vol `  b
) ) ) )  ->  y  e.  RR )
9392rexlimdvaa 2833 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  -> 
( E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) )  ->  y  e.  RR ) )
9493abssdv 3419 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  ->  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  C_  RR )
95 retop 18797 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( topGen ` 
ran  (,) )  e.  Top
96 0cld 17104 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
9795, 96ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )
98 0ss 3658 . . . . . . . . . . . . . . . . . . . . . 22  |-  (/)  C_  v
99 0mbl 19436 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (/)  e.  dom  vol
100 mblvol 19428 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol * `  (/) ) )
10199, 100ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( vol `  (/) )  =  ( vol * `  (/) )
102 ovol0 19391 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( vol
* `  (/) )  =  0
103101, 102eqtr2i 2459 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  =  ( vol `  (/) )
10498, 103pm3.2i 443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (/)  C_  v  /\  0  =  ( vol `  (/) ) )
105 sseq1 3371 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  (/)  ->  ( b 
C_  v  <->  (/)  C_  v
) )
106 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  =  (/)  ->  ( vol `  b )  =  ( vol `  (/) ) )
107106eqeq2d 2449 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  (/)  ->  ( 0  =  ( vol `  b
)  <->  0  =  ( vol `  (/) ) ) )
108105, 107anbi12d 693 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  (/)  ->  ( ( b  C_  v  /\  0  =  ( vol `  b ) )  <->  ( (/)  C_  v  /\  0  =  ( vol `  (/) ) ) ) )
109108rspcev 3054 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
(/)  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( (/)  C_  v  /\  0  =  ( vol `  (/) ) ) )  ->  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  v  /\  0  =  ( vol `  b ) ) )
11097, 104, 109mp2an 655 . . . . . . . . . . . . . . . . . . . 20  |-  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  0  =  ( vol `  b ) )
111 c0ex 9087 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  _V
112 eqeq1 2444 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  0  ->  (
y  =  ( vol `  b )  <->  0  =  ( vol `  b ) ) )
113112anbi2d 686 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  0  ->  (
( b  C_  v  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  v  /\  0  =  ( vol `  b ) ) ) )
114113rexbidv 2728 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  0  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  v  /\  y  =  ( vol `  b
) )  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  0  =  ( vol `  b ) ) ) )
115111, 114spcev 3045 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  0  =  ( vol `  b ) )  ->  E. y E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  v  /\  y  =  ( vol `  b
) ) )
116110, 115ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  E. y E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  v  /\  y  =  ( vol `  b
) )
117 abn0 3648 . . . . . . . . . . . . . . . . . . . 20  |-  ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/)  <->  E. y E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  v  /\  y  =  ( vol `  b
) ) )
118117biimpri 199 . . . . . . . . . . . . . . . . . . 19  |-  ( E. y E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) )  ->  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/) )
119116, 118mp1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  ->  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/) )
120 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( b  C_  v  /\  z  =  ( vol `  b ) )  -> 
z  =  ( vol `  b ) )
121120, 36sylan9eqr 2492 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  z  =  ( vol `  b
) ) )  -> 
z  =  ( vol
* `  b )
)
122121adantl 454 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  z  =  ( vol `  b
) ) ) )  ->  z  =  ( vol * `  b
) )
123 simprl 734 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  z  =  ( vol `  b
) ) )  -> 
b  C_  v )
124 ovolss 19383 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( b  C_  v  /\  v  C_  RR )  -> 
( vol * `  b )  <_  ( vol * `  v ) )
125124ancoms 441 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( v  C_  RR  /\  b  C_  v )  ->  ( vol * `  b )  <_  ( vol * `  v ) )
126123, 125sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  z  =  ( vol `  b
) ) ) )  ->  ( vol * `  b )  <_  ( vol * `  v ) )
127122, 126eqbrtrd 4234 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  C_  RR  /\  (
b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  v  /\  z  =  ( vol `  b
) ) ) )  ->  z  <_  ( vol * `  v ) )
128127rexlimdvaa 2833 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v 
C_  RR  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  z  =  ( vol `  b ) )  ->  z  <_  ( vol * `  v
) ) )
129128alrimiv 1642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v 
C_  RR  ->  A. z
( E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  z  =  ( vol `  b ) )  ->  z  <_  ( vol * `  v
) ) )
130 eqeq1 2444 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  z  ->  (
y  =  ( vol `  b )  <->  z  =  ( vol `  b ) ) )
131130anbi2d 686 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  z  ->  (
( b  C_  v  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  v  /\  z  =  ( vol `  b ) ) ) )
132131rexbidv 2728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  z  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  v  /\  y  =  ( vol `  b
) )  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  z  =  ( vol `  b ) ) ) )
133132ralab 3097 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. z  e.  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  ( vol * `
 v )  <->  A. z
( E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  z  =  ( vol `  b ) )  ->  z  <_  ( vol * `  v
) ) )
134129, 133sylibr 205 . . . . . . . . . . . . . . . . . . . 20  |-  ( v 
C_  RR  ->  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_ 
( vol * `  v ) )
135 breq2 4218 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( vol * `  v )  ->  (
z  <_  x  <->  z  <_  ( vol * `  v
) ) )
136135ralbidv 2727 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( vol * `  v )  ->  ( A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x 
<-> 
A. z  e.  {
y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_ 
( vol * `  v ) ) )
137136rspcev 3054 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( vol * `  v )  e.  RR  /\ 
A. z  e.  {
y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_ 
( vol * `  v ) )  ->  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x )
138134, 137sylan2 462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( vol * `  v )  e.  RR  /\  v  C_  RR )  ->  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x )
139138ancoms 441 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  ->  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x )
14094, 119, 1393jca 1135 . . . . . . . . . . . . . . . . 17  |-  ( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  -> 
( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  v  /\  y  =  ( vol `  b ) ) } 
C_  RR  /\  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x ) )
14183, 140vtoclg 3013 . . . . . . . . . . . . . . . 16  |-  ( A  e.  _V  ->  (
( A  C_  RR  /\  ( vol * `  A )  e.  RR )  ->  ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  C_  RR  /\ 
{ y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } z  <_  x ) ) )
14269, 141mpcom 35 . . . . . . . . . . . . . . 15  |-  ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  -> 
( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) } 
C_  RR  /\  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } z  <_  x ) )
143142adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) } 
C_  RR  /\  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } z  <_  x ) )
14462rpred 10650 . . . . . . . . . . . . . . 15  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( ( ( vol
* `  ( A  \  B ) )  -  u )  /  3
)  e.  RR )
14549, 144resubcld 9467 . . . . . . . . . . . . . 14  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  e.  RR )
146 suprlub 9972 . . . . . . . . . . . . . 14  |-  ( ( ( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) } 
C_  RR  /\  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } z  <_  x )  /\  (
( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  e.  RR )  ->  ( ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  <->  E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v ) )
147143, 145, 146syl2anc 644 . . . . . . . . . . . . 13  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  <  sup ( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  <->  E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v ) )
148147adantr 453 . . . . . . . . . . . 12  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  -> 
( ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  <  sup ( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  <->  E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v ) )
14966, 148mpbid 203 . . . . . . . . . . 11  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  ->  E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v )
150 eqeq1 2444 . . . . . . . . . . . . . . 15  |-  ( y  =  v  ->  (
y  =  ( vol `  b )  <->  v  =  ( vol `  b ) ) )
151150anbi2d 686 . . . . . . . . . . . . . 14  |-  ( y  =  v  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  v  =  ( vol `  b ) ) ) )
152151rexbidv 2728 . . . . . . . . . . . . 13  |-  ( y  =  v  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  y  =  ( vol `  b
) )  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  v  =  ( vol `  b ) ) ) )
153152rexab 3099 . . . . . . . . . . . 12  |-  ( E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v  <->  E. v
( E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  v  =  ( vol `  b ) )  /\  ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v ) )
154 breq2 4218 . . . . . . . . . . . . . . . . 17  |-  ( v  =  ( vol `  b
)  ->  ( (
( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  v  <->  ( ( vol * `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
) ) )
155154ad2antll 711 . . . . . . . . . . . . . . . 16  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  v  =  ( vol `  b
) ) )  -> 
( ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
v  <->  ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
) ) )
156 sseq1 3371 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  b  ->  (
s  C_  A  <->  b  C_  A ) )
157 fveq2 5730 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  b  ->  ( vol `  s )  =  ( vol `  b
) )
158157breq2d 4226 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  b  ->  (
( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  s )  <->  ( ( vol * `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
) ) )
159156, 158anbi12d 693 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  b  ->  (
( s  C_  A  /\  ( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  s ) )  <->  ( b  C_  A  /\  ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  ( vol `  b
) ) ) )
160159rspcev 3054 . . . . . . . . . . . . . . . . . 18  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  ( vol `  b
) ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  A  /\  (
( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  s ) ) )
161160expr 600 . . . . . . . . . . . . . . . . 17  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  b  C_  A )  ->  (
( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  b )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  s
) ) ) )
162161adantrr 699 . . . . . . . . . . . . . . . 16  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  v  =  ( vol `  b
) ) )  -> 
( ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
)  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  s
) ) ) )
163155, 162sylbid 208 . . . . . . . . . . . . . . 15  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  A  /\  v  =  ( vol `  b
) ) )  -> 
( ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
v  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  s
) ) ) )
164163rexlimiva 2827 . . . . . . . . . . . . . 14  |-  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  v  =  ( vol `  b ) )  ->  ( (
( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  v  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  A  /\  (
( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  s ) ) ) )
165164imp 420 . . . . . . . . . . . . 13  |-  ( ( E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  A  /\  v  =  ( vol `  b ) )  /\  ( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  v )  ->  E. s  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( s  C_  A  /\  ( ( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  s ) ) )
166165exlimiv 1645 . . . . . . . . . . . 12  |-  ( E. v ( E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  v  =  ( vol `  b ) )  /\  ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  A  /\  (
( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  s ) ) )
167153, 166sylbi 189 . . . . . . . . . . 11  |-  ( E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  A
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  s
) ) )
168149, 167syl 16 . . . . . . . . . 10  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  A  /\  (
( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  s ) ) )
169168ex 425 . . . . . . . . 9  |-  ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  -> 
( ( vol * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  s
) ) ) )
170169adantlr 697 . . . . . . . 8  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( ( vol
* `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  s
) ) ) )
171 simplrr 739 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( vol * `  B )  e.  RR )
17262adantlr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 )  e.  RR+ )
173171, 172ltsubrpd 10678 . . . . . . . . . . . . 13  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol * `  B ) )
174173adantr 453 . . . . . . . . . . . 12  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B
)  e.  RR ) )  /\  ( u  e.  RR  /\  u  <  ( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  B
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  -> 
( ( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol
* `  B )
)
175 simpr 449 . . . . . . . . . . . 12  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B
)  e.  RR ) )  /\  ( u  e.  RR  /\  u  <  ( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  B
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  -> 
( vol * `  B )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )
176174, 175breqtrd 4238 . . . . . . . . . . 11  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B
)  e.  RR ) )  /\  ( u  e.  RR  /\  u  <  ( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  B
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  -> 
( ( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )
17767ssex 4349 . . . . . . . . . . . . . . . 16  |-  ( B 
C_  RR  ->  B  e. 
_V )
178177adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  ->  B  e.  _V )
179 sseq1 3371 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  B  ->  (
v  C_  RR  <->  B  C_  RR ) )
180 fveq2 5730 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  B  ->  ( vol * `  v )  =  ( vol * `  B ) )
181180eleq1d 2504 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  B  ->  (
( vol * `  v )  e.  RR  <->  ( vol * `  B
)  e.  RR ) )
182179, 181anbi12d 693 . . . . . . . . . . . . . . . . 17  |-  ( v  =  B  ->  (
( v  C_  RR  /\  ( vol * `  v )  e.  RR ) 
<->  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) ) )
183 sseq2 3372 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  =  B  ->  (
b  C_  v  <->  b  C_  B ) )
184183anbi1d 687 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  =  B  ->  (
( b  C_  v  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  B  /\  y  =  ( vol `  b ) ) ) )
185184rexbidv 2728 . . . . . . . . . . . . . . . . . . . 20  |-  ( v  =  B  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  v  /\  y  =  ( vol `  b
) )  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) ) )
186185abbidv 2552 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  B  ->  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =  {
y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } )
187186sseq1d 3377 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  B  ->  ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  C_  RR  <->  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  C_  RR ) )
188186neeq1d 2616 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  B  ->  ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/)  <->  { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  =/=  (/) ) )
189186raleqdv 2912 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  B  ->  ( A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x 
<-> 
A. z  e.  {
y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } z  <_  x ) )
190189rexbidv 2728 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  B  ->  ( E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x 
<->  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } z  <_  x ) )
191187, 188, 1903anbi123d 1255 . . . . . . . . . . . . . . . . 17  |-  ( v  =  B  ->  (
( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  v  /\  y  =  ( vol `  b ) ) } 
C_  RR  /\  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x )  <->  ( {
y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  C_  RR  /\ 
{ y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } z  <_  x ) ) )
192182, 191imbi12d 313 . . . . . . . . . . . . . . . 16  |-  ( v  =  B  ->  (
( ( v  C_  RR  /\  ( vol * `  v )  e.  RR )  ->  ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  C_  RR  /\ 
{ y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  v  /\  y  =  ( vol `  b ) ) } z  <_  x ) )  <->  ( ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  -> 
( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  B  /\  y  =  ( vol `  b ) ) } 
C_  RR  /\  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } z  <_  x ) ) ) )
193192, 140vtoclg 3013 . . . . . . . . . . . . . . 15  |-  ( B  e.  _V  ->  (
( B  C_  RR  /\  ( vol * `  B )  e.  RR )  ->  ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  C_  RR  /\ 
{ y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } z  <_  x ) ) )
194178, 193mpcom 35 . . . . . . . . . . . . . 14  |-  ( ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  -> 
( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  B  /\  y  =  ( vol `  b ) ) } 
C_  RR  /\  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } z  <_  x ) )
195194ad2antlr 709 . . . . . . . . . . . . 13  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  C_  RR  /\ 
{ y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } z  <_  x ) )
196144adantlr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 )  e.  RR )
197171, 196resubcld 9467 . . . . . . . . . . . . 13  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  e.  RR )
198 suprlub 9972 . . . . . . . . . . . . 13  |-  ( ( ( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  B  /\  y  =  ( vol `  b ) ) } 
C_  RR  /\  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  =/=  (/)  /\  E. x  e.  RR  A. z  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } z  <_  x )  /\  (
( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  e.  RR )  ->  ( ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  <->  E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v ) )
199195, 197, 198syl2anc 644 . . . . . . . . . . . 12  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  <->  E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v ) )
200199adantr 453 . . . . . . . . . . 11  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B
)  e.  RR ) )  /\  ( u  e.  RR  /\  u  <  ( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  B
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  -> 
( ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  <  sup ( { y  |  E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  <->  E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v ) )
201176, 200mpbid 203 . . . . . . . . . 10  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B
)  e.  RR ) )  /\  ( u  e.  RR  /\  u  <  ( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  B
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  ->  E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v )
202150anbi2d 686 . . . . . . . . . . . . 13  |-  ( y  =  v  ->  (
( b  C_  B  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  B  /\  v  =  ( vol `  b ) ) ) )
203202rexbidv 2728 . . . . . . . . . . . 12  |-  ( y  =  v  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  B  /\  y  =  ( vol `  b
) )  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  v  =  ( vol `  b ) ) ) )
204203rexab 3099 . . . . . . . . . . 11  |-  ( E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v  <->  E. v
( E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  v  =  ( vol `  b ) )  /\  ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v ) )
205 breq2 4218 . . . . . . . . . . . . . . . 16  |-  ( v  =  ( vol `  b
)  ->  ( (
( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  v  <->  ( ( vol * `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
) ) )
206205ad2antll 711 . . . . . . . . . . . . . . 15  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  B  /\  v  =  ( vol `  b
) ) )  -> 
( ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
v  <->  ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
) ) )
207 sseq1 3371 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  b  ->  (
w  C_  B  <->  b  C_  B ) )
208 fveq2 5730 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  b  ->  ( vol `  w )  =  ( vol `  b
) )
209208breq2d 4226 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  b  ->  (
( ( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  w )  <->  ( ( vol * `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
) ) )
210207, 209anbi12d 693 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  b  ->  (
( w  C_  B  /\  ( ( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  w ) )  <->  ( b  C_  B  /\  ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  ( vol `  b
) ) ) )
211210rspcev 3054 . . . . . . . . . . . . . . . . 17  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  B  /\  ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  ( vol `  b
) ) )  ->  E. w  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( w 
C_  B  /\  (
( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  w ) ) )
212211expr 600 . . . . . . . . . . . . . . . 16  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  b  C_  B )  ->  (
( ( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  b )  ->  E. w  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( w  C_  B  /\  ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  w
) ) ) )
213212adantrr 699 . . . . . . . . . . . . . . 15  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  B  /\  v  =  ( vol `  b
) ) )  -> 
( ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  b
)  ->  E. w  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( w  C_  B  /\  ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  w
) ) ) )
214206, 213sylbid 208 . . . . . . . . . . . . . 14  |-  ( ( b  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( b  C_  B  /\  v  =  ( vol `  b
) ) )  -> 
( ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
v  ->  E. w  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( w  C_  B  /\  ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  w
) ) ) )
215214rexlimiva 2827 . . . . . . . . . . . . 13  |-  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  v  =  ( vol `  b ) )  ->  ( (
( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  v  ->  E. w  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( w 
C_  B  /\  (
( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  w ) ) ) )
216215imp 420 . . . . . . . . . . . 12  |-  ( ( E. b  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( b  C_  B  /\  v  =  ( vol `  b ) )  /\  ( ( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  v )  ->  E. w  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( w  C_  B  /\  ( ( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  w ) ) )
217216exlimiv 1645 . . . . . . . . . . 11  |-  ( E. v ( E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  v  =  ( vol `  b ) )  /\  ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v )  ->  E. w  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( w 
C_  B  /\  (
( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  w ) ) )
218204, 217sylbi 189 . . . . . . . . . 10  |-  ( E. v  e.  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) }  ( ( vol * `  B
)  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  /  3 ) )  <  v  ->  E. w  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( w  C_  B  /\  ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  w
) ) )
219201, 218syl 16 . . . . . . . . 9  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B
)  e.  RR ) )  /\  ( u  e.  RR  /\  u  <  ( vol * `  ( A  \  B ) ) ) )  /\  ( vol * `  B
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  ->  E. w  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( w 
C_  B  /\  (
( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  w ) ) )
220219ex 425 . . . . . . . 8  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( ( vol
* `  B )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  ->  E. w  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( w  C_  B  /\  ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  w
) ) ) )
221170, 220anim12d 548 . . . . . . 7  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( ( ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  /\  ( vol * `  B )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  -> 
( E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  s
) )  /\  E. w  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( w  C_  B  /\  ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  w
) ) ) ) )
222 reeanv 2877 . . . . . . 7  |-  ( E. s  e.  ( Clsd `  ( topGen `  ran  (,) )
) E. w  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( ( s 
C_  A  /\  (
( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  s ) )  /\  ( w  C_  B  /\  ( ( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  w ) ) )  <-> 
( E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  ( ( vol
* `  A )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  s
) )  /\  E. w  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( w  C_  B  /\  ( ( vol
* `  B )  -  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) )  < 
( vol `  w
) ) ) )
223221, 222syl6ibr 220 . . . . . 6  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  ( ( ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  /\  ( vol * `  B )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  B  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) E. w  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( ( s 
C_  A  /\  (
( vol * `  A )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  s ) )  /\  ( w  C_  B  /\  ( ( vol * `  B )  -  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) )  <  ( vol `  w ) ) ) ) )
224 eqid 2438 . . . . . . . . . . . . . 14  |-  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
225224ovolgelb 19378 . . . . . . . . . . . . 13  |-  ( ( B  C_  RR  /\  ( vol * `  B )  e.  RR  /\  (
( ( vol * `  ( A  \  B
) )  -  u
)  /  3 )  e.  RR+ )  ->  E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( B  C_  U.
ran  ( (,)  o.  f )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  B )  +  ( ( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) ) ) )
2262253expa 1154 . . . . . . . . . . . 12  |-  ( ( ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  /\  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 )  e.  RR+ )  ->  E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( B  C_  U. ran  ( (,)  o.  f )  /\  sup ( ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
) ,  RR* ,  <  )  <_  ( ( vol
* `  B )  +  ( ( ( vol * `  ( A  \  B ) )  -  u )  / 
3 ) ) ) )
22762, 226sylan2 462 . . . . . . . . . . 11  |-  ( ( ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  /\  ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  <  ( vol
* `  ( A  \  B ) ) ) ) )  ->  E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( B  C_  U.
ran  ( (,)  o.  f )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  B )  +  ( ( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) ) ) )
228227ancoms 441 . . . . . . . . . 10  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( u  e.  RR  /\  u  < 
( vol * `  ( A  \  B ) ) ) )  /\  ( B  C_  RR  /\  ( vol * `  B
)  e.  RR ) )  ->  E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( B  C_  U.
ran  ( (,)  o.  f )  /\  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  <_ 
( ( vol * `  B )  +  ( ( ( vol * `  ( A  \  B
) )  -  u
)  /  3 ) ) ) )
229228an32s 781 . . . . . . . . 9  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )  /\  (
u  e.  RR  /\  u  <  ( vol * `  ( A  \  B
) ) ) )  ->  E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( B  C_  U. ran  ( (,)