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

Theorem ismblfin 28458
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 28457 . 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 3890 . . . . 5  |-  ( w  e.  ~P RR  ->  w 
C_  RR )
3 elmapi 7255 . . . . . . . . . . . 12  |-  ( f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
4 inss1 3591 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  i^i  A )  C_  w
5 ovolsscl 20991 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  i^i  A
)  C_  w  /\  w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  i^i  A ) )  e.  RR )
64, 5mp3an1 1301 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  i^i  A ) )  e.  RR )
7 difss 3504 . . . . . . . . . . . . . . . . . . . 20  |-  ( w 
\  A )  C_  w
8 ovolsscl 20991 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  \  A
)  C_  w  /\  w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  \  A ) )  e.  RR )
97, 8mp3an1 1301 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  \  A ) )  e.  RR )
106, 9readdcld 9434 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( ( vol* `  ( w  i^i  A
) )  +  ( vol* `  (
w  \  A )
) )  e.  RR )
1110rexrd 9454 . . . . . . . . . . . . . . . . 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 5121 . . . . . . . . . . . . . . . . . . 19  |-  ran  ( (,)  o.  f )  C_  ran  (,)
1413unissi 4135 . . . . . . . . . . . . . . . . . 18  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  (,)
15 unirnioo 11410 . . . . . . . . . . . . . . . . . 18  |-  RR  =  U. ran  (,)
1614, 15sseqtr4i 3410 . . . . . . . . . . . . . . . . 17  |-  U. ran  ( (,)  o.  f ) 
C_  RR
17 ovolcl 20983 . . . . . . . . . . . . . . . . 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 20978 . . . . . . . . . . . . . . . . . 18  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo ) )
22 frn 5586 . . . . . . . . . . . . . . . . . . 19  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  ( 0 [,) +oo ) )
23 icossxr 11401 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,) +oo )  C_  RR*
2422, 23syl6ss 3389 . . . . . . . . . . . . . . . . . 18  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  RR* )
25 supxrcl 11298 . . . . . . . . . . . . . . . . . 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 11131 . . . . . . . . . . . . . . . . . . . . . 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 4339 . . . . . . . . . . . . . . . . . . 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 11159 . . . . . . . . . . . . . . . . . . . . . 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 2690 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  < +oo  <->  ( vol* `  U. ran  ( (,)  o.  f ) )  =/= +oo )
38 ovolge0 20986 . . . . . . . . . . . . . . . . . . . . . 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 9407 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
41 xrre3 11164 . . . . . . . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  =  a  ->  (
b  e.  dom  vol  <->  a  e.  dom  vol ) )
48 uniretop 20363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  RR  =  U. ( topGen `  ran  (,) )
4948cldss 18655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
50 dfss4 3605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
5149, 50sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
52 rembl 21044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  RR  e.  dom  vol
5348cldopn 18657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
54 opnmbl 21104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 21046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
5947, 58vtoclga 3057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  a  e.  dom  vol )
60 mblvol 21035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  dom  vol  ->  ( vol `  a )  =  ( vol* `  a ) )
6159, 60syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  a )  =  ( vol* `  a
) )
6246, 61sylan9eqr 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  C_ 
U. ran  ( (,)  o.  f )
65 sstr 3385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 20991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1302 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . . . . . . . . . . . . . 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 2863 . . . . . . . . . . . . . . . . . . . . . . . 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 3447 . . . . . . . . . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2757 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3141 . . . . . . . . . . . . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  y  =  ( vol `  a
) ) )  -> 
y  =  ( vol* `  a )
)
81 ovolss 20990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4333 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2857 . . . . . . . . . . . . . . . . . . . . . . . . 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 1595 . . . . . . . . . . . . . . . . . . . . . . . 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 4317 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( vol* `  U. ran  ( (,) 
o.  f ) )  ->  ( y  <_  x 
<->  y  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) ) )
8887ralbidv 2756 . . . . . . . . . . . . . . . . . . . . . . . . 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 3094 . . . . . . . . . . . . . . . . . . . . . . . 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 20362 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( topGen ` 
ran  (,) )  e.  Top
92 0cld 18664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
9391, 92ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )
94 0ss 3687 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  (/)  C_  ( U. ran  ( (,)  o.  f )  i^i  A
)
95 0mbl 21043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (/)  e.  dom  vol
96 mblvol 21035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol* `  (/) ) )
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( vol `  (/) )  =  ( vol* `  (/) )
98 ovol0 20998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( vol* `  (/) )  =  0
9997, 98eqtr2i 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  =  ( vol `  (/) )
10094, 99pm3.2i 455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (/)  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  0  =  ( vol `  (/) ) )
101 sseq1 3398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  =  (/)  ->  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  <->  (/)  C_  ( U. ran  ( (,)  o.  f )  i^i  A
) ) )
102 fveq2 5712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  =  (/)  ->  ( vol `  a )  =  ( vol `  (/) ) )
103102eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3094 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  _V
108 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3127 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) }
113 ne0i 3664 . . . . . . . . . . . . . . . . . . . . . . . . 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 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) }  =/=  (/)
115 suprcl 10311 . . . . . . . . . . . . . . . . . . . . . . . 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 1302 . . . . . . . . . . . . . . . . . . . . . . 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 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 )
118 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) )  ->  z  =  ( vol `  c ) )
119 eleq1 2503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  =  c  ->  (
b  e.  dom  vol  <->  c  e.  dom  vol ) )
120119, 58vtoclga 3057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  c  e.  dom  vol )
121 mblvol 21035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  dom  vol  ->  ( vol `  c )  =  ( vol* `  c ) )
122120, 121syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  c )  =  ( vol* `  c
) )
123118, 122sylan9eqr 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) )  -> 
z  =  ( vol* `  c )
)
124123adantl 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
) )
125 difss2 3506 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  -> 
c  C_  U. ran  ( (,)  o.  f ) )
126125ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) )  -> 
c  C_  U. ran  ( (,)  o.  f ) )
127 ovolsscl 20991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1302 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol* `  c )  e.  RR )
129128ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  c  C_  U.
ran  ( (,)  o.  f ) )  -> 
( vol* `  c )  e.  RR )
130126, 129sylan2 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 )
131124, 130eqeltrd 2517 . . . . . . . . . . . . . . . . . . . . . . . . 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 2863 . . . . . . . . . . . . . . . . . . . . . . . 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 3447 . . . . . . . . . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
z  =  ( vol `  c )  <->  y  =  ( vol `  c ) ) )
135134anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  y  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  y  =  ( vol `  c
) ) ) )
136135rexbidv 2757 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3141 . . . . . . . . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  y  =  ( vol `  c ) )  ->  y  =  ( vol `  c ) )
139138, 122sylan9eqr 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  y  =  ( vol `  c
) ) )  -> 
y  =  ( vol* `  c )
)
140 ovolss 20990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR )  ->  ( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
141125, 16, 140sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  -> 
( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
142141ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4333 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  y  =  ( vol `  c
) ) )  -> 
y  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
144143rexlimiva 2857 . . . . . . . . . . . . . . . . . . . . . . . . 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 1595 . . . . . . . . . . . . . . . . . . . . . . . 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 2756 . . . . . . . . . . . . . . . . . . . . . . . . 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 3094 . . . . . . . . . . . . . . . . . . . . . . . 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 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 )
149 0ss 3687 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  (/)  C_  ( U. ran  ( (,)  o.  f )  \  A
)
150149, 99pm3.2i 455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (/)  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  0  =  ( vol `  (/) ) )
151 sseq1 3398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  (/)  ->  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  <->  (/)  C_  ( U. ran  ( (,)  o.  f )  \  A
) ) )
152 fveq2 5712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  (/)  ->  ( vol `  c )  =  ( vol `  (/) ) )
153152eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  (/)  ->  ( 0  =  ( vol `  c
)  <->  0  =  ( vol `  (/) ) ) )
154151, 153anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  (/)  ->  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  0  =  ( vol `  c ) )  <-> 
( (/)  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  0  =  ( vol `  (/) ) ) ) )
155154rspcev 3094 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 672 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  0  =  ( vol `  c
) )
157 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  0  ->  (
z  =  ( vol `  c )  <->  0  =  ( vol `  c ) ) )
158157anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  0  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  0  =  ( vol `  c
) ) ) )
159158rexbidv 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3127 . . . . . . . . . . . . . . . . . . . . . . . . . 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 209 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  e.  { z  |  E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }
162 ne0i 3664 . . . . . . . . . . . . . . . . . . . . . . . . 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 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }  =/=  (/)
164 suprcl 10311 . . . . . . . . . . . . . . . . . . . . . . . 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 1302 . . . . . . . . . . . . . . . . . . . . . . 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 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 )
167117, 166readdcld 9434 . . . . . . . . . . . . . . . . . . . . 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 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 )
169 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 )
1706ad2antrr 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 )
1719ad2antrr 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 )
172 ovolsscl 20991 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1304 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol* `  ( U. ran  ( (,) 
o.  f )  i^i 
A ) )  e.  RR )
174173adantl 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 )
175 difss 3504 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  f )
176 ovolsscl 20991 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1304 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
178177adantl 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 )
179 ssrin 3596 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( w  i^i  A
)  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )
)
18064, 16sstri 3386 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  C_  RR
181 ovolss 20990 . . . . . . . . . . . . . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol* `  ( w  i^i  A ) )  <_  ( vol* `  ( U. ran  ( (,)  o.  f )  i^i  A ) ) )
183182ad2antlr 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 ) ) )
184 ssdif 3512 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( w  \  A
)  C_  ( U. ran  ( (,)  o.  f
)  \  A )
)
185175, 16sstri 3386 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_  RR
186 ovolss 20990 . . . . . . . . . . . . . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol* `  ( w  \  A ) )  <_  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
188187ad2antlr 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 ) ) )
189170, 171, 174, 178, 183, 188le2addd 9978 . . . . . . . . . . . . . . . . . . . . . . 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 3611 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  =  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) )
191190fveq2i 5715 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( vol* `  ( U. ran  ( (,)  o.  f
)  i^i  A )
)  =  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  ( U. ran  ( (,)  o.  f
)  \  A )
) )
192191oveq1i 6122 . . . . . . . . . . . . . . . . . . . . . . 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 4352 . . . . . . . . . . . . . . . . . . . . . 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 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 ) ) ) )
195 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 ,  <  ) ) )
196190sseq2i 3402 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  <->  a  C_  ( U. ran  ( (,) 
o.  f )  \ 
( U. ran  ( (,)  o.  f )  \  A ) ) )
197196anbi1i 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
) ) )
198197rexbii 2761 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2561 . . . . . . . . . . . . . . . . . . . . . . . . 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 7718 . . . . . . . . . . . . . . . . . . . . . . . 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 541 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( U. ran  ( (,)  o.  f )  C_  RR  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  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 ) 
C_  RR  /\  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR ) )
203177, 185jctil 537 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  RR  /\  ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  e.  RR ) )
204203adantl 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 ) )
205 ltso 9476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  <  Or  RR
206205a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  <  Or  RR )
207 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
208 vex 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  x  e. 
_V
209 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  x  ->  (
z  =  ( vol `  c )  <->  x  =  ( vol `  c ) ) )
210209anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  x  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) ) )
211210rexbidv 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
214213ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_ 
U. ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) )  -> 
( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
21548cldss 18655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  c  C_  RR )
216 ovolcl 20983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c 
C_  RR  ->  ( vol* `  c )  e.  RR* )
217215, 216syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol* `  c )  e. 
RR* )
218 xrlenlt 9463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( ( vol* `  c )  <_  ( vol* `  U. ran  ( (,) 
o.  f ) )  <->  -.  ( vol* `  U. ran  ( (,)  o.  f ) )  < 
( vol* `  c ) ) )
220219adantr 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 ) ) )
221 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( vol `  c
)  ->  x  =  ( vol `  c ) )
222221, 122sylan9eqr 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  x  =  ( vol `  c ) )  ->  x  =  ( vol* `  c
) )
223 breq2 4317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( vol* `  c )  ->  (
( vol* `  U. ran  ( (,)  o.  f ) )  < 
x  <->  ( vol* `  U. ran  ( (,) 
o.  f ) )  <  ( vol* `  c ) ) )
224223notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 )
) )
227220, 226bitr4d 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 ) )
228214, 227mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_ 
U. ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) )  ->  -.  ( vol* `  U. ran  ( (,)  o.  f ) )  < 
x )
229228rexlimiva 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. c  e.  ( Clsd `  ( topGen `  ran  (,) )
) ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) )  ->  -.  ( vol* `  U. ran  ( (,)  o.  f
) )  <  x
)
230212, 229sylbi 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 )
231230adantl 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 )
232 retopbas 20361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ran  (,)  e. 
TopBases
233 bastg 18593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ran 
(,)  e.  TopBases  ->  ran  (,)  C_  ( topGen `  ran  (,) )
)
234232, 233ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ran  (,)  C_  ( topGen `  ran  (,) )
23513, 234sstri 3386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
236 uniopn 18532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
)
23791, 235, 236mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
238 mblfinlem2 28455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol* `  c )  =  ( vol `  c
) )
241240anim1i 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  x  <  ( vol* `  c
) )  ->  (
( vol* `  c )  =  ( vol `  c )  /\  x  <  ( vol* `  c ) ) )
242241ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( x  <  ( vol* `  c )  ->  (
( vol* `  c )  =  ( vol `  c )  /\  x  <  ( vol* `  c ) ) ) )
243242anim2d 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
) ) ) ) )
244 fvex 5722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( vol* `  c )  e.  _V
245 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  ( vol* `  c )  ->  (
y  =  ( vol `  c )  <->  ( vol* `  c )  =  ( vol `  c
) ) )
246245anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  ( vol* `  c )  ->  (
x  <  y  <->  x  <  ( vol* `  c
) ) )
248246, 247anbi12d 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 ) ) ) )
249244, 248spcev 3085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 ) )
251243, 250syl6 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 ) ) )
252251reximia 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  y  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) ) ) )
258257rexbidv 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 )
261253, 260sylib 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 )
262261adantl 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 )
263206, 207, 231, 262eqsupd 7728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 ,  <  ) )
266 sseq1 3398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
c  C_  U. ran  ( (,)  o.  f )  <->  a  C_  U.
ran  ( (,)  o.  f ) ) )
267 fveq2 5712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  ( vol `  c )  =  ( vol `  a
) )
268267eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
z  =  ( vol `  c )  <->  z  =  ( vol `  a ) ) )
269266, 268anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  a  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( a  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  a
) ) ) )
270269cbvrexv 2969 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2561 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7718 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2491 . . . . . . . . . . . . . . . . . . . . . . . . 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 3398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  <->  a 
C_  ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
275274, 268anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  a  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( a  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  a
) ) ) )
276275cbvrexv 2969 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2561 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7718 . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 ) )
280 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  z  ->  (
y  =  ( vol `  b )  <->  z  =  ( vol `  b ) ) )
281280anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  z  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  z  =  ( vol `  b ) ) ) )
282281rexbidv 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( b  =  c  ->  (
b  C_  A  <->  c  C_  A ) )
284 fveq2 5712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( b  =  c  ->  ( vol `  b )  =  ( vol `  c
) )
285284eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( b  =  c  ->  (
z  =  ( vol `  b )  <->  z  =  ( vol `  c ) ) )
286283, 285anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( b  =  c  ->  (
( b  C_  A  /\  z  =  ( vol `  b ) )  <-> 
( c  C_  A  /\  z  =  ( vol `  c ) ) ) )
287286cbvrexv 2969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 ) ) ) )
289288cbvabv 2570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 ,  <  ) )
293292ad2antlr 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 ,  <  ) )
294 mblfinlem3 28456 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) } ,