Metamath Proof Explorer

Theorem ismblfin

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)

Ref Expression
Assertion 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 , < ) ) )

Proof

Step Hyp Ref Expression
1 mblfinlem4 
 |-  ( ( ( 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 
 |-  ( w e. ~P RR -> w C_ RR )
3 elmapi 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
4 inss1 
 |-  ( w i^i A ) C_ w
5 ovolsscl 
 |-  ( ( ( w i^i A ) C_ w /\ w C_ RR /\ ( vol* ` w ) e. RR ) -> ( vol* ` ( w i^i A ) ) e. RR )
6 4 5 mp3an1 
 |-  ( ( w C_ RR /\ ( vol* ` w ) e. RR ) -> ( vol* ` ( w i^i A ) ) e. RR )
7 difss 
 |-  ( w \ A ) C_ w
8 ovolsscl 
 |-  ( ( ( w \ A ) C_ w /\ w C_ RR /\ ( vol* ` w ) e. RR ) -> ( vol* ` ( w \ A ) ) e. RR )
9 7 8 mp3an1 
 |-  ( ( w C_ RR /\ ( vol* ` w ) e. RR ) -> ( vol* ` ( w \ A ) ) e. RR )
10 6 9 readdcld 
 |-  ( ( w C_ RR /\ ( vol* ` w ) e. RR ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) e. RR )
11 10 rexrd 
 |-  ( ( w C_ RR /\ ( vol* ` w ) e. RR ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) e. RR* )
12 11 ad3antlr 
 |-  ( ( ( ( ( ( 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 
 |-  ran ( (,) o. f ) C_ ran (,)
14 13 unissi 
 |-  U. ran ( (,) o. f ) C_ U. ran (,)
15 unirnioo 
 |-  RR = U. ran (,)
16 14 15 sseqtrri 
 |-  U. ran ( (,) o. f ) C_ RR
17 ovolcl 
 |-  ( U. ran ( (,) o. f ) C_ RR -> ( vol* ` U. ran ( (,) o. f ) ) e. RR* )
18 16 17 mp1i 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( abs o. - ) o. f ) = ( ( abs o. - ) o. f )
20 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
21 19 20 ovolsf 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) )
22 frn 
 |-  ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ ( 0 [,) +oo ) )
23 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
24 22 23 sstrdi 
 |-  ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* )
25 supxrcl 
 |-  ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* )
26 21 24 25 3syl 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* )
27 26 ad2antlr 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) e. RR* -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ +oo )
29 11 28 syl 
 |-  ( ( w C_ RR /\ ( vol* ` w ) e. RR ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ +oo )
30 29 ad2antrr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 )
32 30 31 breqtrrd 
 |-  ( ( ( ( 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 ) ) )
33 32 adantlll 
 |-  ( ( ( ( ( ( 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 ) ) )
34 16 17 ax-mp 
 |-  ( vol* ` U. ran ( (,) o. f ) ) e. RR*
35 nltpnft 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* -> ( ( vol* ` U. ran ( (,) o. f ) ) = +oo <-> -. ( vol* ` U. ran ( (,) o. f ) ) < +oo ) )
36 34 35 ax-mp 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) = +oo <-> -. ( vol* ` U. ran ( (,) o. f ) ) < +oo )
37 36 necon2abii 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) < +oo <-> ( vol* ` U. ran ( (,) o. f ) ) =/= +oo )
38 ovolge0 
 |-  ( U. ran ( (,) o. f ) C_ RR -> 0 <_ ( vol* ` U. ran ( (,) o. f ) ) )
39 16 38 ax-mp 
 |-  0 <_ ( vol* ` U. ran ( (,) o. f ) )
40 0re 
 |-  0 e. RR
41 xrre3 
 |-  ( ( ( ( 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 )
42 34 40 41 mpanl12 
 |-  ( ( 0 <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) < +oo ) -> ( vol* ` U. ran ( (,) o. f ) ) e. RR )
43 39 42 mpan 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) < +oo -> ( vol* ` U. ran ( (,) o. f ) ) e. RR )
44 37 43 sylbir 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) =/= +oo -> ( vol* ` U. ran ( (,) o. f ) ) e. RR )
45 10 ad3antlr 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) -> z = ( vol ` a ) )
47 eleq1w 
 |-  ( b = a -> ( b e. dom vol <-> a e. dom vol ) )
48 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
49 48 cldss 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> b C_ RR )
50 dfss4 
 |-  ( b C_ RR <-> ( RR \ ( RR \ b ) ) = b )
51 49 50 sylib 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ ( RR \ b ) ) = b )
52 rembl 
 |-  RR e. dom vol
53 48 cldopn 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ b ) e. ( topGen ` ran (,) ) )
54 opnmbl 
 |-  ( ( RR \ b ) e. ( topGen ` ran (,) ) -> ( RR \ b ) e. dom vol )
55 53 54 syl 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ b ) e. dom vol )
56 difmbl 
 |-  ( ( RR e. dom vol /\ ( RR \ b ) e. dom vol ) -> ( RR \ ( RR \ b ) ) e. dom vol )
57 52 55 56 sylancr 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ ( RR \ b ) ) e. dom vol )
58 51 57 eqeltrrd 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> b e. dom vol )
59 47 58 vtoclga 
 |-  ( a e. ( Clsd ` ( topGen ` ran (,) ) ) -> a e. dom vol )
60 mblvol 
 |-  ( a e. dom vol -> ( vol ` a ) = ( vol* ` a ) )
61 59 60 syl 
 |-  ( a e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` a ) = ( vol* ` a ) )
62 46 61 sylan9eqr 
 |-  ( ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) ) -> z = ( vol* ` a ) )
63 62 adantl 
 |-  ( ( ( 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 
 |-  ( U. ran ( (,) o. f ) i^i A ) C_ U. ran ( (,) o. f )
65 sstr 
 |-  ( ( 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 ) )
66 64 65 mpan2 
 |-  ( a C_ ( U. ran ( (,) o. f ) i^i A ) -> a C_ U. ran ( (,) o. f ) )
67 66 ad2antrl 
 |-  ( ( 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 
 |-  ( ( a C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` a ) e. RR )
69 16 68 mp3an2 
 |-  ( ( a C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` a ) e. RR )
70 69 ancoms 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ a C_ U. ran ( (,) o. f ) ) -> ( vol* ` a ) e. RR )
71 67 70 sylan2 
 |-  ( ( ( 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 )
72 63 71 eqeltrd 
 |-  ( ( ( 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 )
73 72 rexlimdvaa 
 |-  ( ( 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 ) )
74 73 abssdv 
 |-  ( ( 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 
 |-  ( z = y -> ( z = ( vol ` a ) <-> y = ( vol ` a ) ) )
76 75 anbi2d 
 |-  ( 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 ) ) ) )
77 76 rexbidv 
 |-  ( 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 ) ) ) )
78 77 ralab 
 |-  ( 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 
 |-  ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ y = ( vol ` a ) ) -> y = ( vol ` a ) )
80 79 61 sylan9eqr 
 |-  ( ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ y = ( vol ` a ) ) ) -> y = ( vol* ` a ) )
81 ovolss 
 |-  ( ( a C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR ) -> ( vol* ` a ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
82 66 16 81 sylancl 
 |-  ( a C_ ( U. ran ( (,) o. f ) i^i A ) -> ( vol* ` a ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
83 82 ad2antrl 
 |-  ( ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ y = ( vol ` a ) ) ) -> ( vol* ` a ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
84 80 83 eqbrtrd 
 |-  ( ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ y = ( vol ` a ) ) ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) )
85 84 rexlimiva 
 |-  ( E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ y = ( vol ` a ) ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) )
86 78 85 mpgbir 
 |-  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 brralrspcev 
 |-  ( ( ( 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 )
88 86 87 mpan2 
 |-  ( ( 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 )
89 retop 
 |-  ( topGen ` ran (,) ) e. Top
90 0cld 
 |-  ( ( topGen ` ran (,) ) e. Top -> (/) e. ( Clsd ` ( topGen ` ran (,) ) ) )
91 89 90 ax-mp 
 |-  (/) e. ( Clsd ` ( topGen ` ran (,) ) )
92 0ss 
 |-  (/) C_ ( U. ran ( (,) o. f ) i^i A )
93 0mbl 
 |-  (/) e. dom vol
94 mblvol 
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
95 93 94 ax-mp 
 |-  ( vol ` (/) ) = ( vol* ` (/) )
96 ovol0 
 |-  ( vol* ` (/) ) = 0
97 95 96 eqtr2i 
 |-  0 = ( vol ` (/) )
98 92 97 pm3.2i 
 |-  ( (/) C_ ( U. ran ( (,) o. f ) i^i A ) /\ 0 = ( vol ` (/) ) )
99 sseq1 
 |-  ( a = (/) -> ( a C_ ( U. ran ( (,) o. f ) i^i A ) <-> (/) C_ ( U. ran ( (,) o. f ) i^i A ) ) )
100 fveq2 
 |-  ( a = (/) -> ( vol ` a ) = ( vol ` (/) ) )
101 100 eqeq2d 
 |-  ( a = (/) -> ( 0 = ( vol ` a ) <-> 0 = ( vol ` (/) ) ) )
102 99 101 anbi12d 
 |-  ( a = (/) -> ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ 0 = ( vol ` a ) ) <-> ( (/) C_ ( U. ran ( (,) o. f ) i^i A ) /\ 0 = ( vol ` (/) ) ) ) )
103 102 rspcev 
 |-  ( ( (/) 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 ) ) )
104 91 98 103 mp2an 
 |-  E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ 0 = ( vol ` a ) )
105 c0ex 
 |-  0 e. _V
106 eqeq1 
 |-  ( z = 0 -> ( z = ( vol ` a ) <-> 0 = ( vol ` a ) ) )
107 106 anbi2d 
 |-  ( 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 ) ) ) )
108 107 rexbidv 
 |-  ( 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 ) ) ) )
109 105 108 elab 
 |-  ( 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 ) ) )
110 104 109 mpbir 
 |-  0 e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) }
111 110 ne0ii 
 |-  { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } =/= (/)
112 suprcl 
 |-  ( ( { 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 )
113 111 112 mp3an2 
 |-  ( ( { 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 )
114 74 88 113 syl2anc 
 |-  ( ( 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 )
115 simpr 
 |-  ( ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) -> z = ( vol ` c ) )
116 eleq1w 
 |-  ( b = c -> ( b e. dom vol <-> c e. dom vol ) )
117 116 58 vtoclga 
 |-  ( c e. ( Clsd ` ( topGen ` ran (,) ) ) -> c e. dom vol )
118 mblvol 
 |-  ( c e. dom vol -> ( vol ` c ) = ( vol* ` c ) )
119 117 118 syl 
 |-  ( c e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` c ) = ( vol* ` c ) )
120 115 119 sylan9eqr 
 |-  ( ( c e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) ) -> z = ( vol* ` c ) )
121 120 adantl 
 |-  ( ( ( 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 ) )
122 difss2 
 |-  ( c C_ ( U. ran ( (,) o. f ) \ A ) -> c C_ U. ran ( (,) o. f ) )
123 122 ad2antrl 
 |-  ( ( c e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) ) -> c C_ U. ran ( (,) o. f ) )
124 ovolsscl 
 |-  ( ( c C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` c ) e. RR )
125 16 124 mp3an2 
 |-  ( ( c C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` c ) e. RR )
126 125 ancoms 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ c C_ U. ran ( (,) o. f ) ) -> ( vol* ` c ) e. RR )
127 123 126 sylan2 
 |-  ( ( ( 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 )
128 121 127 eqeltrd 
 |-  ( ( ( 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 )
129 128 rexlimdvaa 
 |-  ( ( 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 ) )
130 129 abssdv 
 |-  ( ( 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 )
131 eqeq1 
 |-  ( z = y -> ( z = ( vol ` c ) <-> y = ( vol ` c ) ) )
132 131 anbi2d 
 |-  ( z = y -> ( ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) <-> ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ y = ( vol ` c ) ) ) )
133 132 rexbidv 
 |-  ( 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 ) ) ) )
134 133 ralab 
 |-  ( 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 ) ) ) )
135 simpr 
 |-  ( ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ y = ( vol ` c ) ) -> y = ( vol ` c ) )
136 135 119 sylan9eqr 
 |-  ( ( c e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ y = ( vol ` c ) ) ) -> y = ( vol* ` c ) )
137 ovolss 
 |-  ( ( c C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR ) -> ( vol* ` c ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
138 122 16 137 sylancl 
 |-  ( c C_ ( U. ran ( (,) o. f ) \ A ) -> ( vol* ` c ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
139 138 ad2antrl 
 |-  ( ( c e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ y = ( vol ` c ) ) ) -> ( vol* ` c ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
140 136 139 eqbrtrd 
 |-  ( ( c e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ y = ( vol ` c ) ) ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) )
141 140 rexlimiva 
 |-  ( E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ y = ( vol ` c ) ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) )
142 134 141 mpgbir 
 |-  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 ) )
143 brralrspcev 
 |-  ( ( ( 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 )
144 142 143 mpan2 
 |-  ( ( 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 )
145 0ss 
 |-  (/) C_ ( U. ran ( (,) o. f ) \ A )
146 145 97 pm3.2i 
 |-  ( (/) C_ ( U. ran ( (,) o. f ) \ A ) /\ 0 = ( vol ` (/) ) )
147 sseq1 
 |-  ( c = (/) -> ( c C_ ( U. ran ( (,) o. f ) \ A ) <-> (/) C_ ( U. ran ( (,) o. f ) \ A ) ) )
148 fveq2 
 |-  ( c = (/) -> ( vol ` c ) = ( vol ` (/) ) )
149 148 eqeq2d 
 |-  ( c = (/) -> ( 0 = ( vol ` c ) <-> 0 = ( vol ` (/) ) ) )
150 147 149 anbi12d 
 |-  ( c = (/) -> ( ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ 0 = ( vol ` c ) ) <-> ( (/) C_ ( U. ran ( (,) o. f ) \ A ) /\ 0 = ( vol ` (/) ) ) ) )
151 150 rspcev 
 |-  ( ( (/) 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 ) ) )
152 91 146 151 mp2an 
 |-  E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ 0 = ( vol ` c ) )
153 eqeq1 
 |-  ( z = 0 -> ( z = ( vol ` c ) <-> 0 = ( vol ` c ) ) )
154 153 anbi2d 
 |-  ( z = 0 -> ( ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) <-> ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ 0 = ( vol ` c ) ) ) )
155 154 rexbidv 
 |-  ( 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 ) ) ) )
156 105 155 elab 
 |-  ( 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 ) ) )
157 152 156 mpbir 
 |-  0 e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) }
158 157 ne0ii 
 |-  { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } =/= (/)
159 suprcl 
 |-  ( ( { 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 )
160 158 159 mp3an2 
 |-  ( ( { 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 )
161 130 144 160 syl2anc 
 |-  ( ( 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 )
162 114 161 readdcld 
 |-  ( ( 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 )
163 162 adantl 
 |-  ( ( ( ( ( ( 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 )
164 simpr 
 |-  ( ( ( ( ( ( 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 )
165 6 ad2antrr 
 |-  ( ( ( ( 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 )
166 9 ad2antrr 
 |-  ( ( ( ( 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 )
167 ovolsscl 
 |-  ( ( ( 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 )
168 64 16 167 mp3an12 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( vol* ` ( U. ran ( (,) o. f ) i^i A ) ) e. RR )
169 168 adantl 
 |-  ( ( ( ( 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 )
170 difss 
 |-  ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. f )
171 ovolsscl 
 |-  ( ( ( 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 )
172 170 16 171 mp3an12 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR )
173 172 adantl 
 |-  ( ( ( ( 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 )
174 ssrin 
 |-  ( w C_ U. ran ( (,) o. f ) -> ( w i^i A ) C_ ( U. ran ( (,) o. f ) i^i A ) )
175 64 16 sstri 
 |-  ( U. ran ( (,) o. f ) i^i A ) C_ RR
176 ovolss 
 |-  ( ( ( 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 ) ) )
177 174 175 176 sylancl 
 |-  ( w C_ U. ran ( (,) o. f ) -> ( vol* ` ( w i^i A ) ) <_ ( vol* ` ( U. ran ( (,) o. f ) i^i A ) ) )
178 177 ad2antlr 
 |-  ( ( ( ( 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 ) ) )
179 ssdif 
 |-  ( w C_ U. ran ( (,) o. f ) -> ( w \ A ) C_ ( U. ran ( (,) o. f ) \ A ) )
180 170 16 sstri 
 |-  ( U. ran ( (,) o. f ) \ A ) C_ RR
181 ovolss 
 |-  ( ( ( w \ A ) C_ ( U. ran ( (,) o. f ) \ A ) /\ ( U. ran ( (,) o. f ) \ A ) C_ RR ) -> ( vol* ` ( w \ A ) ) <_ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) )
182 179 180 181 sylancl 
 |-  ( w C_ U. ran ( (,) o. f ) -> ( vol* ` ( w \ A ) ) <_ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) )
183 182 ad2antlr 
 |-  ( ( ( ( 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 ) ) )
184 165 166 169 173 178 183 le2addd 
 |-  ( ( ( ( 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 ) ) ) )
185 dfin4 
 |-  ( U. ran ( (,) o. f ) i^i A ) = ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) )
186 185 fveq2i 
 |-  ( vol* ` ( U. ran ( (,) o. f ) i^i A ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) )
187 186 oveq1i 
 |-  ( ( 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 ) ) )
188 184 187 breqtrdi 
 |-  ( ( ( ( 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 ) ) ) )
189 188 adantlll 
 |-  ( ( ( ( ( ( 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 ) ) ) )
190 simpll 
 |-  ( ( ( ( ( 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 , < ) ) )
191 185 sseq2i 
 |-  ( a C_ ( U. ran ( (,) o. f ) i^i A ) <-> a C_ ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) )
192 191 anbi1i 
 |-  ( ( 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 ) ) )
193 192 rexbii 
 |-  ( 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 ) ) )
194 193 abbii 
 |-  { 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 ) ) }
195 194 supeq1i 
 |-  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 , < )
196 16 jctl 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) )
197 196 adantl 
 |-  ( ( ( ( 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 ) )
198 172 180 jctil 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( ( U. ran ( (,) o. f ) \ A ) C_ RR /\ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR ) )
199 198 adantl 
 |-  ( ( ( ( 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 ) )
200 ltso 
 |-  < Or RR
201 200 a1i 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> < Or RR )
202 id 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( vol* ` U. ran ( (,) o. f ) ) e. RR )
203 vex 
 |-  x e. _V
204 eqeq1 
 |-  ( z = x -> ( z = ( vol ` c ) <-> x = ( vol ` c ) ) )
205 204 anbi2d 
 |-  ( z = x -> ( ( c C_ U. ran ( (,) o. f ) /\ z = ( vol ` c ) ) <-> ( c C_ U. ran ( (,) o. f ) /\ x = ( vol ` c ) ) ) )
206 205 rexbidv 
 |-  ( 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 ) ) ) )
207 203 206 elab 
 |-  ( 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 ) ) )
208 16 137 mpan2 
 |-  ( c C_ U. ran ( (,) o. f ) -> ( vol* ` c ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
209 208 ad2antrl 
 |-  ( ( c e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( c C_ U. ran ( (,) o. f ) /\ x = ( vol ` c ) ) ) -> ( vol* ` c ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
210 48 cldss 
 |-  ( c e. ( Clsd ` ( topGen ` ran (,) ) ) -> c C_ RR )
211 ovolcl 
 |-  ( c C_ RR -> ( vol* ` c ) e. RR* )
212 210 211 syl 
 |-  ( c e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol* ` c ) e. RR* )
213 xrlenlt 
 |-  ( ( ( 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 ) ) )
214 212 34 213 sylancl 
 |-  ( c e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( ( vol* ` c ) <_ ( vol* ` U. ran ( (,) o. f ) ) <-> -. ( vol* ` U. ran ( (,) o. f ) ) < ( vol* ` c ) ) )
215 214 adantr 
 |-  ( ( 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 ) ) )
216 id 
 |-  ( x = ( vol ` c ) -> x = ( vol ` c ) )
217 216 119 sylan9eqr 
 |-  ( ( c e. ( Clsd ` ( topGen ` ran (,) ) ) /\ x = ( vol ` c ) ) -> x = ( vol* ` c ) )
218 breq2 
 |-  ( x = ( vol* ` c ) -> ( ( vol* ` U. ran ( (,) o. f ) ) < x <-> ( vol* ` U. ran ( (,) o. f ) ) < ( vol* ` c ) ) )
219 218 notbid 
 |-  ( x = ( vol* ` c ) -> ( -. ( vol* ` U. ran ( (,) o. f ) ) < x <-> -. ( vol* ` U. ran ( (,) o. f ) ) < ( vol* ` c ) ) )
220 217 219 syl 
 |-  ( ( c e. ( Clsd ` ( topGen ` ran (,) ) ) /\ x = ( vol ` c ) ) -> ( -. ( vol* ` U. ran ( (,) o. f ) ) < x <-> -. ( vol* ` U. ran ( (,) o. f ) ) < ( vol* ` c ) ) )
221 220 adantrl 
 |-  ( ( 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 ) ) )
222 215 221 bitr4d 
 |-  ( ( 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 ) )
223 209 222 mpbid 
 |-  ( ( c e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( c C_ U. ran ( (,) o. f ) /\ x = ( vol ` c ) ) ) -> -. ( vol* ` U. ran ( (,) o. f ) ) < x )
224 223 rexlimiva 
 |-  ( E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ U. ran ( (,) o. f ) /\ x = ( vol ` c ) ) -> -. ( vol* ` U. ran ( (,) o. f ) ) < x )
225 207 224 sylbi 
 |-  ( x e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ U. ran ( (,) o. f ) /\ z = ( vol ` c ) ) } -> -. ( vol* ` U. ran ( (,) o. f ) ) < x )
226 225 adantl 
 |-  ( ( ( 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 )
227 retopbas 
 |-  ran (,) e. TopBases
228 bastg 
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
229 227 228 ax-mp 
 |-  ran (,) C_ ( topGen ` ran (,) )
230 13 229 sstri 
 |-  ran ( (,) o. f ) C_ ( topGen ` ran (,) )
231 uniopn 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ran ( (,) o. f ) C_ ( topGen ` ran (,) ) ) -> U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) )
232 89 230 231 mp2an 
 |-  U. ran ( (,) o. f ) e. ( topGen ` ran (,) )
233 mblfinlem2 
 |-  ( ( 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 ) ) )
234 232 233 mp3an1 
 |-  ( ( x e. RR /\ x < ( vol* ` U. ran ( (,) o. f ) ) ) -> E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ U. ran ( (,) o. f ) /\ x < ( vol* ` c ) ) )
235 119 eqcomd 
 |-  ( c e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol* ` c ) = ( vol ` c ) )
236 235 anim1i 
 |-  ( ( c e. ( Clsd ` ( topGen ` ran (,) ) ) /\ x < ( vol* ` c ) ) -> ( ( vol* ` c ) = ( vol ` c ) /\ x < ( vol* ` c ) ) )
237 236 ex 
 |-  ( c e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( x < ( vol* ` c ) -> ( ( vol* ` c ) = ( vol ` c ) /\ x < ( vol* ` c ) ) ) )
238 237 anim2d 
 |-  ( 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 ) ) ) ) )
239 fvex 
 |-  ( vol* ` c ) e. _V
240 eqeq1 
 |-  ( y = ( vol* ` c ) -> ( y = ( vol ` c ) <-> ( vol* ` c ) = ( vol ` c ) ) )
241 240 anbi2d 
 |-  ( y = ( vol* ` c ) -> ( ( c C_ U. ran ( (,) o. f ) /\ y = ( vol ` c ) ) <-> ( c C_ U. ran ( (,) o. f ) /\ ( vol* ` c ) = ( vol ` c ) ) ) )
242 breq2 
 |-  ( y = ( vol* ` c ) -> ( x < y <-> x < ( vol* ` c ) ) )
243 241 242 anbi12d 
 |-  ( 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 ) ) ) )
244 239 243 spcev 
 |-  ( ( ( 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 ) )
245 244 anasss 
 |-  ( ( 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 ) )
246 238 245 syl6 
 |-  ( 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 ) ) )
247 246 reximia 
 |-  ( 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 ) )
248 234 247 syl 
 |-  ( ( 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 ) )
249 r19.41v 
 |-  ( 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 ) )
250 249 exbii 
 |-  ( 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 ) )
251 rexcom4 
 |-  ( 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 ) )
252 131 anbi2d 
 |-  ( z = y -> ( ( c C_ U. ran ( (,) o. f ) /\ z = ( vol ` c ) ) <-> ( c C_ U. ran ( (,) o. f ) /\ y = ( vol ` c ) ) ) )
253 252 rexbidv 
 |-  ( 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 ) ) ) )
254 253 rexab 
 |-  ( 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 ) )
255 250 251 254 3bitr4i 
 |-  ( 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 )
256 248 255 sylib 
 |-  ( ( 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 )
257 256 adantl 
 |-  ( ( ( 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 )
258 201 202 226 257 eqsupd 
 |-  ( ( 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 ) ) )
259 258 eqcomd 
 |-  ( ( 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 , < ) )
260 259 adantl 
 |-  ( ( ( ( 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 , < ) )
261 sseq1 
 |-  ( c = a -> ( c C_ U. ran ( (,) o. f ) <-> a C_ U. ran ( (,) o. f ) ) )
262 fveq2 
 |-  ( c = a -> ( vol ` c ) = ( vol ` a ) )
263 262 eqeq2d 
 |-  ( c = a -> ( z = ( vol ` c ) <-> z = ( vol ` a ) ) )
264 261 263 anbi12d 
 |-  ( c = a -> ( ( c C_ U. ran ( (,) o. f ) /\ z = ( vol ` c ) ) <-> ( a C_ U. ran ( (,) o. f ) /\ z = ( vol ` a ) ) ) )
265 264 cbvrexvw 
 |-  ( 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 ) ) )
266 265 abbii 
 |-  { 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 ) ) }
267 266 supeq1i 
 |-  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 , < )
268 260 267 eqtrdi 
 |-  ( ( ( ( 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 , < ) )
269 simpll 
 |-  ( ( ( ( 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 ) )
270 eqeq1 
 |-  ( y = z -> ( y = ( vol ` b ) <-> z = ( vol ` b ) ) )
271 270 anbi2d 
 |-  ( y = z -> ( ( b C_ A /\ y = ( vol ` b ) ) <-> ( b C_ A /\ z = ( vol ` b ) ) ) )
272 271 rexbidv 
 |-  ( 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 ) ) ) )
273 sseq1 
 |-  ( b = c -> ( b C_ A <-> c C_ A ) )
274 fveq2 
 |-  ( b = c -> ( vol ` b ) = ( vol ` c ) )
275 274 eqeq2d 
 |-  ( b = c -> ( z = ( vol ` b ) <-> z = ( vol ` c ) ) )
276 273 275 anbi12d 
 |-  ( b = c -> ( ( b C_ A /\ z = ( vol ` b ) ) <-> ( c C_ A /\ z = ( vol ` c ) ) ) )
277 276 cbvrexvw 
 |-  ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ z = ( vol ` b ) ) <-> E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ A /\ z = ( vol ` c ) ) )
278 272 277 bitrdi 
 |-  ( 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 ) ) ) )
279 278 cbvabv 
 |-  { 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 ) ) }
280 279 supeq1i 
 |-  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 , < )
281 280 eqeq2i 
 |-  ( ( 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 , < ) )
282 281 biimpi 
 |-  ( ( 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 , < ) )
283 282 ad2antlr 
 |-  ( ( ( ( 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 , < ) )
284 mblfinlem3 
 |-  ( ( ( 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 ) ) )
285 197 269 260 283 284 syl112anc 
 |-  ( ( ( ( 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 ) -> 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 ) ) )
286 sseq1 
 |-  ( c = a -> ( c C_ ( U. ran ( (,) o. f ) \ A ) <-> a C_ ( U. ran ( (,) o. f ) \ A ) ) )
287 286 263 anbi12d 
 |-  ( c = a -> ( ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) <-> ( a C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` a ) ) ) )
288 287 cbvrexvw 
 |-  ( 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 ) ) )
289 288 abbii 
 |-  { 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 ) ) }
290 289 supeq1i 
 |-  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 , < )
291 285 290 eqtr3di 
 |-  ( ( ( ( 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 ) \ A ) ) = sup ( { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` a ) ) } , RR , < ) )
292 mblfinlem3 
 |-  ( ( ( U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ RR /\ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) 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 , < ) /\ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) = sup ( { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) \ 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 , < ) = ( vol* ` ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) ) )
293 197 199 268 291 292 syl112anc 
 |-  ( ( ( ( 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 ) -> sup ( { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) /\ z = ( vol ` a ) ) } , RR , < ) = ( vol* ` ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) ) )
294 195 293 eqtrid 
 |-  ( ( ( ( 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 ) -> sup ( { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } , RR , < ) = ( vol* ` ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) ) )
295 294 285 oveq12d 
 |-  ( ( ( ( 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 ) -> ( 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 , < ) ) = ( ( vol* ` ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) ) )
296 190 295 sylan 
 |-  ( ( ( ( ( ( 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 , < ) ) = ( ( vol* ` ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) ) )
297 189 296 breqtrrd 
 |-  ( ( ( ( ( ( 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 ) ) ) <_ ( 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 , < ) ) )
298 ne0i 
 |-  ( 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 ) ) } =/= (/) )
299 110 298 mp1i 
 |-  ( ( 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 ) ) } =/= (/) )
300 ne0i 
 |-  ( 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 ) ) } =/= (/) )
301 157 300 mp1i 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } =/= (/) )
302 eqid 
 |-  { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } = { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) }
303 74 299 88 130 301 144 302 supadd 
 |-  ( ( 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 , < ) ) = sup ( { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } , RR , < ) )
304 reeanv 
 |-  ( E. a e. ( Clsd ` ( topGen ` ran (,) ) ) E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ u = ( vol ` a ) ) /\ ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ v = ( vol ` c ) ) ) <-> ( E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ u = ( vol ` a ) ) /\ E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ v = ( vol ` c ) ) ) )
305 vex 
 |-  u e. _V
306 eqeq1 
 |-  ( z = u -> ( z = ( vol ` a ) <-> u = ( vol ` a ) ) )
307 306 anbi2d 
 |-  ( z = u -> ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) <-> ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ u = ( vol ` a ) ) ) )
308 307 rexbidv 
 |-  ( z = u -> ( 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 ) /\ u = ( vol ` a ) ) ) )
309 305 308 elab 
 |-  ( u 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 ) /\ u = ( vol ` a ) ) )
310 vex 
 |-  v e. _V
311 eqeq1 
 |-  ( z = v -> ( z = ( vol ` c ) <-> v = ( vol ` c ) ) )
312 311 anbi2d 
 |-  ( z = v -> ( ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) <-> ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ v = ( vol ` c ) ) ) )
313 312 rexbidv 
 |-  ( z = v -> ( 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 ) /\ v = ( vol ` c ) ) ) )
314 310 313 elab 
 |-  ( v 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 ) /\ v = ( vol ` c ) ) )
315 309 314 anbi12i 
 |-  ( ( u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } /\ v e. { z | 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 ) i^i A ) /\ u = ( vol ` a ) ) /\ E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ v = ( vol ` c ) ) ) )
316 304 315 bitr4i 
 |-  ( E. a e. ( Clsd ` ( topGen ` ran (,) ) ) E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ u = ( vol ` a ) ) /\ ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ v = ( vol ` c ) ) ) <-> ( u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } /\ v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } ) )
317 an4 
 |-  ( ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) /\ ( u = ( vol ` a ) /\ v = ( vol ` c ) ) ) <-> ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ u = ( vol ` a ) ) /\ ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ v = ( vol ` c ) ) ) )
318 oveq12 
 |-  ( ( u = ( vol ` a ) /\ v = ( vol ` c ) ) -> ( u + v ) = ( ( vol ` a ) + ( vol ` c ) ) )
319 59 adantr 
 |-  ( ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> a e. dom vol )
320 319 ad2antlr 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> a e. dom vol )
321 117 adantl 
 |-  ( ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> c e. dom vol )
322 321 ad2antlr 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> c e. dom vol )
323 ss2in 
 |-  ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) -> ( a i^i c ) C_ ( ( U. ran ( (,) o. f ) i^i A ) i^i ( U. ran ( (,) o. f ) \ A ) ) )
324 185 ineq1i 
 |-  ( ( U. ran ( (,) o. f ) i^i A ) i^i ( U. ran ( (,) o. f ) \ A ) ) = ( ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) i^i ( U. ran ( (,) o. f ) \ A ) )
325 incom 
 |-  ( ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) i^i ( U. ran ( (,) o. f ) \ A ) ) = ( ( U. ran ( (,) o. f ) \ A ) i^i ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) )
326 disjdif 
 |-  ( ( U. ran ( (,) o. f ) \ A ) i^i ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) ) = (/)
327 324 325 326 3eqtri 
 |-  ( ( U. ran ( (,) o. f ) i^i A ) i^i ( U. ran ( (,) o. f ) \ A ) ) = (/)
328 323 327 sseqtrdi 
 |-  ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) -> ( a i^i c ) C_ (/) )
329 ss0 
 |-  ( ( a i^i c ) C_ (/) -> ( a i^i c ) = (/) )
330 328 329 syl 
 |-  ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) -> ( a i^i c ) = (/) )
331 330 adantl 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> ( a i^i c ) = (/) )
332 61 adantr 
 |-  ( ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( vol ` a ) = ( vol* ` a ) )
333 332 ad2antlr 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> ( vol ` a ) = ( vol* ` a ) )
334 66 16 jctir 
 |-  ( a C_ ( U. ran ( (,) o. f ) i^i A ) -> ( a C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR ) )
335 68 3expa 
 |-  ( ( ( a C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR ) /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` a ) e. RR )
336 334 335 sylan 
 |-  ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` a ) e. RR )
337 336 ancoms 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ a C_ ( U. ran ( (,) o. f ) i^i A ) ) -> ( vol* ` a ) e. RR )
338 337 ad2ant2r 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> ( vol* ` a ) e. RR )
339 333 338 eqeltrd 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> ( vol ` a ) e. RR )
340 119 adantl 
 |-  ( ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( vol ` c ) = ( vol* ` c ) )
341 340 ad2antlr 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> ( vol ` c ) = ( vol* ` c ) )
342 122 16 jctir 
 |-  ( c C_ ( U. ran ( (,) o. f ) \ A ) -> ( c C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR ) )
343 124 3expa 
 |-  ( ( ( c C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR ) /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` c ) e. RR )
344 342 343 sylan 
 |-  ( ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` c ) e. RR )
345 344 ancoms 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) -> ( vol* ` c ) e. RR )
346 345 ad2ant2rl 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> ( vol* ` c ) e. RR )
347 341 346 eqeltrd 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> ( vol ` c ) e. RR )
348 volun 
 |-  ( ( ( a e. dom vol /\ c e. dom vol /\ ( a i^i c ) = (/) ) /\ ( ( vol ` a ) e. RR /\ ( vol ` c ) e. RR ) ) -> ( vol ` ( a u. c ) ) = ( ( vol ` a ) + ( vol ` c ) ) )
349 320 322 331 339 347 348 syl32anc 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> ( vol ` ( a u. c ) ) = ( ( vol ` a ) + ( vol ` c ) ) )
350 unmbl 
 |-  ( ( a e. dom vol /\ c e. dom vol ) -> ( a u. c ) e. dom vol )
351 59 117 350 syl2an 
 |-  ( ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( a u. c ) e. dom vol )
352 mblvol 
 |-  ( ( a u. c ) e. dom vol -> ( vol ` ( a u. c ) ) = ( vol* ` ( a u. c ) ) )
353 351 352 syl 
 |-  ( ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( vol ` ( a u. c ) ) = ( vol* ` ( a u. c ) ) )
354 353 ad2antlr 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> ( vol ` ( a u. c ) ) = ( vol* ` ( a u. c ) ) )
355 349 354 eqtr3d 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) -> ( ( vol ` a ) + ( vol ` c ) ) = ( vol* ` ( a u. c ) ) )
356 318 355 sylan9eqr 
 |-  ( ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) /\ ( u = ( vol ` a ) /\ v = ( vol ` c ) ) ) -> ( u + v ) = ( vol* ` ( a u. c ) ) )
357 eqtr 
 |-  ( ( y = ( u + v ) /\ ( u + v ) = ( vol* ` ( a u. c ) ) ) -> y = ( vol* ` ( a u. c ) ) )
358 357 ancoms 
 |-  ( ( ( u + v ) = ( vol* ` ( a u. c ) ) /\ y = ( u + v ) ) -> y = ( vol* ` ( a u. c ) ) )
359 356 358 sylan 
 |-  ( ( ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) /\ ( u = ( vol ` a ) /\ v = ( vol ` c ) ) ) /\ y = ( u + v ) ) -> y = ( vol* ` ( a u. c ) ) )
360 66 122 anim12i 
 |-  ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) -> ( a C_ U. ran ( (,) o. f ) /\ c C_ U. ran ( (,) o. f ) ) )
361 unss 
 |-  ( ( a C_ U. ran ( (,) o. f ) /\ c C_ U. ran ( (,) o. f ) ) <-> ( a u. c ) C_ U. ran ( (,) o. f ) )
362 360 361 sylib 
 |-  ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) -> ( a u. c ) C_ U. ran ( (,) o. f ) )
363 ovolss 
 |-  ( ( ( a u. c ) C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR ) -> ( vol* ` ( a u. c ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
364 362 16 363 sylancl 
 |-  ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) -> ( vol* ` ( a u. c ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
365 364 ad3antlr 
 |-  ( ( ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) /\ ( u = ( vol ` a ) /\ v = ( vol ` c ) ) ) /\ y = ( u + v ) ) -> ( vol* ` ( a u. c ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
366 359 365 eqbrtrd 
 |-  ( ( ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) /\ ( u = ( vol ` a ) /\ v = ( vol ` c ) ) ) /\ y = ( u + v ) ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) )
367 366 ex 
 |-  ( ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) ) /\ ( u = ( vol ` a ) /\ v = ( vol ` c ) ) ) -> ( y = ( u + v ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) ) )
368 367 expl 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ c C_ ( U. ran ( (,) o. f ) \ A ) ) /\ ( u = ( vol ` a ) /\ v = ( vol ` c ) ) ) -> ( y = ( u + v ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) ) ) )
369 317 368 biimtrrid 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( a e. ( Clsd ` ( topGen ` ran (,) ) ) /\ c e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ u = ( vol ` a ) ) /\ ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ v = ( vol ` c ) ) ) -> ( y = ( u + v ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) ) ) )
370 369 rexlimdvva 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( E. a e. ( Clsd ` ( topGen ` ran (,) ) ) E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ u = ( vol ` a ) ) /\ ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ v = ( vol ` c ) ) ) -> ( y = ( u + v ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) ) ) )
371 316 370 biimtrrid 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( ( u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } /\ v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } ) -> ( y = ( u + v ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) ) ) )
372 371 rexlimdvv 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } y = ( u + v ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) ) )
373 372 alrimiv 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> A. y ( E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } y = ( u + v ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) ) )
374 eqeq1 
 |-  ( t = y -> ( t = ( u + v ) <-> y = ( u + v ) ) )
375 374 2rexbidv 
 |-  ( t = y -> ( E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) <-> E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } y = ( u + v ) ) )
376 375 ralab 
 |-  ( A. y e. { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } y <_ ( vol* ` U. ran ( (,) o. f ) ) <-> A. y ( E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } y = ( u + v ) -> y <_ ( vol* ` U. ran ( (,) o. f ) ) ) )
377 373 376 sylibr 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> A. y e. { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } y <_ ( vol* ` U. ran ( (,) o. f ) ) )
378 simpr 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } /\ v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } ) ) /\ t = ( u + v ) ) -> t = ( u + v ) )
379 74 sselda 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } ) -> u e. RR )
380 130 sselda 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } ) -> v e. RR )
381 readdcl 
 |-  ( ( u e. RR /\ v e. RR ) -> ( u + v ) e. RR )
382 379 380 381 syl2an 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } ) ) -> ( u + v ) e. RR )
383 382 anandis 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } /\ v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } ) ) -> ( u + v ) e. RR )
384 383 adantr 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } /\ v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } ) ) /\ t = ( u + v ) ) -> ( u + v ) e. RR )
385 378 384 eqeltrd 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } /\ v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } ) ) /\ t = ( u + v ) ) -> t e. RR )
386 385 ex 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ ( u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } /\ v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } ) ) -> ( t = ( u + v ) -> t e. RR ) )
387 386 rexlimdvva 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) -> t e. RR ) )
388 387 abssdv 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } C_ RR )
389 00id 
 |-  ( 0 + 0 ) = 0
390 389 eqcomi 
 |-  0 = ( 0 + 0 )
391 rspceov 
 |-  ( ( 0 e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } /\ 0 e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } /\ 0 = ( 0 + 0 ) ) -> E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } 0 = ( u + v ) )
392 110 157 390 391 mp3an 
 |-  E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } 0 = ( u + v )
393 eqeq1 
 |-  ( t = 0 -> ( t = ( u + v ) <-> 0 = ( u + v ) ) )
394 393 2rexbidv 
 |-  ( t = 0 -> ( E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) <-> E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } 0 = ( u + v ) ) )
395 105 394 spcev 
 |-  ( E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } 0 = ( u + v ) -> E. t E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) )
396 392 395 ax-mp 
 |-  E. t E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v )
397 abn0 
 |-  ( { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } =/= (/) <-> E. t E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) )
398 396 397 mpbir 
 |-  { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } =/= (/)
399 398 a1i 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } =/= (/) )
400 brralrspcev 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR /\ A. y e. { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } y <_ ( vol* ` U. ran ( (,) o. f ) ) ) -> E. x e. RR A. y e. { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } y <_ x )
401 377 400 mpdan 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> E. x e. RR A. y e. { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } y <_ x )
402 388 399 401 3jca 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } C_ RR /\ { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } =/= (/) /\ E. x e. RR A. y e. { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } y <_ x ) )
403 suprleub 
 |-  ( ( ( { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } C_ RR /\ { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } =/= (/) /\ E. x e. RR A. y e. { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } y <_ x ) /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( sup ( { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } , RR , < ) <_ ( vol* ` U. ran ( (,) o. f ) ) <-> A. y e. { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } y <_ ( vol* ` U. ran ( (,) o. f ) ) ) )
404 402 403 mpancom 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( sup ( { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } , RR , < ) <_ ( vol* ` U. ran ( (,) o. f ) ) <-> A. y e. { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } y <_ ( vol* ` U. ran ( (,) o. f ) ) ) )
405 377 404 mpbird 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> sup ( { t | E. u e. { z | E. a e. ( Clsd ` ( topGen ` ran (,) ) ) ( a C_ ( U. ran ( (,) o. f ) i^i A ) /\ z = ( vol ` a ) ) } E. v e. { z | E. c e. ( Clsd ` ( topGen ` ran (,) ) ) ( c C_ ( U. ran ( (,) o. f ) \ A ) /\ z = ( vol ` c ) ) } t = ( u + v ) } , RR , < ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
406 303 405 eqbrtrd 
 |-  ( ( 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 , < ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
407 406 adantl 
 |-  ( ( ( ( ( ( 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 , < ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
408 45 163 164 297 407 letrd 
 |-  ( ( ( ( ( ( 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 ) ) )
409 44 408 sylan2 
 |-  ( ( ( ( ( ( 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 ) ) )
410 33 409 pm2.61dane 
 |-  ( ( ( ( ( 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* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
411 410 adantlr 
 |-  ( ( ( ( ( ( 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 ) ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
412 ssid 
 |-  U. ran ( (,) o. f ) C_ U. ran ( (,) o. f )
413 20 ovollb 
 |-  ( ( f : NN --> ( <_ i^i ( RR X. RR ) ) /\ U. ran ( (,) o. f ) C_ U. ran ( (,) o. f ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
414 412 413 mpan2 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
415 414 ad2antlr 
 |-  ( ( ( ( ( ( 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 ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
416 12 18 27 411 415 xrletrd 
 |-  ( ( ( ( ( ( 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 ) ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
417 416 adantr 
 |-  ( ( ( ( ( ( ( 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 ) ) /\ u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
418 simpr 
 |-  ( ( ( ( ( ( ( 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 ) ) /\ u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
419 417 418 breqtrrd 
 |-  ( ( ( ( ( ( ( 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 ) ) /\ u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ u )
420 419 expl 
 |-  ( ( ( ( ( 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 ) /\ u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ u ) )
421 3 420 sylan2 
 |-  ( ( ( ( ( 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 e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( ( w C_ U. ran ( (,) o. f ) /\ u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ u ) )
422 421 rexlimdva 
 |-  ( ( ( ( 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 ) ) -> ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ u ) )
423 422 ralrimivw 
 |-  ( ( ( ( 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 ) ) -> A. u e. RR* ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ u ) )
424 eqeq1 
 |-  ( v = u -> ( v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <-> u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
425 424 anbi2d 
 |-  ( v = u -> ( ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> ( w C_ U. ran ( (,) o. f ) /\ u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
426 425 rexbidv 
 |-  ( v = u -> ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
427 426 ralrab 
 |-  ( A. u e. { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ u <-> A. u e. RR* ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ u = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ u ) )
428 423 427 sylibr 
 |-  ( ( ( ( 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 ) ) -> A. u e. { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ u )
429 ssrab2 
 |-  { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } C_ RR*
430 11 adantl 
 |-  ( ( ( ( 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 ) ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) e. RR* )
431 infxrgelb 
 |-  ( ( { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } C_ RR* /\ ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) e. RR* ) -> ( ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ inf ( { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) <-> A. u e. { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ u ) )
432 429 430 431 sylancr 
 |-  ( ( ( ( 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 ) ) -> ( ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ inf ( { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) <-> A. u e. { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ u ) )
433 428 432 mpbird 
 |-  ( ( ( ( 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 ) ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ inf ( { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )
434 eqid 
 |-  { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
435 434 ovolval 
 |-  ( w C_ RR -> ( vol* ` w ) = inf ( { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )
436 435 ad2antrl 
 |-  ( ( ( ( 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 ) ) -> ( vol* ` w ) = inf ( { v e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( w C_ U. ran ( (,) o. f ) /\ v = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )
437 433 436 breqtrrd 
 |-  ( ( ( ( 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 ) ) -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ ( vol* ` w ) )
438 437 expr 
 |-  ( ( ( ( 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 -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ ( vol* ` w ) ) )
439 2 438 sylan2 
 |-  ( ( ( ( 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 e. ~P RR ) -> ( ( vol* ` w ) e. RR -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ ( vol* ` w ) ) )
440 439 ralrimiva 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> A. w e. ~P RR ( ( vol* ` w ) e. RR -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ ( vol* ` w ) ) )
441 ismbl2 
 |-  ( A e. dom vol <-> ( A C_ RR /\ A. w e. ~P RR ( ( vol* ` w ) e. RR -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ ( vol* ` w ) ) ) )
442 441 baibr 
 |-  ( A C_ RR -> ( A. w e. ~P RR ( ( vol* ` w ) e. RR -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ ( vol* ` w ) ) <-> A e. dom vol ) )
443 442 ad2antrr 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( A. w e. ~P RR ( ( vol* ` w ) e. RR -> ( ( vol* ` ( w i^i A ) ) + ( vol* ` ( w \ A ) ) ) <_ ( vol* ` w ) ) <-> A e. dom vol ) )
444 440 443 mpbid 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> A e. dom vol )
445 1 444 impbida 
 |-  ( ( 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 , < ) ) )