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

Theorem ismblfin 26146
Description: Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky8] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) (Revised by Brendan Leahy, 28-Mar-2018.)
Assertion
Ref Expression
ismblfin  |-  ( ( 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 ismblfin
Dummy variables  a 
c  f  t  u  v  w  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mblfinlem3 26145 . 2  |-  ( ( ( 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 ,  <  ) )
2 elpwi 3767 . . . . 5  |-  ( w  e.  ~P RR  ->  w 
C_  RR )
3 elmapi 6997 . . . . . . . . . . . 12  |-  ( f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
4 inss1 3521 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  i^i  A )  C_  w
5 ovolsscl 19335 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  i^i  A
)  C_  w  /\  w  C_  RR  /\  ( vol * `  w )  e.  RR )  -> 
( vol * `  ( w  i^i  A ) )  e.  RR )
64, 5mp3an1 1266 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  -> 
( vol * `  ( w  i^i  A ) )  e.  RR )
7 difss 3434 . . . . . . . . . . . . . . . . . . . 20  |-  ( w 
\  A )  C_  w
8 ovolsscl 19335 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  \  A
)  C_  w  /\  w  C_  RR  /\  ( vol * `  w )  e.  RR )  -> 
( vol * `  ( w  \  A ) )  e.  RR )
97, 8mp3an1 1266 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  -> 
( vol * `  ( w  \  A ) )  e.  RR )
106, 9readdcld 9071 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  -> 
( ( vol * `  ( w  i^i  A
) )  +  ( vol * `  (
w  \  A )
) )  e.  RR )
1110rexrd 9090 . . . . . . . . . . . . . . . . 17  |-  ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  -> 
( ( vol * `  ( w  i^i  A
) )  +  ( vol * `  (
w  \  A )
) )  e.  RR* )
1211ad3antlr 712 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( w  C_  RR  /\  ( vol * `  w
)  e.  RR ) )  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  /\  w  C_  U. ran  ( (,)  o.  f ) )  ->  ( ( vol
* `  ( w  i^i  A ) )  +  ( vol * `  ( w  \  A ) ) )  e.  RR* )
13 rncoss 5095 . . . . . . . . . . . . . . . . . . 19  |-  ran  ( (,)  o.  f )  C_  ran  (,)
1413unissi 3998 . . . . . . . . . . . . . . . . . 18  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  (,)
15 unirnioo 10960 . . . . . . . . . . . . . . . . . 18  |-  RR  =  U. ran  (,)
1614, 15sseqtr4i 3341 . . . . . . . . . . . . . . . . 17  |-  U. ran  ( (,)  o.  f ) 
C_  RR
17 ovolcl 19327 . . . . . . . . . . . . . . . . 17  |-  ( U. ran  ( (,)  o.  f
)  C_  RR  ->  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR* )
1816, 17mp1i 12 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( w  C_  RR  /\  ( vol * `  w
)  e.  RR ) )  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  /\  w  C_  U. ran  ( (,)  o.  f ) )  ->  ( vol * `  U. ran  ( (,) 
o.  f ) )  e.  RR* )
19 eqid 2404 . . . . . . . . . . . . . . . . . . 19  |-  ( ( abs  o.  -  )  o.  f )  =  ( ( abs  o.  -  )  o.  f )
20 eqid 2404 . . . . . . . . . . . . . . . . . . 19  |-  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
2119, 20ovolsf 19322 . . . . . . . . . . . . . . . . . 18  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,)  +oo ) )
22 frn 5556 . . . . . . . . . . . . . . . . . . 19  |-  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,)  +oo )  ->  ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  ( 0 [,)  +oo ) )
23 icossxr 10951 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,)  +oo )  C_  RR*
2422, 23syl6ss 3320 . . . . . . . . . . . . . . . . . 18  |-  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,)  +oo )  ->  ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  RR* )
25 supxrcl 10849 . . . . . . . . . . . . . . . . . 18  |-  ( ran 
seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) )  C_  RR* 
->  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  e.  RR* )
2621, 24, 253syl 19 . . . . . . . . . . . . . . . . 17  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  sup ( ran  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  e. 
RR* )
2726ad2antlr 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( w  C_  RR  /\  ( vol * `  w
)  e.  RR ) )  /\  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )  /\  w  C_  U. ran  ( (,)  o.  f ) )  ->  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  e.  RR* )
28 pnfge 10683 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( vol * `  ( w  i^i  A ) )  +  ( vol
* `  ( w  \  A ) ) )  e.  RR*  ->  ( ( vol * `  (
w  i^i  A )
)  +  ( vol
* `  ( w  \  A ) ) )  <_  +oo )
2911, 28syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  -> 
( ( vol * `  ( w  i^i  A
) )  +  ( vol * `  (
w  \  A )
) )  <_  +oo )
3029ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  =  +oo )  -> 
( ( vol * `  ( w  i^i  A
) )  +  ( vol * `  (
w  \  A )
) )  <_  +oo )
31 simpr 448 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  =  +oo )  -> 
( vol * `  U. ran  ( (,)  o.  f ) )  = 
+oo )
3230, 31breqtrrd 4198 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  =  +oo )  -> 
( ( vol * `  ( w  i^i  A
) )  +  ( vol * `  (
w  \  A )
) )  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
3332adantlll 699 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( w  C_  RR  /\  ( vol * `  w
)  e.  RR ) )  /\  w  C_  U.
ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  =  +oo )  ->  ( ( vol
* `  ( w  i^i  A ) )  +  ( vol * `  ( w  \  A ) ) )  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
3416, 17ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR*
35 nltpnft 10710 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR*  ->  ( ( vol * `  U. ran  ( (,) 
o.  f ) )  =  +oo  <->  -.  ( vol * `  U. ran  ( (,)  o.  f ) )  <  +oo )
)
3634, 35ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  =  +oo  <->  -.  ( vol * `  U. ran  ( (,)  o.  f
) )  <  +oo )
3736necon2abii 2622 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  <  +oo  <->  ( vol * `  U. ran  ( (,)  o.  f ) )  =/=  +oo )
38 ovolge0 19330 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U. ran  ( (,)  o.  f
)  C_  RR  ->  0  <_  ( vol * `  U. ran  ( (,) 
o.  f ) ) )
3916, 38ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <_  ( vol * `  U. ran  ( (,)  o.  f ) )
40 0re 9047 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
41 xrre3 10715 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( vol * `  U. ran  ( (,) 
o.  f ) )  e.  RR*  /\  0  e.  RR )  /\  (
0  <_  ( vol * `
 U. ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,) 
o.  f ) )  <  +oo ) )  -> 
( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )
4234, 40, 41mpanl12 664 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  <_  ( vol * `
 U. ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,) 
o.  f ) )  <  +oo )  ->  ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )
4339, 42mpan 652 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  <  +oo  ->  ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )
4437, 43sylbir 205 . . . . . . . . . . . . . . . . . . 19  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  =/=  +oo  ->  ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )
4510ad3antlr 712 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( w  C_  RR  /\  ( vol * `  w
)  e.  RR ) )  /\  w  C_  U.
ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( ( vol
* `  ( w  i^i  A ) )  +  ( vol * `  ( w  \  A ) ) )  e.  RR )
46 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) )  ->  z  =  ( vol `  a ) )
47 eleq1 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  =  a  ->  (
b  e.  dom  vol  <->  a  e.  dom  vol ) )
48 uniretop 18749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  RR  =  U. ( topGen `  ran  (,) )
4948cldss 17048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
50 dfss4 3535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
5149, 50sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
52 rembl 19388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  RR  e.  dom  vol
5348cldopn 17050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
54 opnmbl 19447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( RR  \  b )  e.  ( topGen `  ran  (,) )  ->  ( RR  \  b )  e.  dom  vol )
5553, 54syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  dom  vol )
56 difmbl 19390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  b
)  e.  dom  vol )  ->  ( RR  \ 
( RR  \  b
) )  e.  dom  vol )
5752, 55, 56sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  e.  dom  vol )
5851, 57eqeltrrd 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
5947, 58vtoclga 2977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  a  e.  dom  vol )
60 mblvol 19379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  dom  vol  ->  ( vol `  a )  =  ( vol * `  a ) )
6159, 60syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  a )  =  ( vol * `  a
) )
6246, 61sylan9eqr 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) )  -> 
z  =  ( vol
* `  a )
)
6362adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) ) )  ->  z  =  ( vol * `  a
) )
64 inss1 3521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  C_ 
U. ran  ( (,)  o.  f )
65 sstr 3316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  ( U. ran  ( (,)  o.  f )  i^i 
A )  C_  U. ran  ( (,)  o.  f ) )  ->  a  C_  U.
ran  ( (,)  o.  f ) )
6664, 65mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  -> 
a  C_  U. ran  ( (,)  o.  f ) )
6766ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) )  -> 
a  C_  U. ran  ( (,)  o.  f ) )
68 ovolsscl 19335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( a  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )  ->  ( vol * `  a )  e.  RR )
6916, 68mp3an2 1267 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol * `  a )  e.  RR )
7069ancoms 440 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  a  C_  U.
ran  ( (,)  o.  f ) )  -> 
( vol * `  a )  e.  RR )
7167, 70sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) ) )  ->  ( vol * `  a )  e.  RR )
7263, 71eqeltrd 2478 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) ) )  ->  z  e.  RR )
7372rexlimdvaa 2791 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) )  ->  z  e.  RR ) )
7473abssdv 3377 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) }  C_  RR )
75 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
z  =  ( vol `  a )  <->  y  =  ( vol `  a ) ) )
7675anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  y  ->  (
( a  C_  ( U. ran  ( (,)  o.  f )  i^i  A
)  /\  z  =  ( vol `  a ) )  <->  ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  y  =  ( vol `  a
) ) ) )
7776rexbidv 2687 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  y  ->  ( E. a  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  /\  z  =  ( vol `  a ) )  <->  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  y  =  ( vol `  a
) ) ) )
7877ralab 3055 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. y  e.  { z  |  E. a  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) ) } y  <_  ( vol * `  U. ran  ( (,)  o.  f ) )  <->  A. y ( E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  y  =  ( vol `  a
) )  ->  y  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) ) )
79 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  y  =  ( vol `  a ) )  ->  y  =  ( vol `  a ) )
8079, 61sylan9eqr 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  y  =  ( vol `  a
) ) )  -> 
y  =  ( vol
* `  a )
)
81 ovolss 19334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( a  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR )  ->  ( vol * `  a )  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
8266, 16, 81sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  -> 
( vol * `  a )  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
8382ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  y  =  ( vol `  a
) ) )  -> 
( vol * `  a )  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
8480, 83eqbrtrd 4192 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( a  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  y  =  ( vol `  a
) ) )  -> 
y  <_  ( vol * `
 U. ran  ( (,)  o.  f ) ) )
8584rexlimiva 2785 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  y  =  ( vol `  a
) )  ->  y  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
8678, 85mpgbir 1556 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  A. y  e.  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } y  <_  ( vol * `  U. ran  ( (,) 
o.  f ) )
87 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( vol * `  U. ran  ( (,) 
o.  f ) )  ->  ( y  <_  x 
<->  y  <_  ( vol * `
 U. ran  ( (,)  o.  f ) ) ) )
8887ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( vol * `  U. ran  ( (,) 
o.  f ) )  ->  ( A. y  e.  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } y  <_  x  <->  A. y  e.  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } y  <_  ( vol * `  U. ran  ( (,) 
o.  f ) ) ) )
8988rspcev 3012 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  A. y  e.  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } y  <_  ( vol * `  U. ran  ( (,) 
o.  f ) ) )  ->  E. x  e.  RR  A. y  e. 
{ z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } y  <_  x )
9086, 89mpan2 653 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  E. x  e.  RR  A. y  e.  { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } y  <_  x )
91 retop 18748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( topGen ` 
ran  (,) )  e.  Top
92 0cld 17057 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
9391, 92ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )
94 0ss 3616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  (/)  C_  ( U. ran  ( (,)  o.  f )  i^i  A
)
95 0mbl 19387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (/)  e.  dom  vol
96 mblvol 19379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol * `  (/) ) )
9795, 96ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( vol `  (/) )  =  ( vol * `  (/) )
98 ovol0 19342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( vol
* `  (/) )  =  0
9997, 98eqtr2i 2425 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  =  ( vol `  (/) )
10094, 99pm3.2i 442 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (/)  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  0  =  ( vol `  (/) ) )
101 sseq1 3329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  =  (/)  ->  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  <->  (/)  C_  ( U. ran  ( (,)  o.  f )  i^i  A
) ) )
102 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  =  (/)  ->  ( vol `  a )  =  ( vol `  (/) ) )
103102eqeq2d 2415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  =  (/)  ->  ( 0  =  ( vol `  a
)  <->  0  =  ( vol `  (/) ) ) )
104101, 103anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  (/)  ->  ( ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  0  =  ( vol `  a ) )  <-> 
( (/)  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  0  =  ( vol `  (/) ) ) ) )
105104rspcev 3012 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
(/)  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( (/)  C_  ( U. ran  ( (,)  o.  f )  i^i  A
)  /\  0  =  ( vol `  (/) ) ) )  ->  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  0  =  ( vol `  a
) ) )
10693, 100, 105mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  0  =  ( vol `  a
) )
107 c0ex 9041 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  _V
108 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  0  ->  (
z  =  ( vol `  a )  <->  0  =  ( vol `  a ) ) )
109108anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  0  ->  (
( a  C_  ( U. ran  ( (,)  o.  f )  i^i  A
)  /\  z  =  ( vol `  a ) )  <->  ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  0  =  ( vol `  a
) ) ) )
110109rexbidv 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  0  ->  ( E. a  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  /\  z  =  ( vol `  a ) )  <->  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  0  =  ( vol `  a
) ) ) )
111107, 110elab 3042 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0  e.  { z  |  E. a  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) ) }  <->  E. a  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  0  =  ( vol `  a ) ) )
112106, 111mpbir 201 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  e.  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) }
113 ne0i 3594 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  e.  { z  |  E. a  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) ) }  ->  { z  |  E. a  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) ) }  =/=  (/) )
114112, 113ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) }  =/=  (/)
115 suprcl 9924 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) }  C_  RR  /\  { z  |  E. a  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) ) }  =/=  (/)  /\  E. x  e.  RR  A. y  e.  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } y  <_  x )  ->  sup ( { z  |  E. a  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) ) } ,  RR ,  <  )  e.  RR )
116114, 115mp3an2 1267 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) }  C_  RR  /\  E. x  e.  RR  A. y  e. 
{ z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } y  <_  x )  ->  sup ( { z  |  E. a  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) ) } ,  RR ,  <  )  e.  RR )
11774, 90, 116syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  sup ( { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } ,  RR ,  <  )  e.  RR )
118 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) )  ->  z  =  ( vol `  c ) )
119 eleq1 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  =  c  ->  (
b  e.  dom  vol  <->  c  e.  dom  vol ) )
120119, 58vtoclga 2977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  c  e.  dom  vol )
121 mblvol 19379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  dom  vol  ->  ( vol `  c )  =  ( vol * `  c ) )
122120, 121syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  c )  =  ( vol * `  c
) )
123118, 122sylan9eqr 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) )  -> 
z  =  ( vol
* `  c )
)
124123adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) ) )  ->  z  =  ( vol * `  c
) )
125 difss2 3436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  -> 
c  C_  U. ran  ( (,)  o.  f ) )
126125ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) )  -> 
c  C_  U. ran  ( (,)  o.  f ) )
127 ovolsscl 19335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )  ->  ( vol * `  c )  e.  RR )
12816, 127mp3an2 1267 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol * `  c )  e.  RR )
129128ancoms 440 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  c  C_  U.
ran  ( (,)  o.  f ) )  -> 
( vol * `  c )  e.  RR )
130126, 129sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) ) )  ->  ( vol * `  c )  e.  RR )
131124, 130eqeltrd 2478 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) ) )  ->  z  e.  RR )
132131rexlimdvaa 2791 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) )  ->  z  e.  RR ) )
133132abssdv 3377 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }  C_  RR )
134 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
z  =  ( vol `  c )  <->  y  =  ( vol `  c ) ) )
135134anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  y  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  y  =  ( vol `  c
) ) ) )
136135rexbidv 2687 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  y  ->  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  /\  z  =  ( vol `  c ) )  <->  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  y  =  ( vol `  c
) ) ) )
137136ralab 3055 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. y  e.  { z  |  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) ) } y  <_  ( vol * `  U. ran  ( (,)  o.  f ) )  <->  A. y ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  y  =  ( vol `  c
) )  ->  y  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) ) )
138 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  y  =  ( vol `  c ) )  ->  y  =  ( vol `  c ) )
139138, 122sylan9eqr 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  y  =  ( vol `  c
) ) )  -> 
y  =  ( vol
* `  c )
)
140 ovolss 19334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR )  ->  ( vol * `  c )  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
141125, 16, 140sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  -> 
( vol * `  c )  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
142141ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  y  =  ( vol `  c
) ) )  -> 
( vol * `  c )  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
143139, 142eqbrtrd 4192 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  y  =  ( vol `  c
) ) )  -> 
y  <_  ( vol * `
 U. ran  ( (,)  o.  f ) ) )
144143rexlimiva 2785 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  y  =  ( vol `  c
) )  ->  y  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
145137, 144mpgbir 1556 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  A. y  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } y  <_  ( vol * `  U. ran  ( (,) 
o.  f ) )
14687ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( vol * `  U. ran  ( (,) 
o.  f ) )  ->  ( A. y  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } y  <_  x  <->  A. y  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } y  <_  ( vol * `  U. ran  ( (,) 
o.  f ) ) ) )
147146rspcev 3012 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  A. y  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } y  <_  ( vol * `  U. ran  ( (,) 
o.  f ) ) )  ->  E. x  e.  RR  A. y  e. 
{ z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } y  <_  x )
148145, 147mpan2 653 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  E. x  e.  RR  A. y  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } y  <_  x )
149 0ss 3616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  (/)  C_  ( U. ran  ( (,)  o.  f )  \  A
)
150149, 99pm3.2i 442 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (/)  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  0  =  ( vol `  (/) ) )
151 sseq1 3329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  (/)  ->  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  <->  (/)  C_  ( U. ran  ( (,)  o.  f )  \  A
) ) )
152 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  (/)  ->  ( vol `  c )  =  ( vol `  (/) ) )
153152eqeq2d 2415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  (/)  ->  ( 0  =  ( vol `  c
)  <->  0  =  ( vol `  (/) ) ) )
154151, 153anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  (/)  ->  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  0  =  ( vol `  c ) )  <-> 
( (/)  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  0  =  ( vol `  (/) ) ) ) )
155154rspcev 3012 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
(/)  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( (/)  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  0  =  ( vol `  (/) ) ) )  ->  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  0  =  ( vol `  c
) ) )
15693, 150, 155mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  0  =  ( vol `  c
) )
157 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  0  ->  (
z  =  ( vol `  c )  <->  0  =  ( vol `  c ) ) )
158157anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  0  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  0  =  ( vol `  c
) ) ) )
159158rexbidv 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  0  ->  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  /\  z  =  ( vol `  c ) )  <->  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  0  =  ( vol `  c
) ) ) )
160107, 159elab 3042 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0  e.  { z  |  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) ) }  <->  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  0  =  ( vol `  c ) ) )
161156, 160mpbir 201 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }
162 ne0i 3594 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  e.  { z  |  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) ) }  ->  { z  |  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) ) }  =/=  (/) )
163161, 162ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }  =/=  (/)
164 suprcl 9924 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }  C_  RR  /\  { z  |  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) ) }  =/=  (/)  /\  E. x  e.  RR  A. y  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } y  <_  x )  ->  sup ( { z  |  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) ) } ,  RR ,  <  )  e.  RR )
165163, 164mp3an2 1267 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }  C_  RR  /\  E. x  e.  RR  A. y  e. 
{ z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } y  <_  x )  ->  sup ( { z  |  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) ) } ,  RR ,  <  )  e.  RR )
166133, 148, 165syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } ,  RR ,  <  )  e.  RR )
167117, 166readdcld 9071 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( sup ( { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } ,  RR ,  <  )  +  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } ,  RR ,  <  ) )  e.  RR )
168167adantl 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( w  C_  RR  /\  ( vol * `  w
)  e.  RR ) )  /\  w  C_  U.
ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( sup ( { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } ,  RR ,  <  )  +  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } ,  RR ,  <  ) )  e.  RR )
169 simpr 448 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( w  C_  RR  /\  ( vol * `  w
)  e.  RR ) )  /\  w  C_  U.
ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol * `  U. ran  ( (,) 
o.  f ) )  e.  RR )
1706ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR )  -> 
( vol * `  ( w  i^i  A ) )  e.  RR )
1719ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR )  -> 
( vol * `  ( w  \  A ) )  e.  RR )
172 ovolsscl 19335 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( U. ran  ( (,)  o.  f )  i^i 
A )  C_  U. ran  ( (,)  o.  f )  /\  U. ran  ( (,)  o.  f )  C_  RR  /\  ( vol * `  U. ran  ( (,) 
o.  f ) )  e.  RR )  -> 
( vol * `  ( U. ran  ( (,) 
o.  f )  i^i 
A ) )  e.  RR )
17364, 16, 172mp3an12 1269 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol * `  ( U. ran  ( (,) 
o.  f )  i^i 
A ) )  e.  RR )
174173adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR )  -> 
( vol * `  ( U. ran  ( (,) 
o.  f )  i^i 
A ) )  e.  RR )
175 difss 3434 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  f )
176 ovolsscl 19335 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( U. ran  ( (,)  o.  f )  \  A )  C_  U. ran  ( (,)  o.  f )  /\  U. ran  ( (,)  o.  f )  C_  RR  /\  ( vol * `  U. ran  ( (,) 
o.  f ) )  e.  RR )  -> 
( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
177175, 16, 176mp3an12 1269 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
178177adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR )  -> 
( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
179 ssrin 3526 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( w  i^i  A
)  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )
)
18064, 16sstri 3317 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  C_  RR
181 ovolss 19334 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( w  i^i  A
)  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  ( U. ran  ( (,)  o.  f )  i^i 
A )  C_  RR )  ->  ( vol * `  ( w  i^i  A
) )  <_  ( vol * `  ( U. ran  ( (,)  o.  f
)  i^i  A )
) )
182179, 180, 181sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol * `  ( w  i^i  A ) )  <_  ( vol * `
 ( U. ran  ( (,)  o.  f )  i^i  A ) ) )
183182ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR )  -> 
( vol * `  ( w  i^i  A ) )  <_  ( vol * `
 ( U. ran  ( (,)  o.  f )  i^i  A ) ) )
184 ssdif 3442 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( w  \  A
)  C_  ( U. ran  ( (,)  o.  f
)  \  A )
)
185175, 16sstri 3317 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_  RR
186 ovolss 19334 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( w  \  A
)  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  ( U. ran  ( (,)  o.  f )  \  A )  C_  RR )  ->  ( vol * `  ( w  \  A
) )  <_  ( vol * `  ( U. ran  ( (,)  o.  f
)  \  A )
) )
187184, 185, 186sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol * `  ( w  \  A ) )  <_  ( vol * `
 ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
188187ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR )  -> 
( vol * `  ( w  \  A ) )  <_  ( vol * `
 ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
189170, 171, 174, 178, 183, 188le2addd 9600 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR )  -> 
( ( vol * `  ( w  i^i  A
) )  +  ( vol * `  (
w  \  A )
) )  <_  (
( vol * `  ( U. ran  ( (,) 
o.  f )  i^i 
A ) )  +  ( vol * `  ( U. ran  ( (,) 
o.  f )  \  A ) ) ) )
190 dfin4 3541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  =  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) )
191190fveq2i 5690 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( vol
* `  ( U. ran  ( (,)  o.  f
)  i^i  A )
)  =  ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  ( U. ran  ( (,)  o.  f
)  \  A )
) )
192191oveq1i 6050 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( vol * `  ( U. ran  ( (,)  o.  f )  i^i  A
) )  +  ( vol * `  ( U. ran  ( (,)  o.  f )  \  A
) ) )  =  ( ( vol * `  ( U. ran  ( (,)  o.  f )  \ 
( U. ran  ( (,)  o.  f )  \  A ) ) )  +  ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) ) )
193189, 192syl6breq 4211 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( w  C_  RR  /\  ( vol * `  w )  e.  RR )  /\  w  C_  U. ran  ( (,)  o.  f ) )  /\  ( vol
* `  U. ran  ( (,)  o.  f ) )  e.  RR )  -> 
( ( vol * `  ( w  i^i  A
) )  +  ( vol * `  (
w  \  A )
) )  <_  (
( vol * `  ( U. ran  ( (,) 
o.  f )  \ 
( U. ran  ( (,)  o.  f )  \  A ) ) )  +  ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) ) ) )
194193adantlll 699 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( w  C_  RR  /\  ( vol * `  w
)  e.  RR ) )  /\  w  C_  U.
ran  ( (,)  o.  f ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( ( vol
* `  ( w  i^i  A ) )  +  ( vol * `  ( w  \  A ) ) )  <_  (
( vol * `  ( U. ran  ( (,) 
o.  f )  \ 
( U. ran  ( (,)  o.  f )  \  A ) ) )  +  ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) ) ) )
195 simpll 731 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( A 
C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( w  C_  RR  /\  ( vol * `  w
)  e.  RR ) )  /\  w  C_  U.
ran  ( (,)  o.  f ) )  -> 
( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) ) )
196190sseq2i 3333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  <->  a  C_  ( U. ran  ( (,) 
o.  f )  \ 
( U. ran  ( (,)  o.  f )  \  A ) ) )
197196anbi1i 677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) )  <-> 
( a  C_  ( U. ran  ( (,)  o.  f )  \  ( U. ran  ( (,)  o.  f )  \  A
) )  /\  z  =  ( vol `  a
) ) )
198197rexbii 2691 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) )  <->  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  \ 
( U. ran  ( (,)  o.  f )  \  A ) )  /\  z  =  ( vol `  a ) ) )
199198abbii 2516 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) }  =  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  \ 
( U. ran  ( (,)  o.  f )  \  A ) )  /\  z  =  ( vol `  a ) ) }
200199supeq1i 7410 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  sup ( { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) } ,  RR ,  <  )  =  sup ( { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  \ 
( U. ran  ( (,)  o.  f )  \  A ) )  /\  z  =  ( vol `  a ) ) } ,  RR ,  <  )
20116jctl 526 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( U. ran  ( (,)  o.  f )  C_  RR  /\  ( vol * `  U. ran  ( (,) 
o.  f ) )  e.  RR ) )
202201adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( U. ran  ( (,)  o.  f ) 
C_  RR  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR ) )
203177, 185jctil 524 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  RR  /\  ( vol * `  ( U. ran  ( (,)  o.  f )  \  A ) )  e.  RR ) )
204203adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( ( U. ran  ( (,)  o.  f
)  \  A )  C_  RR  /\  ( vol
* `  ( U. ran  ( (,)  o.  f
)  \  A )
)  e.  RR ) )
205 ltso 9112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  <  Or  RR
206205a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  <  Or  RR )
207 id 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR )
208 vex 2919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  x  e. 
_V
209 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  x  ->  (
z  =  ( vol `  c )  <->  x  =  ( vol `  c ) ) )
210209anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  x  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) ) )
211210rexbidv 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  x  ->  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( c 
C_  U. ran  ( (,) 
o.  f )  /\  z  =  ( vol `  c ) )  <->  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) ) )
212208, 211elab 3042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  { z  |  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) ) }  <->  E. c  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( c 
C_  U. ran  ( (,) 
o.  f )  /\  x  =  ( vol `  c ) ) )
21316, 140mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol * `  c )  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
214213ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_ 
U. ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) )  -> 
( vol * `  c )  <_  ( vol * `  U. ran  ( (,)  o.  f ) ) )
21548cldss 17048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  c  C_  RR )
216 ovolcl 19327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c 
C_  RR  ->  ( vol
* `  c )  e.  RR* )
217215, 216syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol * `
 c )  e. 
RR* )
218 xrlenlt 9099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( vol * `  c )  e.  RR*  /\  ( vol * `  U. ran  ( (,)  o.  f ) )  e. 
RR* )  ->  (
( vol * `  c )  <_  ( vol * `  U. ran  ( (,)  o.  f ) )  <->  -.  ( vol * `
 U. ran  ( (,)  o.  f ) )  <  ( vol * `  c ) ) )
219217, 34, 218sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( ( vol * `  c )  <_  ( vol * `  U. ran  ( (,) 
o.  f ) )  <->  -.  ( vol * `  U. ran  ( (,)  o.  f ) )  < 
( vol * `  c ) ) )
220219adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_ 
U. ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) )  -> 
( ( vol * `  c )  <_  ( vol * `  U. ran  ( (,)  o.  f ) )  <->  -.  ( vol * `
 U. ran  ( (,)  o.  f ) )  <  ( vol * `  c ) ) )
221 id 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( vol `  c
)  ->  x  =  ( vol `  c ) )
222221, 122sylan9eqr 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  x  =  ( vol `  c ) )  ->  x  =  ( vol * `  c
) )
223 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( vol * `  c )  ->  (
( vol * `  U. ran  ( (,)  o.  f ) )  < 
x  <->  ( vol * `  U. ran  ( (,) 
o.  f ) )  <  ( vol * `  c ) ) )
224223notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  =  ( vol * `  c )  ->  ( -.  ( vol * `  U. ran  ( (,)  o.  f ) )  < 
x  <->  -.  ( vol * `
 U. ran  ( (,)  o.  f ) )  <  ( vol * `  c ) ) )
225222, 224syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  x  =  ( vol `  c ) )  ->  ( -.  ( vol * `  U. ran  ( (,)  o.  f
) )  <  x  <->  -.  ( vol * `  U. ran  ( (,)  o.  f ) )  < 
( vol * `  c ) ) )
226225adantrl 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_ 
U. ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) )  -> 
( -.  ( vol
* `  U. ran  ( (,)  o.  f ) )  <  x  <->  -.  ( vol * `  U. ran  ( (,)  o.  f ) )  <  ( vol
* `  c )
) )
227220, 226bitr4d 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_ 
U. ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) )  -> 
( ( vol * `  c )  <_  ( vol * `  U. ran  ( (,)  o.  f ) )  <->  -.  ( vol * `
 U. ran  ( (,)  o.  f ) )  <  x ) )
228214, 227mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_ 
U. ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) )  ->  -.  ( vol * `  U. ran  ( (,)  o.  f ) )  < 
x )
229228rexlimiva 2785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) )  ->  -.  ( vol * `  U. ran  ( (,)  o.  f
) )  <  x
)
230212, 229sylbi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  { z  |  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) ) }  ->  -.  ( vol * `
 U. ran  ( (,)  o.  f ) )  <  x )
231230adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  x  e. 
{ z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) ) } )  ->  -.  ( vol * `
 U. ran  ( (,)  o.  f ) )  <  x )
232 retopbas 18747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ran  (,)  e. 
TopBases
233 bastg 16986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ran 
(,)  e.  TopBases  ->  ran  (,)  C_  ( topGen `  ran  (,) )
)
234232, 233ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ran  (,)  C_  ( topGen `  ran  (,) )
23513, 234sstri 3317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
236 uniopn 16925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
)
23791, 235, 236mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
238 mblfinlem 26143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( U. ran  ( (,) 
o.  f )  e.  ( topGen `  ran  (,) )  /\  x  e.  RR  /\  x  <  ( vol
* `  U. ran  ( (,)  o.  f ) ) )  ->  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  <  ( vol * `  c ) ) )
239237, 238mp3an1 1266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( x  e.  RR  /\  x  <  ( vol * `  U. ran  ( (,) 
o.  f ) ) )  ->  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  <  ( vol * `  c ) ) )
240122eqcomd 2409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol * `
 c )  =  ( vol `  c
) )
241240anim1i 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  x  <  ( vol * `  c
) )  ->  (
( vol * `  c )  =  ( vol `  c )  /\  x  <  ( vol * `  c ) ) )
242241ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( x  <  ( vol * `  c )  ->  (
( vol * `  c )  =  ( vol `  c )  /\  x  <  ( vol * `  c ) ) ) )
243242anim2d 549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( (
c  C_  U. ran  ( (,)  o.  f )  /\  x  <  ( vol * `  c ) )  -> 
( c  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol
* `  c )  =  ( vol `  c
)  /\  x  <  ( vol * `  c
) ) ) ) )
244 fvex 5701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( vol
* `  c )  e.  _V
245 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  ( vol * `  c )  ->  (
y  =  ( vol `  c )  <->  ( vol * `
 c )  =  ( vol `  c
) ) )
246245anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  ( vol * `  c )  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  y  =  ( vol `  c ) )  <->  ( c  C_  U.
ran  ( (,)  o.  f )  /\  ( vol * `  c )  =  ( vol `  c
) ) ) )
247 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  ( vol * `  c )  ->  (
x  <  y  <->  x  <  ( vol * `  c
) ) )
248246, 247anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  ( vol * `  c )  ->  (
( ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) )  /\  x  <  y )  <->  ( (
c  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  c
)  =  ( vol `  c ) )  /\  x  <  ( vol * `  c ) ) ) )
249244, 248spcev 3003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( c  C_  U. ran  ( (,)  o.  f )  /\  ( vol * `  c )  =  ( vol `  c ) )  /\  x  < 
( vol * `  c ) )  ->  E. y ( ( c 
C_  U. ran  ( (,) 
o.  f )  /\  y  =  ( vol `  c ) )  /\  x  <  y ) )
250249anasss 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  ( ( vol * `  c )  =  ( vol `  c )  /\  x  <  ( vol * `  c ) ) )  ->  E. y
( ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) )  /\  x  <  y ) )
251243, 250syl6 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( (
c  C_  U. ran  ( (,)  o.  f )  /\  x  <  ( vol * `  c ) )  ->  E. y ( ( c 
C_  U. ran  ( (,) 
o.  f )  /\  y  =  ( vol `  c ) )  /\  x  <  y ) ) )
252251reximia 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  <  ( vol * `  c ) )  ->  E. c  e.  ( Clsd `  ( topGen `  ran  (,) ) ) E. y
( ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) )  /\  x  <  y ) )
253239, 252syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( x  e.  RR  /\  x  <  ( vol * `  U. ran  ( (,) 
o.  f ) ) )  ->  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) E. y ( ( c  C_  U. ran  ( (,)  o.  f )  /\  y  =  ( vol `  c ) )  /\  x  < 
y ) )
254 r19.41v 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( ( c 
C_  U. ran  ( (,) 
o.  f )  /\  y  =  ( vol `  c ) )  /\  x  <  y )  <->  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) )  /\  x  <  y ) )
255254exbii 1589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. y E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( ( c 
C_  U. ran  ( (,) 
o.  f )  /\  y  =  ( vol `  c ) )  /\  x  <  y )  <->  E. y
( E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) )  /\  x  <  y ) )
256 rexcom4 2935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) E. y ( ( c  C_  U. ran  ( (,)  o.  f )  /\  y  =  ( vol `  c ) )  /\  x  < 
y )  <->  E. y E. c  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( ( c  C_  U. ran  ( (,)  o.  f )  /\  y  =  ( vol `  c ) )  /\  x  <  y ) )
257134anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  y  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) ) ) )
258257rexbidv 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  y  ->  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( c 
C_  U. ran  ( (,) 
o.  f )  /\  z  =  ( vol `  c ) )  <->  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) ) ) )
259258rexab 3057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( E. y  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) ) } x  <  y  <->  E. y ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) )  /\  x  <  y ) )
260255, 256, 2593bitr4i 269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) E. y ( ( c  C_  U. ran  ( (,)  o.  f )  /\  y  =  ( vol `  c ) )  /\  x  < 
y )  <->  E. y  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) ) } x  <  y )
261253, 260sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  RR  /\  x  <  ( vol * `  U. ran  ( (,) 
o.  f ) ) )  ->  E. y  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) ) } x  <  y )
262261adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( vol * `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  ( x  e.  RR  /\  x  <  ( vol * `  U. ran  ( (,)  o.  f ) ) ) )  ->  E. y  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) ) } x  <  y )
263206, 207, 231, 262eqsupd 7418 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) ) } ,  RR ,  <  )  =  ( vol * `  U. ran  ( (,)  o.  f ) ) )
264263eqcomd 2409 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol * `  U. ran  ( (,)  o.  f ) )  =  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) ) } ,  RR ,  <  ) )
265264adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol * `  U. ran  ( (,) 
o.  f ) )  =  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) ) } ,  RR ,  <  ) )
266 sseq1 3329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
c  C_  U. ran  ( (,)  o.  f )  <->  a  C_  U.
ran  ( (,)  o.  f ) ) )
267 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  ( vol `  c )  =  ( vol `  a
) )
268267eqeq2d 2415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
z  =  ( vol `  c )  <->  z  =  ( vol `  a ) ) )
269266, 268anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  a  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( a  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  a
) ) ) )
270269cbvrexv 2893 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) )  <->  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  a
) ) )
271270abbii 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) ) }  =  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  a
) ) }
272271supeq1i 7410 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  c
) ) } ,  RR ,  <  )  =  sup ( { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  a
) ) } ,  RR ,  <  )
273265, 272syl6eq 2452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol * `  U. ran  ( (,) 
o.  f ) )  =  sup ( { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  a
) ) } ,  RR ,  <  ) )
274 sseq1 3329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  <->  a 
C_  ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
275274, 268anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  a  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( a  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  a
) ) ) )
276275cbvrexv 2893 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) )  <->  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  a
) ) )
277276abbii 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }  =  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  a
) ) }
278277supeq1i 7410 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } ,  RR ,  <  )  =  sup ( { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  a
) ) } ,  RR ,  <  )
279 simpll 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( A  C_  RR  /\  ( vol * `  A )  e.  RR ) )
280 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  z  ->  (
y  =  ( vol `  b )  <->  z  =  ( vol `  b ) ) )
281280anbi2d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  z  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  z  =  ( vol `  b ) ) ) )
282281rexbidv 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  z  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  y  =  ( vol `  b
) )  <->  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  z  =  ( vol `  b ) ) ) )
283 sseq1 3329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( b  =  c  ->  (
b  C_  A  <->  c  C_  A ) )
284 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( b  =  c  ->  ( vol `  b )  =  ( vol `  c
) )
285284eqeq2d 2415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( b  =  c  ->  (
z  =  ( vol `  b )  <->  z  =  ( vol `  c ) ) )
286283, 285anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( b  =  c  ->  (
( b  C_  A  /\  z  =  ( vol `  b ) )  <-> 
( c  C_  A  /\  z  =  ( vol `  c ) ) ) )
287286cbvrexv 2893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  z  =  ( vol `  b ) )  <->  E. c  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) ( c  C_  A  /\  z  =  ( vol `  c ) ) )
288282, 287syl6bb 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  z  ->  ( E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
C_  A  /\  y  =  ( vol `  b
) )  <->  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  A  /\  z  =  ( vol `  c ) ) ) )
289288cbvabv 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  { y  |  E. b  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) }  =  {
z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  A  /\  z  =  ( vol `  c ) ) }
290289supeq1i 7410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  =  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  A  /\  z  =  ( vol `  c ) ) } ,  RR ,  <  )
291290eqeq2i 2414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  <->  ( vol * `
 A )  =  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  A  /\  z  =  ( vol `  c ) ) } ,  RR ,  <  ) )
292291biimpi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( vol * `  A
)  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  )  ->  ( vol * `  A )  =  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  A  /\  z  =  ( vol `  c ) ) } ,  RR ,  <  ) )
293292ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( vol * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( b  C_  A  /\  y  =  ( vol `  b ) ) } ,  RR ,  <  ) )  /\  ( vol * `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol * `  A )  =  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  A  /\  z  =  ( vol `  c ) ) } ,  RR ,  <  ) )
294 mblfinlem2 26144 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( U. ran  ( (,)  o.  f )  C_  RR  /\  ( vol * `  U. ran  ( (,) 
o.  f ) )  e.  RR )  /\  ( A  C_  RR  /\  ( vol * `  A
)  e.  RR )  /\  ( ( vol
* `  U. ran  ( (,)  o.  f ) )  =  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `