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

Theorem ismblfin 30030
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 mblfinlem4 30029 . 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 4006 . . . . 5  |-  ( w  e.  ~P RR  ->  w 
C_  RR )
3 elmapi 7442 . . . . . . . . . . . 12  |-  ( f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
4 inss1 3703 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  i^i  A )  C_  w
5 ovolsscl 21770 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  i^i  A
)  C_  w  /\  w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  i^i  A ) )  e.  RR )
64, 5mp3an1 1312 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  i^i  A ) )  e.  RR )
7 difss 3616 . . . . . . . . . . . . . . . . . . . 20  |-  ( w 
\  A )  C_  w
8 ovolsscl 21770 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  \  A
)  C_  w  /\  w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  \  A ) )  e.  RR )
97, 8mp3an1 1312 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  \  A ) )  e.  RR )
106, 9readdcld 9626 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( ( vol* `  ( w  i^i  A
) )  +  ( vol* `  (
w  \  A )
) )  e.  RR )
1110rexrd 9646 . . . . . . . . . . . . . . . . 17  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( ( vol* `  ( w  i^i  A
) )  +  ( vol* `  (
w  \  A )
) )  e.  RR* )
1211ad3antlr 730 . . . . . . . . . . . . . . . 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 5253 . . . . . . . . . . . . . . . . . . 19  |-  ran  ( (,)  o.  f )  C_  ran  (,)
1413unissi 4257 . . . . . . . . . . . . . . . . . 18  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  (,)
15 unirnioo 11633 . . . . . . . . . . . . . . . . . 18  |-  RR  =  U. ran  (,)
1614, 15sseqtr4i 3522 . . . . . . . . . . . . . . . . 17  |-  U. ran  ( (,)  o.  f ) 
C_  RR
17 ovolcl 21762 . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . . . . 19  |-  ( ( abs  o.  -  )  o.  f )  =  ( ( abs  o.  -  )  o.  f )
20 eqid 2443 . . . . . . . . . . . . . . . . . . 19  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
2119, 20ovolsf 21757 . . . . . . . . . . . . . . . . . 18  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo ) )
22 frn 5727 . . . . . . . . . . . . . . . . . . 19  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  ( 0 [,) +oo ) )
23 icossxr 11618 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,) +oo )  C_  RR*
2422, 23syl6ss 3501 . . . . . . . . . . . . . . . . . 18  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  RR* )
25 supxrcl 11515 . . . . . . . . . . . . . . . . . 18  |-  ( ran 
seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) )  C_  RR* 
->  sup ( ran  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  )  e.  RR* )
2621, 24, 253syl 20 . . . . . . . . . . . . . . . . 17  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  sup ( ran  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  f ) ) , 
RR* ,  <  )  e. 
RR* )
2726ad2antlr 726 . . . . . . . . . . . . . . . 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 11348 . . . . . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . 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 4463 . . . . . . . . . . . . . . . . . . 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 717 . . . . . . . . . . . . . . . . . 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 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR*
35 nltpnft 11376 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR*  ->  ( ( vol* `  U. ran  ( (,) 
o.  f ) )  = +oo  <->  -.  ( vol* `  U. ran  ( (,)  o.  f ) )  < +oo )
)
3634, 35ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  = +oo  <->  -.  ( vol* `  U. ran  ( (,)  o.  f
) )  < +oo )
3736necon2abii 2709 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  < +oo  <->  ( vol* `  U. ran  ( (,)  o.  f ) )  =/= +oo )
38 ovolge0 21765 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U. ran  ( (,)  o.  f
)  C_  RR  ->  0  <_  ( vol* `  U. ran  ( (,) 
o.  f ) ) )
3916, 38ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <_  ( vol* `  U. ran  ( (,)  o.  f ) )
40 0re 9599 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
41 xrre3 11381 . . . . . . . . . . . . . . . . . . . . . 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 682 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  <_  ( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  < +oo )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
4339, 42mpan 670 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  < +oo  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
4437, 43sylbir 213 . . . . . . . . . . . . . . . . . . 19  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  =/= +oo  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
4510ad3antlr 730 . . . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) )  ->  z  =  ( vol `  a ) )
47 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  =  a  ->  (
b  e.  dom  vol  <->  a  e.  dom  vol ) )
48 uniretop 21142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  RR  =  U. ( topGen `  ran  (,) )
4948cldss 19403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
50 dfss4 3717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
5149, 50sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
52 rembl 21824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  RR  e.  dom  vol
5348cldopn 19405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
54 opnmbl 21884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 21826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  b
)  e.  dom  vol )  ->  ( RR  \ 
( RR  \  b
) )  e.  dom  vol )
5752, 55, 56sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  e.  dom  vol )
5851, 57eqeltrrd 2532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
5947, 58vtoclga 3159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  a  e.  dom  vol )
60 mblvol 21814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  dom  vol  ->  ( vol `  a )  =  ( vol* `  a ) )
6159, 60syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  a )  =  ( vol* `  a
) )
6246, 61sylan9eqr 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) )  -> 
z  =  ( vol* `  a )
)
6362adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  C_ 
U. ran  ( (,)  o.  f )
65 sstr 3497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 671 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  -> 
a  C_  U. ran  ( (,)  o.  f ) )
6766ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 21770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol* `  a )  e.  RR )
7069ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  a  C_  U.
ran  ( (,)  o.  f ) )  -> 
( vol* `  a )  e.  RR )
7167, 70sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2531 . . . . . . . . . . . . . . . . . . . . . . . . 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 2936 . . . . . . . . . . . . . . . . . . . . . . . 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 3559 . . . . . . . . . . . . . . . . . . . . . . 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 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
z  =  ( vol `  a )  <->  y  =  ( vol `  a ) ) )
7675anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2954 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3246 . . . . . . . . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  y  =  ( vol `  a ) )  ->  y  =  ( vol `  a ) )
8079, 61sylan9eqr 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  y  =  ( vol `  a
) ) )  -> 
y  =  ( vol* `  a )
)
81 ovolss 21769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( a  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR )  ->  ( vol* `  a )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
8266, 16, 81sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  -> 
( vol* `  a )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
8382ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4457 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2931 . . . . . . . . . . . . . . . . . . . . . . . . 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 1609 . . . . . . . . . . . . . . . . . . . . . . . 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 4441 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( vol* `  U. ran  ( (,) 
o.  f ) )  ->  ( y  <_  x 
<->  y  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) ) )
8887ralbidv 2882 . . . . . . . . . . . . . . . . . . . . . . . . 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 3196 . . . . . . . . . . . . . . . . . . . . . . . 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 671 . . . . . . . . . . . . . . . . . . . . . . 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 21141 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( topGen ` 
ran  (,) )  e.  Top
92 0cld 19412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
9391, 92ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )
94 0ss 3800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  (/)  C_  ( U. ran  ( (,)  o.  f )  i^i  A
)
95 0mbl 21823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (/)  e.  dom  vol
96 mblvol 21814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol* `  (/) ) )
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( vol `  (/) )  =  ( vol* `  (/) )
98 ovol0 21777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( vol* `  (/) )  =  0
9997, 98eqtr2i 2473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  =  ( vol `  (/) )
10094, 99pm3.2i 455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (/)  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  0  =  ( vol `  (/) ) )
101 sseq1 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  =  (/)  ->  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  <->  (/)  C_  ( U. ran  ( (,)  o.  f )  i^i  A
) ) )
102 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  =  (/)  ->  ( vol `  a )  =  ( vol `  (/) ) )
103102eqeq2d 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  =  (/)  ->  ( 0  =  ( vol `  a
)  <->  0  =  ( vol `  (/) ) ) )
104101, 103anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3196 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 672 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  0  =  ( vol `  a
) )
107 c0ex 9593 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  _V
108 eqeq1 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  0  ->  (
z  =  ( vol `  a )  <->  0  =  ( vol `  a ) ) )
109108anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3232 . . . . . . . . . . . . . . . . . . . . . . . . . 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 209 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  e.  { z  |  E. a  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) }
113112ne0ii 3777 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) }  =/=  (/)
114 suprcl 10509 . . . . . . . . . . . . . . . . . . . . . . . 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 )
115113, 114mp3an2 1313 . . . . . . . . . . . . . . . . . . . . . . 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 )
11674, 90, 115syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 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 )
117 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) )  ->  z  =  ( vol `  c ) )
118 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  =  c  ->  (
b  e.  dom  vol  <->  c  e.  dom  vol ) )
119118, 58vtoclga 3159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  c  e.  dom  vol )
120 mblvol 21814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  dom  vol  ->  ( vol `  c )  =  ( vol* `  c ) )
121119, 120syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  c )  =  ( vol* `  c
) )
122117, 121sylan9eqr 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) )  -> 
z  =  ( vol* `  c )
)
123122adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
124 difss2 3618 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  -> 
c  C_  U. ran  ( (,)  o.  f ) )
125124ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) )  -> 
c  C_  U. ran  ( (,)  o.  f ) )
126 ovolsscl 21770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )  ->  ( vol* `  c )  e.  RR )
12716, 126mp3an2 1313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol* `  c )  e.  RR )
128127ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  c  C_  U.
ran  ( (,)  o.  f ) )  -> 
( vol* `  c )  e.  RR )
129125, 128sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
130123, 129eqeltrd 2531 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
131130rexlimdvaa 2936 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
132131abssdv 3559 . . . . . . . . . . . . . . . . . . . . . . 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 )
133 eqeq1 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
z  =  ( vol `  c )  <->  y  =  ( vol `  c ) ) )
134133anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  y  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  y  =  ( vol `  c
) ) ) )
135134rexbidv 2954 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
136135ralab 3246 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
137 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  y  =  ( vol `  c ) )  ->  y  =  ( vol `  c ) )
138137, 121sylan9eqr 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  y  =  ( vol `  c
) ) )  -> 
y  =  ( vol* `  c )
)
139 ovolss 21769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR )  ->  ( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
140124, 16, 139sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  -> 
( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
141140ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  y  =  ( vol `  c
) ) )  -> 
( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
142138, 141eqbrtrd 4457 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  y  =  ( vol `  c
) ) )  -> 
y  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
143142rexlimiva 2931 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  y  =  ( vol `  c
) )  ->  y  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
144136, 143mpgbir 1609 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
14587ralbidv 2882 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
146145rspcev 3196 . . . . . . . . . . . . . . . . . . . . . . . 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 )
147144, 146mpan2 671 . . . . . . . . . . . . . . . . . . . . . . 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 )
148 0ss 3800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  (/)  C_  ( U. ran  ( (,)  o.  f )  \  A
)
149148, 99pm3.2i 455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (/)  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  0  =  ( vol `  (/) ) )
150 sseq1 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  (/)  ->  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  <->  (/)  C_  ( U. ran  ( (,)  o.  f )  \  A
) ) )
151 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  (/)  ->  ( vol `  c )  =  ( vol `  (/) ) )
152151eqeq2d 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  (/)  ->  ( 0  =  ( vol `  c
)  <->  0  =  ( vol `  (/) ) ) )
153150, 152anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  (/)  ->  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  0  =  ( vol `  c ) )  <-> 
( (/)  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  0  =  ( vol `  (/) ) ) ) )
154153rspcev 3196 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
15593, 149, 154mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  0  =  ( vol `  c
) )
156 eqeq1 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  0  ->  (
z  =  ( vol `  c )  <->  0  =  ( vol `  c ) ) )
157156anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  0  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  0  =  ( vol `  c
) ) ) )
158157rexbidv 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
159107, 158elab 3232 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
160155, 159mpbir 209 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }
161160ne0ii 3777 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }  =/=  (/)
162 suprcl 10509 . . . . . . . . . . . . . . . . . . . . . . . 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 )
163161, 162mp3an2 1313 . . . . . . . . . . . . . . . . . . . . . . 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 )
164132, 147, 163syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 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 )
165116, 164readdcld 9626 . . . . . . . . . . . . . . . . . . . . 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 )
166165adantl 466 . . . . . . . . . . . . . . . . . . . 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 )
167 simpr 461 . . . . . . . . . . . . . . . . . . . 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 )
1686ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 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 )
1699ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 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 )
170 ovolsscl 21770 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
17164, 16, 170mp3an12 1315 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol* `  ( U. ran  ( (,) 
o.  f )  i^i 
A ) )  e.  RR )
172171adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 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 )
173 difss 3616 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  f )
174 ovolsscl 21770 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
175173, 16, 174mp3an12 1315 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
176175adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 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 )
177 ssrin 3708 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( w  i^i  A
)  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )
)
17864, 16sstri 3498 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  C_  RR
179 ovolss 21769 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
180177, 178, 179sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol* `  ( w  i^i  A ) )  <_  ( vol* `  ( U. ran  ( (,)  o.  f )  i^i  A ) ) )
181180ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
182 ssdif 3624 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( w  \  A
)  C_  ( U. ran  ( (,)  o.  f
)  \  A )
)
183173, 16sstri 3498 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_  RR
184 ovolss 21769 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
185182, 183, 184sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol* `  ( w  \  A ) )  <_  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
186185ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
187168, 169, 172, 176, 181, 186le2addd 10176 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
188 dfin4 3723 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  =  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) )
189188fveq2i 5859 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( vol* `  ( U. ran  ( (,)  o.  f
)  i^i  A )
)  =  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  ( U. ran  ( (,)  o.  f
)  \  A )
) )
190189oveq1i 6291 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
191187, 190syl6breq 4476 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
192191adantlll 717 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
193 simpll 753 . . . . . . . . . . . . . . . . . . . . . 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 ,  <  ) ) )
194188sseq2i 3514 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  <->  a  C_  ( U. ran  ( (,) 
o.  f )  \ 
( U. ran  ( (,)  o.  f )  \  A ) ) )
195194anbi1i 695 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
196195rexbii 2945 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
197196abbii 2577 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) }
198197supeq1i 7909 . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  )
19916jctl 541 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( U. ran  ( (,)  o.  f )  C_  RR  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  e.  RR ) )
200199adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
201175, 183jctil 537 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  RR  /\  ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  e.  RR ) )
202201adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
203 ltso 9668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  <  Or  RR
204203a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  <  Or  RR )
205 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
206 vex 3098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  x  e. 
_V
207 eqeq1 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  x  ->  (
z  =  ( vol `  c )  <->  x  =  ( vol `  c ) ) )
208207anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  x  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) ) )
209208rexbidv 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
210206, 209elab 3232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
21116, 139mpan2 671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
212211ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_ 
U. ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) )  -> 
( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
21348cldss 19403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  c  C_  RR )
214 ovolcl 21762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c 
C_  RR  ->  ( vol* `  c )  e.  RR* )
215213, 214syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol* `  c )  e. 
RR* )
216 xrlenlt 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
217215, 34, 216sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( ( vol* `  c )  <_  ( vol* `  U. ran  ( (,) 
o.  f ) )  <->  -.  ( vol* `  U. ran  ( (,)  o.  f ) )  < 
( vol* `  c ) ) )
218217adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
219 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( vol `  c
)  ->  x  =  ( vol `  c ) )
220219, 121sylan9eqr 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  x  =  ( vol `  c ) )  ->  x  =  ( vol* `  c
) )
221 breq2 4441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( vol* `  c )  ->  (
( vol* `  U. ran  ( (,)  o.  f ) )  < 
x  <->  ( vol* `  U. ran  ( (,) 
o.  f ) )  <  ( vol* `  c ) ) )
222221notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  =  ( vol* `  c )  ->  ( -.  ( vol* `  U. ran  ( (,)  o.  f ) )  < 
x  <->  -.  ( vol* `  U. ran  ( (,)  o.  f ) )  <  ( vol* `  c ) ) )
223220, 222syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  x  =  ( vol `  c ) )  ->  ( -.  ( vol* `  U. ran  ( (,)  o.  f
) )  <  x  <->  -.  ( vol* `  U. ran  ( (,)  o.  f ) )  < 
( vol* `  c ) ) )
224223adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
225218, 224bitr4d 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
226212, 225mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_ 
U. ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) )  ->  -.  ( vol* `  U. ran  ( (,)  o.  f ) )  < 
x )
227226rexlimiva 2931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) )  ->  -.  ( vol* `  U. ran  ( (,)  o.  f
) )  <  x
)
228210, 227sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
229228adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
230 retopbas 21140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ran  (,)  e. 
TopBases
231 bastg 19340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ran 
(,)  e.  TopBases  ->  ran  (,)  C_  ( topGen `  ran  (,) )
)
232230, 231ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ran  (,)  C_  ( topGen `  ran  (,) )
23313, 232sstri 3498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
234 uniopn 19279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
)
23591, 233, 234mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
236 mblfinlem2 30027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
237235, 236mp3an1 1312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
238121eqcomd 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol* `  c )  =  ( vol `  c
) )
239238anim1i 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  x  <  ( vol* `  c
) )  ->  (
( vol* `  c )  =  ( vol `  c )  /\  x  <  ( vol* `  c ) ) )
240239ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( x  <  ( vol* `  c )  ->  (
( vol* `  c )  =  ( vol `  c )  /\  x  <  ( vol* `  c ) ) ) )
241240anim2d 565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
242 fvex 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( vol* `  c )  e.  _V
243 eqeq1 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  ( vol* `  c )  ->  (
y  =  ( vol `  c )  <->  ( vol* `  c )  =  ( vol `  c
) ) )
244243anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  ( vol* `  c )  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  y  =  ( vol `  c ) )  <->  ( c  C_  U.
ran  ( (,)  o.  f )  /\  ( vol* `  c )  =  ( vol `  c
) ) ) )
245 breq2 4441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  ( vol* `  c )  ->  (
x  <  y  <->  x  <  ( vol* `  c
) ) )
246244, 245anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
247242, 246spcev 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
248247anasss 647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
249241, 248syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
250249reximia 2909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
251237, 250syl 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 ) )
252 r19.41v 2995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
253252exbii 1654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
254 rexcom4 3115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
255133anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  y  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) ) ) )
256255rexbidv 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
257256rexab 3248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
258253, 254, 2573bitr4i 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
259251, 258sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
260259adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
261204, 205, 229, 260eqsupd 7919 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
262261eqcomd 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  ) )
263262adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  ) )
264 sseq1 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
c  C_  U. ran  ( (,)  o.  f )  <->  a  C_  U.
ran  ( (,)  o.  f ) ) )
265 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  ( vol `  c )  =  ( vol `  a
) )
266265eqeq2d 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
z  =  ( vol `  c )  <->  z  =  ( vol `  a ) ) )
267264, 266anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  a  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( a  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  a
) ) ) )
268267cbvrexv 3071 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
269268abbii 2577 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) }
270269supeq1i 7909 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  )
271263, 270syl6eq 2500 . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  ) )
272 sseq1 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  <->  a 
C_  ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
273272, 266anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  a  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( a  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  a
) ) ) )
274273cbvrexv 3071 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
275274abbii 2577 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) }
276275supeq1i 7909 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  )
277 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
278 eqeq1 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  z  ->  (
y  =  ( vol `  b )  <->  z  =  ( vol `  b ) ) )
279278anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  z  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  z  =  ( vol `  b ) ) ) )
280279rexbidv 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
281 sseq1 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( b  =  c  ->  (
b  C_  A  <->  c  C_  A ) )
282 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( b  =  c  ->  ( vol `  b )  =  ( vol `  c
) )
283282eqeq2d 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( b  =  c  ->  (
z  =  ( vol `  b )  <->  z  =  ( vol `  c ) ) )
284281, 283anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( b  =  c  ->  (
( b  C_  A  /\  z  =  ( vol `  b ) )  <-> 
( c  C_  A  /\  z  =  ( vol `  c ) ) ) )
285284cbvrexv 3071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
286280, 285syl6bb 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
287286cbvabv 2586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) }
288287supeq1i 7909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  )
289288eqeq2i 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  ) )
290289biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  ) )
291290ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  ) )
292 mblfinlem3 30028 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 `  c
) ) } ,  RR ,  <  )  /\  ( vol* `  A
)  =  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  A  /\  z  =  ( vol `  c ) ) } ,  RR ,  <  ) ) )  ->  sup ( { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) } ,  RR ,  <  )  =  ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) ) )
293200, 277, 263, 291, 292syl112anc 1233 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  )