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

Theorem ismblfin 30295
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 30294 . 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 4008 . . . . 5  |-  ( w  e.  ~P RR  ->  w 
C_  RR )
3 elmapi 7433 . . . . . . . . . . . 12  |-  ( f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN )  ->  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
4 inss1 3704 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  i^i  A )  C_  w
5 ovolsscl 22063 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  i^i  A
)  C_  w  /\  w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  i^i  A ) )  e.  RR )
64, 5mp3an1 1309 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  i^i  A ) )  e.  RR )
7 difss 3617 . . . . . . . . . . . . . . . . . . . 20  |-  ( w 
\  A )  C_  w
8 ovolsscl 22063 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  \  A
)  C_  w  /\  w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  \  A ) )  e.  RR )
97, 8mp3an1 1309 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( vol* `  ( w  \  A ) )  e.  RR )
106, 9readdcld 9612 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( ( vol* `  ( w  i^i  A
) )  +  ( vol* `  (
w  \  A )
) )  e.  RR )
1110rexrd 9632 . . . . . . . . . . . . . . . . 17  |-  ( ( w  C_  RR  /\  ( vol* `  w )  e.  RR )  -> 
( ( vol* `  ( w  i^i  A
) )  +  ( vol* `  (
w  \  A )
) )  e.  RR* )
1211ad3antlr 728 . . . . . . . . . . . . . . . 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 5252 . . . . . . . . . . . . . . . . . . 19  |-  ran  ( (,)  o.  f )  C_  ran  (,)
1413unissi 4258 . . . . . . . . . . . . . . . . . 18  |-  U. ran  ( (,)  o.  f ) 
C_  U. ran  (,)
15 unirnioo 11627 . . . . . . . . . . . . . . . . . 18  |-  RR  =  U. ran  (,)
1614, 15sseqtr4i 3522 . . . . . . . . . . . . . . . . 17  |-  U. ran  ( (,)  o.  f ) 
C_  RR
17 ovolcl 22055 . . . . . . . . . . . . . . . . 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 2454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( abs  o.  -  )  o.  f )  =  ( ( abs  o.  -  )  o.  f )
20 eqid 2454 . . . . . . . . . . . . . . . . . . 19  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
2119, 20ovolsf 22050 . . . . . . . . . . . . . . . . . 18  |-  ( f : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo ) )
22 frn 5719 . . . . . . . . . . . . . . . . . . 19  |-  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) : NN --> ( 0 [,) +oo )  ->  ran  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  C_  ( 0 [,) +oo ) )
23 icossxr 11612 . . . . . . . . . . . . . . . . . . 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 11509 . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . 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 11342 . . . . . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . 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 4465 . . . . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . . . 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 11370 . . . . . . . . . . . . . . . . . . . . . 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 2720 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  < +oo  <->  ( vol* `  U. ran  ( (,)  o.  f ) )  =/= +oo )
38 ovolge0 22058 . . . . . . . . . . . . . . . . . . . . . 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 9585 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
41 xrre3 11375 . . . . . . . . . . . . . . . . . . . . . 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 680 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  <_  ( vol* `  U. ran  ( (,)  o.  f ) )  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  < +oo )  ->  ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR )
4339, 42mpan 668 . . . . . . . . . . . . . . . . . . . 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 728 . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  z  =  ( vol `  a ) )  ->  z  =  ( vol `  a ) )
47 eleq1 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  =  a  ->  (
b  e.  dom  vol  <->  a  e.  dom  vol ) )
48 uniretop 21435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  RR  =  U. ( topGen `  ran  (,) )
4948cldss 19697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  C_  RR )
50 dfss4 3729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( b 
C_  RR  <->  ( RR  \ 
( RR  \  b
) )  =  b )
5149, 50sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  =  b )
52 rembl 22117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  RR  e.  dom  vol
5348cldopn 19699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  b )  e.  (
topGen `  ran  (,) )
)
54 opnmbl 22177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 22119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( RR  e.  dom  vol  /\  ( RR  \  b
)  e.  dom  vol )  ->  ( RR  \ 
( RR  \  b
) )  e.  dom  vol )
5752, 55, 56sylancr 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( RR  \  ( RR  \  b
) )  e.  dom  vol )
5851, 57eqeltrrd 2543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  b  e.  dom  vol )
5947, 58vtoclga 3170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  a  e.  dom  vol )
60 mblvol 22107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  dom  vol  ->  ( vol `  a )  =  ( vol* `  a ) )
6159, 60syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  a )  =  ( vol* `  a
) )
6246, 61sylan9eqr 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) )  -> 
z  =  ( vol* `  a )
)
6362adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  -> 
a  C_  U. ran  ( (,)  o.  f ) )
6766ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 22063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1310 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol* `  a )  e.  RR )
7069ancoms 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  a  C_  U.
ran  ( (,)  o.  f ) )  -> 
( vol* `  a )  e.  RR )
7167, 70sylan2 472 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2542 . . . . . . . . . . . . . . . . . . . . . . . . 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 2947 . . . . . . . . . . . . . . . . . . . . . . . 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 3560 . . . . . . . . . . . . . . . . . . . . . . 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 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
z  =  ( vol `  a )  <->  y  =  ( vol `  a ) ) )
7675anbi2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2965 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3257 . . . . . . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  C_  ( U. ran  ( (,)  o.  f
)  i^i  A )  /\  y  =  ( vol `  a ) )  ->  y  =  ( vol `  a ) )
8079, 61sylan9eqr 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( a  C_  ( U. ran  ( (,)  o.  f )  i^i 
A )  /\  y  =  ( vol `  a
) ) )  -> 
y  =  ( vol* `  a )
)
81 ovolss 22062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( a  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR )  ->  ( vol* `  a )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
8266, 16, 81sylancl 660 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a 
C_  ( U. ran  ( (,)  o.  f )  i^i  A )  -> 
( vol* `  a )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
8382ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4459 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2942 . . . . . . . . . . . . . . . . . . . . . . . . 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 1627 . . . . . . . . . . . . . . . . . . . . . . . 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 4443 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( vol* `  U. ran  ( (,) 
o.  f ) )  ->  ( y  <_  x 
<->  y  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) ) )
8887ralbidv 2893 . . . . . . . . . . . . . . . . . . . . . . . . 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 3207 . . . . . . . . . . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . . . . . . . . . . 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 21434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( topGen ` 
ran  (,) )  e.  Top
92 0cld 19706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
9391, 92ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )
94 0ss 3813 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  (/)  C_  ( U. ran  ( (,)  o.  f )  i^i  A
)
95 0mbl 22116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (/)  e.  dom  vol
96 mblvol 22107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (/)  e.  dom  vol  ->  ( vol `  (/) )  =  ( vol* `  (/) ) )
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( vol `  (/) )  =  ( vol* `  (/) )
98 ovol0 22070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( vol* `  (/) )  =  0
9997, 98eqtr2i 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  =  ( vol `  (/) )
10094, 99pm3.2i 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  =  (/)  ->  ( vol `  a )  =  ( vol `  (/) ) )
103102eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  =  (/)  ->  ( 0  =  ( vol `  a
)  <->  0  =  ( vol `  (/) ) ) )
104101, 103anbi12d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 670 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  0  =  ( vol `  a
) )
107 c0ex 9579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  _V
108 eqeq1 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  0  ->  (
z  =  ( vol `  a )  <->  0  =  ( vol `  a ) ) )
109108anbi2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2965 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3243 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3790 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  |  E. a  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( a  C_  ( U. ran  ( (,) 
o.  f )  i^i 
A )  /\  z  =  ( vol `  a
) ) }  =/=  (/)
114 suprcl 10498 . . . . . . . . . . . . . . . . . . . . . . . 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 1310 . . . . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  z  =  ( vol `  c ) )  ->  z  =  ( vol `  c ) )
118 eleq1 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  =  c  ->  (
b  e.  dom  vol  <->  c  e.  dom  vol ) )
119118, 58vtoclga 3170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  c  e.  dom  vol )
120 mblvol 22107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  dom  vol  ->  ( vol `  c )  =  ( vol* `  c ) )
121119, 120syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol `  c )  =  ( vol* `  c
) )
122117, 121sylan9eqr 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) )  -> 
z  =  ( vol* `  c )
)
123122adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3619 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  -> 
c  C_  U. ran  ( (,)  o.  f ) )
125124ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  z  =  ( vol `  c
) ) )  -> 
c  C_  U. ran  ( (,)  o.  f ) )
126 ovolsscl 22063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1310 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR )  ->  ( vol* `  c )  e.  RR )
128127ancoms 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( vol* `  U. ran  ( (,)  o.  f ) )  e.  RR  /\  c  C_  U.
ran  ( (,)  o.  f ) )  -> 
( vol* `  c )  e.  RR )
129125, 128sylan2 472 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2542 . . . . . . . . . . . . . . . . . . . . . . . . 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 2947 . . . . . . . . . . . . . . . . . . . . . . . 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 3560 . . . . . . . . . . . . . . . . . . . . . . 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 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
z  =  ( vol `  c )  <->  y  =  ( vol `  c ) ) )
134133anbi2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  y  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  y  =  ( vol `  c
) ) ) )
135134rexbidv 2965 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3257 . . . . . . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  y  =  ( vol `  c ) )  ->  y  =  ( vol `  c ) )
138137, 121sylan9eqr 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  y  =  ( vol `  c
) ) )  -> 
y  =  ( vol* `  c )
)
139 ovolss 22062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( c  C_  U. ran  ( (,)  o.  f )  /\  U.
ran  ( (,)  o.  f )  C_  RR )  ->  ( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
140124, 16, 139sylancl 660 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c 
C_  ( U. ran  ( (,)  o.  f ) 
\  A )  -> 
( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
141140ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4459 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_  ( U. ran  ( (,)  o.  f )  \  A )  /\  y  =  ( vol `  c
) ) )  -> 
y  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
143142rexlimiva 2942 . . . . . . . . . . . . . . . . . . . . . . . . 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 1627 . . . . . . . . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . . . . . . . . . . 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 3207 . . . . . . . . . . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . . . . . . . . . . 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 3813 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  (/)  C_  ( U. ran  ( (,)  o.  f )  \  A
)
149148, 99pm3.2i 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  (/)  ->  ( vol `  c )  =  ( vol `  (/) ) )
152151eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  (/)  ->  ( 0  =  ( vol `  c
)  <->  0  =  ( vol `  (/) ) ) )
153150, 152anbi12d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  (/)  ->  ( ( c  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  0  =  ( vol `  c ) )  <-> 
( (/)  C_  ( U. ran  ( (,)  o.  f
)  \  A )  /\  0  =  ( vol `  (/) ) ) ) )
154153rspcev 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 670 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  0  =  ( vol `  c
) )
156 eqeq1 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  0  ->  (
z  =  ( vol `  c )  <->  0  =  ( vol `  c ) ) )
157156anbi2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  0  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  0  =  ( vol `  c
) ) ) )
158157rexbidv 2965 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3243 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3790 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  |  E. c  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( c  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  c
) ) }  =/=  (/)
162 suprcl 10498 . . . . . . . . . . . . . . . . . . . . . . . 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 1310 . . . . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . . . . 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 9612 . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . . . . . . . . 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 22063 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1312 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol* `  ( U. ran  ( (,) 
o.  f )  i^i 
A ) )  e.  RR )
172171adantl 464 . . . . . . . . . . . . . . . . . . . . . . . 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 3617 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( U. ran  ( (,)  o.  f
)  \  A )  C_ 
U. ran  ( (,)  o.  f )
174 ovolsscl 22063 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1312 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( vol* `  ( U. ran  ( (,) 
o.  f )  \  A ) )  e.  RR )
176175adantl 464 . . . . . . . . . . . . . . . . . . . . . . . 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 3709 . . . . . . . . . . . . . . . . . . . . . . . . . 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 22062 . . . . . . . . . . . . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol* `  ( w  i^i  A ) )  <_  ( vol* `  ( U. ran  ( (,)  o.  f )  i^i  A ) ) )
181180ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . 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 3625 . . . . . . . . . . . . . . . . . . . . . . . . . 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 22062 . . . . . . . . . . . . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol* `  ( w  \  A ) )  <_  ( vol* `  ( U. ran  ( (,)  o.  f ) 
\  A ) ) )
186185ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . 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 10166 . . . . . . . . . . . . . . . . . . . . . . 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 3735 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( U. ran  ( (,)  o.  f
)  i^i  A )  =  ( U. ran  ( (,)  o.  f ) 
\  ( U. ran  ( (,)  o.  f ) 
\  A ) )
189188fveq2i 5851 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( vol* `  ( U. ran  ( (,)  o.  f
)  i^i  A )
)  =  ( vol* `  ( U. ran  ( (,)  o.  f
)  \  ( U. ran  ( (,)  o.  f
)  \  A )
) )
190189oveq1i 6280 . . . . . . . . . . . . . . . . . . . . . . 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 4478 . . . . . . . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . . . . . . 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 751 . . . . . . . . . . . . . . . . . . . . . 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 693 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2956 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2588 . . . . . . . . . . . . . . . . . . . . . . . . 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 7898 . . . . . . . . . . . . . . . . . . . . . . . 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 539 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( U. ran  ( (,)  o.  f )  C_  RR  /\  ( vol* `  U. ran  ( (,) 
o.  f ) )  e.  RR ) )
200199adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . 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 535 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( vol* `  U. ran  ( (,)  o.  f
) )  e.  RR  ->  ( ( U. ran  ( (,)  o.  f ) 
\  A )  C_  RR  /\  ( vol* `  ( U. ran  ( (,)  o.  f )  \  A ) )  e.  RR ) )
202201adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . 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 9654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  x  e. 
_V
207 eqeq1 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  x  ->  (
z  =  ( vol `  c )  <->  x  =  ( vol `  c ) ) )
208207anbi2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  x  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( c  C_  U.
ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) ) )
209208rexbidv 2965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c 
C_  U. ran  ( (,) 
o.  f )  -> 
( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
212211ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( c  C_ 
U. ran  ( (,)  o.  f )  /\  x  =  ( vol `  c
) ) )  -> 
( vol* `  c )  <_  ( vol* `  U. ran  ( (,)  o.  f ) ) )
21348cldss 19697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  c  C_  RR )
214 ovolcl 22055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c 
C_  RR  ->  ( vol* `  c )  e.  RR* )
215213, 214syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol* `  c )  e. 
RR* )
216 xrlenlt 9641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( ( vol* `  c )  <_  ( vol* `  U. ran  ( (,) 
o.  f ) )  <->  -.  ( vol* `  U. ran  ( (,)  o.  f ) )  < 
( vol* `  c ) ) )
218217adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  x  =  ( vol `  c ) )  ->  x  =  ( vol* `  c
) )
221 breq2 4443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( vol* `  c )  ->  (
( vol* `  U. ran  ( (,)  o.  f ) )  < 
x  <->  ( vol* `  U. ran  ( (,) 
o.  f ) )  <  ( vol* `  c ) ) )
222221notbid 292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 21433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ran  (,)  e. 
TopBases
231 bastg 19634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 19573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ran  ( (,)  o.  f )  C_  ( topGen `  ran  (,) )
)  ->  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
)
23591, 233, 234mp2an 670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  U. ran  ( (,)  o.  f )  e.  ( topGen `  ran  (,) )
236 mblfinlem2 30292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( vol* `  c )  =  ( vol `  c
) )
239238anim1i 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  x  <  ( vol* `  c
) )  ->  (
( vol* `  c )  =  ( vol `  c )  /\  x  <  ( vol* `  c ) ) )
240239ex 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  e.  ( Clsd `  ( topGen `
 ran  (,) )
)  ->  ( x  <  ( vol* `  c )  ->  (
( vol* `  c )  =  ( vol `  c )  /\  x  <  ( vol* `  c ) ) ) )
241240anim2d 563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( vol* `  c )  e.  _V
243 eqeq1 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  ( vol* `  c )  ->  (
y  =  ( vol `  c )  <->  ( vol* `  c )  =  ( vol `  c
) ) )
244243anbi2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  ( vol* `  c )  ->  (
x  <  y  <->  x  <  ( vol* `  c
) ) )
246244, 245anbi12d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  y  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( c  C_  U.
ran  ( (,)  o.  f )  /\  y  =  ( vol `  c
) ) ) )
256255rexbidv 2965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7908 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  a  ->  ( vol `  c )  =  ( vol `  a
) )
266265eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  a  ->  (
z  =  ( vol `  c )  <->  z  =  ( vol `  a ) ) )
267264, 266anbi12d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  a  ->  (
( c  C_  U. ran  ( (,)  o.  f )  /\  z  =  ( vol `  c ) )  <->  ( a  C_  U.
ran  ( (,)  o.  f )  /\  z  =  ( vol `  a
) ) ) )
268267cbvrexv 3082 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2588 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7898 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2511 . . . . . . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  a  ->  (
( c  C_  ( U. ran  ( (,)  o.  f )  \  A
)  /\  z  =  ( vol `  c ) )  <->  ( a  C_  ( U. ran  ( (,) 
o.  f )  \  A )  /\  z  =  ( vol `  a
) ) ) )
274273cbvrexv 3082 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2588 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7898 . . . . . . . . . . . . . . . . . . . . . . . . . 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 751 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  z  ->  (
y  =  ( vol `  b )  <->  z  =  ( vol `  b ) ) )
279278anbi2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  z  ->  (
( b  C_  A  /\  y  =  ( vol `  b ) )  <-> 
( b  C_  A  /\  z  =  ( vol `  b ) ) ) )
280279rexbidv 2965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( b  =  c  ->  ( vol `  b )  =  ( vol `  c
) )
283282eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( b  =  c  ->  (
z  =  ( vol `  b )  <->  z  =  ( vol `  c ) ) )
284281, 283anbi12d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( b  =  c  ->  (
( b  C_  A  /\  z  =  ( vol `  b ) )  <-> 
( c  C_  A  /\  z  =  ( vol `  c ) ) ) )
285284cbvrexv 3082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 30293 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ,  <  )