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 syl5bir
 |-  ( ( ( 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 syl5bir
 |-  ( ( 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 , < ) ) )