Metamath Proof Explorer

Theorem mblfinlem4

Description: Backward direction of ismblfin . (Contributed by Brendan Leahy, 28-Mar-2018) (Revised by Brendan Leahy, 13-Jul-2018)

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

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 1 a1i 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) -> < Or RR )
3 simplr 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) -> ( vol* ` A ) e. RR )
4 vex 
 |-  u e. _V
5 eqeq1 
 |-  ( y = u -> ( y = ( vol ` b ) <-> u = ( vol ` b ) ) )
6 5 anbi2d 
 |-  ( y = u -> ( ( b C_ A /\ y = ( vol ` b ) ) <-> ( b C_ A /\ u = ( vol ` b ) ) ) )
7 6 rexbidv 
 |-  ( y = u -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ u = ( vol ` b ) ) ) )
8 4 7 elab 
 |-  ( u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ u = ( vol ` b ) ) )
9 simprl 
 |-  ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ u = ( vol ` b ) ) ) -> b C_ A )
10 ovolss 
 |-  ( ( b C_ A /\ A C_ RR ) -> ( vol* ` b ) <_ ( vol* ` A ) )
11 sstr 
 |-  ( ( b C_ A /\ A C_ RR ) -> b C_ RR )
12 ovolcl 
 |-  ( b C_ RR -> ( vol* ` b ) e. RR* )
13 11 12 syl 
 |-  ( ( b C_ A /\ A C_ RR ) -> ( vol* ` b ) e. RR* )
14 ovolcl 
 |-  ( A C_ RR -> ( vol* ` A ) e. RR* )
15 14 adantl 
 |-  ( ( b C_ A /\ A C_ RR ) -> ( vol* ` A ) e. RR* )
16 xrlenlt 
 |-  ( ( ( vol* ` b ) e. RR* /\ ( vol* ` A ) e. RR* ) -> ( ( vol* ` b ) <_ ( vol* ` A ) <-> -. ( vol* ` A ) < ( vol* ` b ) ) )
17 13 15 16 syl2anc 
 |-  ( ( b C_ A /\ A C_ RR ) -> ( ( vol* ` b ) <_ ( vol* ` A ) <-> -. ( vol* ` A ) < ( vol* ` b ) ) )
18 10 17 mpbid 
 |-  ( ( b C_ A /\ A C_ RR ) -> -. ( vol* ` A ) < ( vol* ` b ) )
19 18 ancoms 
 |-  ( ( A C_ RR /\ b C_ A ) -> -. ( vol* ` A ) < ( vol* ` b ) )
20 9 19 sylan2 
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ u = ( vol ` b ) ) ) ) -> -. ( vol* ` A ) < ( vol* ` b ) )
21 simprrr 
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ u = ( vol ` b ) ) ) ) -> u = ( vol ` b ) )
22 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
23 22 cldss 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> b C_ RR )
24 dfss4 
 |-  ( b C_ RR <-> ( RR \ ( RR \ b ) ) = b )
25 23 24 sylib 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ ( RR \ b ) ) = b )
26 rembl 
 |-  RR e. dom vol
27 22 cldopn 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ b ) e. ( topGen ` ran (,) ) )
28 opnmbl 
 |-  ( ( RR \ b ) e. ( topGen ` ran (,) ) -> ( RR \ b ) e. dom vol )
29 27 28 syl 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ b ) e. dom vol )
30 difmbl 
 |-  ( ( RR e. dom vol /\ ( RR \ b ) e. dom vol ) -> ( RR \ ( RR \ b ) ) e. dom vol )
31 26 29 30 sylancr 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ ( RR \ b ) ) e. dom vol )
32 25 31 eqeltrrd 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> b e. dom vol )
33 mblvol 
 |-  ( b e. dom vol -> ( vol ` b ) = ( vol* ` b ) )
34 32 33 syl 
 |-  ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` b ) = ( vol* ` b ) )
35 34 ad2antrl 
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ u = ( vol ` b ) ) ) ) -> ( vol ` b ) = ( vol* ` b ) )
36 21 35 eqtrd 
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ u = ( vol ` b ) ) ) ) -> u = ( vol* ` b ) )
37 36 breq2d 
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ u = ( vol ` b ) ) ) ) -> ( ( vol* ` A ) < u <-> ( vol* ` A ) < ( vol* ` b ) ) )
38 20 37 mtbird 
 |-  ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ u = ( vol ` b ) ) ) ) -> -. ( vol* ` A ) < u )
39 38 rexlimdvaa 
 |-  ( A C_ RR -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ u = ( vol ` b ) ) -> -. ( vol* ` A ) < u ) )
40 8 39 syl5bi 
 |-  ( A C_ RR -> ( u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } -> -. ( vol* ` A ) < u ) )
41 40 ad2antrr 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) -> ( u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } -> -. ( vol* ` A ) < u ) )
42 41 imp 
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ) -> -. ( vol* ` A ) < u )
43 1rp 
 |-  1 e. RR+
44 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
45 44 ovolgelb 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ 1 e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + 1 ) ) )
46 43 45 mp3an3 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + 1 ) ) )
47 elmapi 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
48 ssid 
 |-  U. ran ( (,) o. f ) C_ U. ran ( (,) o. f )
49 44 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* , < ) )
50 48 49 mpan2 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
51 50 adantl 
 |-  ( ( ( vol* ` A ) e. RR /\ f : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
52 eqid 
 |-  ( ( abs o. - ) o. f ) = ( ( abs o. - ) o. f )
53 52 44 ovolsf 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) )
54 frn 
 |-  ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ ( 0 [,) +oo ) )
55 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
56 54 55 sstrdi 
 |-  ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* )
57 supxrcl 
 |-  ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* )
58 53 56 57 3syl 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* )
59 peano2re 
 |-  ( ( vol* ` A ) e. RR -> ( ( vol* ` A ) + 1 ) e. RR )
60 59 rexrd 
 |-  ( ( vol* ` A ) e. RR -> ( ( vol* ` A ) + 1 ) e. RR* )
61 rncoss 
 |-  ran ( (,) o. f ) C_ ran (,)
62 61 unissi 
 |-  U. ran ( (,) o. f ) C_ U. ran (,)
63 unirnioo 
 |-  RR = U. ran (,)
64 62 63 sseqtrri 
 |-  U. ran ( (,) o. f ) C_ RR
65 ovolcl 
 |-  ( U. ran ( (,) o. f ) C_ RR -> ( vol* ` U. ran ( (,) o. f ) ) e. RR* )
66 64 65 ax-mp 
 |-  ( vol* ` U. ran ( (,) o. f ) ) e. RR*
67 xrletr 
 |-  ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* /\ ( ( vol* ` A ) + 1 ) e. RR* ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + 1 ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
68 66 67 mp3an1 
 |-  ( ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* /\ ( ( vol* ` A ) + 1 ) e. RR* ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + 1 ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
69 58 60 68 syl2anr 
 |-  ( ( ( vol* ` A ) e. RR /\ f : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + 1 ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
70 51 69 mpand 
 |-  ( ( ( vol* ` A ) e. RR /\ f : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + 1 ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
71 70 adantll 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ f : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + 1 ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
72 47 71 sylan2 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + 1 ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
73 72 anim2d 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + 1 ) ) -> ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) )
74 73 reximdva 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + 1 ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) )
75 46 74 mpd 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
76 rexex 
 |-  ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) -> E. f ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
77 75 76 syl 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> E. f ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
78 77 ad2antrr 
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> E. f ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
79 difss 
 |-  ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. f )
80 79 64 sstri 
 |-  ( U. ran ( (,) o. f ) \ A ) C_ RR
81 ovolcl 
 |-  ( ( U. ran ( (,) o. f ) \ A ) C_ RR -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR* )
82 80 81 ax-mp 
 |-  ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR*
83 59 82 jctil 
 |-  ( ( vol* ` A ) e. RR -> ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR* /\ ( ( vol* ` A ) + 1 ) e. RR ) )
84 83 ad4antlr 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR* /\ ( ( vol* ` A ) + 1 ) e. RR ) )
85 ovolss 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) )
86 79 64 85 mp2an 
 |-  ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( vol* ` U. ran ( (,) o. f ) )
87 xrletr 
 |-  ( ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR* /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ ( ( vol* ` A ) + 1 ) e. RR* ) -> ( ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( ( vol* ` A ) + 1 ) ) )
88 82 66 87 mp3an12 
 |-  ( ( ( vol* ` A ) + 1 ) e. RR* -> ( ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( ( vol* ` A ) + 1 ) ) )
89 60 88 syl 
 |-  ( ( vol* ` A ) e. RR -> ( ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( ( vol* ` A ) + 1 ) ) )
90 86 89 mpani 
 |-  ( ( vol* ` A ) e. RR -> ( ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( ( vol* ` A ) + 1 ) ) )
91 90 ad4antlr 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ A C_ U. ran ( (,) o. f ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( ( vol* ` A ) + 1 ) ) )
92 91 impr 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( ( vol* ` A ) + 1 ) )
93 ovolge0 
 |-  ( ( U. ran ( (,) o. f ) \ A ) C_ RR -> 0 <_ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) )
94 80 93 ax-mp 
 |-  0 <_ ( vol* ` ( U. ran ( (,) o. f ) \ A ) )
95 92 94 jctil 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( 0 <_ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) /\ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( ( vol* ` A ) + 1 ) ) )
96 xrrege0 
 |-  ( ( ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR* /\ ( ( vol* ` A ) + 1 ) e. RR ) /\ ( 0 <_ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) /\ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR )
97 84 95 96 syl2anc 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR )
98 resubcl 
 |-  ( ( ( vol* ` A ) e. RR /\ u e. RR ) -> ( ( vol* ` A ) - u ) e. RR )
99 98 adantrr 
 |-  ( ( ( vol* ` A ) e. RR /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> ( ( vol* ` A ) - u ) e. RR )
100 posdif 
 |-  ( ( u e. RR /\ ( vol* ` A ) e. RR ) -> ( u < ( vol* ` A ) <-> 0 < ( ( vol* ` A ) - u ) ) )
101 100 ancoms 
 |-  ( ( ( vol* ` A ) e. RR /\ u e. RR ) -> ( u < ( vol* ` A ) <-> 0 < ( ( vol* ` A ) - u ) ) )
102 101 biimpd 
 |-  ( ( ( vol* ` A ) e. RR /\ u e. RR ) -> ( u < ( vol* ` A ) -> 0 < ( ( vol* ` A ) - u ) ) )
103 102 impr 
 |-  ( ( ( vol* ` A ) e. RR /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> 0 < ( ( vol* ` A ) - u ) )
104 99 103 elrpd 
 |-  ( ( ( vol* ` A ) e. RR /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> ( ( vol* ` A ) - u ) e. RR+ )
105 104 rphalfcld 
 |-  ( ( ( vol* ` A ) e. RR /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> ( ( ( vol* ` A ) - u ) / 2 ) e. RR+ )
106 3 105 sylan 
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> ( ( ( vol* ` A ) - u ) / 2 ) e. RR+ )
107 106 adantr 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( ( ( vol* ` A ) - u ) / 2 ) e. RR+ )
108 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. g ) ) = seq 1 ( + , ( ( abs o. - ) o. g ) )
109 108 ovolgelb 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ RR /\ ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR /\ ( ( ( vol* ` A ) - u ) / 2 ) e. RR+ ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
110 80 109 mp3an1 
 |-  ( ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR /\ ( ( ( vol* ` A ) - u ) / 2 ) e. RR+ ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
111 97 107 110 syl2anc 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
112 elmapi 
 |-  ( g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> g : NN --> ( <_ i^i ( RR X. RR ) ) )
113 ssid 
 |-  U. ran ( (,) o. g ) C_ U. ran ( (,) o. g )
114 108 ovollb 
 |-  ( ( g : NN --> ( <_ i^i ( RR X. RR ) ) /\ U. ran ( (,) o. g ) C_ U. ran ( (,) o. g ) ) -> ( vol* ` U. ran ( (,) o. g ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) )
115 113 114 mpan2 
 |-  ( g : NN --> ( <_ i^i ( RR X. RR ) ) -> ( vol* ` U. ran ( (,) o. g ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) )
116 115 adantl 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ g : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( vol* ` U. ran ( (,) o. g ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) )
117 eqid 
 |-  ( ( abs o. - ) o. g ) = ( ( abs o. - ) o. g )
118 117 108 ovolsf 
 |-  ( g : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. g ) ) : NN --> ( 0 [,) +oo ) )
119 frn 
 |-  ( seq 1 ( + , ( ( abs o. - ) o. g ) ) : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , ( ( abs o. - ) o. g ) ) C_ ( 0 [,) +oo ) )
120 119 55 sstrdi 
 |-  ( seq 1 ( + , ( ( abs o. - ) o. g ) ) : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , ( ( abs o. - ) o. g ) ) C_ RR* )
121 supxrcl 
 |-  ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) C_ RR* -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) e. RR* )
122 118 120 121 3syl 
 |-  ( g : NN --> ( <_ i^i ( RR X. RR ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) e. RR* )
123 99 rehalfcld 
 |-  ( ( ( vol* ` A ) e. RR /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> ( ( ( vol* ` A ) - u ) / 2 ) e. RR )
124 3 123 sylan 
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> ( ( ( vol* ` A ) - u ) / 2 ) e. RR )
125 124 adantr 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( ( ( vol* ` A ) - u ) / 2 ) e. RR )
126 97 125 readdcld 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) e. RR )
127 126 rexrd 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) e. RR* )
128 rncoss 
 |-  ran ( (,) o. g ) C_ ran (,)
129 128 unissi 
 |-  U. ran ( (,) o. g ) C_ U. ran (,)
130 129 63 sseqtrri 
 |-  U. ran ( (,) o. g ) C_ RR
131 ovolcl 
 |-  ( U. ran ( (,) o. g ) C_ RR -> ( vol* ` U. ran ( (,) o. g ) ) e. RR* )
132 130 131 ax-mp 
 |-  ( vol* ` U. ran ( (,) o. g ) ) e. RR*
133 xrletr 
 |-  ( ( ( vol* ` U. ran ( (,) o. g ) ) e. RR* /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) e. RR* /\ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) e. RR* ) -> ( ( ( vol* ` U. ran ( (,) o. g ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) -> ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
134 132 133 mp3an1 
 |-  ( ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) e. RR* /\ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) e. RR* ) -> ( ( ( vol* ` U. ran ( (,) o. g ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) -> ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
135 122 127 134 syl2anr 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ g : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. g ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) -> ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
136 116 135 mpand 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ g : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) -> ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
137 112 136 sylan2 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) -> ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
138 137 anim2d 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) -> ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) )
139 138 reximdva 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. g ) ) , RR* , < ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) )
140 111 139 mpd 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
141 rexex 
 |-  ( E. g e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) -> E. g ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
142 140 141 syl 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> E. g ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
143 59 66 jctil 
 |-  ( ( vol* ` A ) e. RR -> ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ ( ( vol* ` A ) + 1 ) e. RR ) )
144 143 ad3antlr 
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ ( ( vol* ` A ) + 1 ) e. RR ) )
145 ovolge0 
 |-  ( U. ran ( (,) o. f ) C_ RR -> 0 <_ ( vol* ` U. ran ( (,) o. f ) ) )
146 64 145 ax-mp 
 |-  0 <_ ( vol* ` U. ran ( (,) o. f ) )
147 146 jctl 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) -> ( 0 <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
148 147 adantl 
 |-  ( ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) -> ( 0 <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) )
149 xrrege0 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ ( ( vol* ` A ) + 1 ) e. RR ) /\ ( 0 <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. RR )
150 144 148 149 syl2an 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. RR )
151 150 125 resubcld 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) e. RR )
152 150 107 ltsubrpd 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` U. ran ( (,) o. f ) ) )
153 retop 
 |-  ( topGen ` ran (,) ) e. Top
154 retopbas 
 |-  ran (,) e. TopBases
155 bastg 
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
156 154 155 ax-mp 
 |-  ran (,) C_ ( topGen ` ran (,) )
157 61 156 sstri 
 |-  ran ( (,) o. f ) C_ ( topGen ` ran (,) )
158 uniopn 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ran ( (,) o. f ) C_ ( topGen ` ran (,) ) ) -> U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) )
159 153 157 158 mp2an 
 |-  U. ran ( (,) o. f ) e. ( topGen ` ran (,) )
160 mblfinlem2 
 |-  ( ( U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) e. RR /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` U. ran ( (,) o. f ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) )
161 159 160 mp3an1 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) e. RR /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` U. ran ( (,) o. f ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) )
162 151 152 161 syl2anc 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) )
163 162 adantr 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) )
164 indif2 
 |-  ( s i^i ( RR \ U. ran ( (,) o. g ) ) ) = ( ( s i^i RR ) \ U. ran ( (,) o. g ) )
165 22 cldss 
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> s C_ RR )
166 df-ss 
 |-  ( s C_ RR <-> ( s i^i RR ) = s )
167 165 166 sylib 
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s i^i RR ) = s )
168 167 difeq1d 
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( ( s i^i RR ) \ U. ran ( (,) o. g ) ) = ( s \ U. ran ( (,) o. g ) ) )
169 164 168 syl5eq 
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s i^i ( RR \ U. ran ( (,) o. g ) ) ) = ( s \ U. ran ( (,) o. g ) ) )
170 128 156 sstri 
 |-  ran ( (,) o. g ) C_ ( topGen ` ran (,) )
171 uniopn 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ran ( (,) o. g ) C_ ( topGen ` ran (,) ) ) -> U. ran ( (,) o. g ) e. ( topGen ` ran (,) ) )
172 153 170 171 mp2an 
 |-  U. ran ( (,) o. g ) e. ( topGen ` ran (,) )
173 22 opncld 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ U. ran ( (,) o. g ) e. ( topGen ` ran (,) ) ) -> ( RR \ U. ran ( (,) o. g ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
174 153 172 173 mp2an 
 |-  ( RR \ U. ran ( (,) o. g ) ) e. ( Clsd ` ( topGen ` ran (,) ) )
175 incld 
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( RR \ U. ran ( (,) o. g ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( s i^i ( RR \ U. ran ( (,) o. g ) ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
176 174 175 mpan2 
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s i^i ( RR \ U. ran ( (,) o. g ) ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
177 169 176 eqeltrrd 
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s \ U. ran ( (,) o. g ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
178 simpr 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ s C_ U. ran ( (,) o. f ) ) -> s C_ U. ran ( (,) o. f ) )
179 simpl 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ s C_ U. ran ( (,) o. f ) ) -> ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) )
180 178 179 ssdif2d 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ s C_ U. ran ( (,) o. f ) ) -> ( s \ U. ran ( (,) o. g ) ) C_ ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) )
181 dfin4 
 |-  ( U. ran ( (,) o. f ) i^i A ) = ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) )
182 inss2 
 |-  ( U. ran ( (,) o. f ) i^i A ) C_ A
183 181 182 eqsstrri 
 |-  ( U. ran ( (,) o. f ) \ ( U. ran ( (,) o. f ) \ A ) ) C_ A
184 180 183 sstrdi 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ s C_ U. ran ( (,) o. f ) ) -> ( s \ U. ran ( (,) o. g ) ) C_ A )
185 sseq1 
 |-  ( b = ( s \ U. ran ( (,) o. g ) ) -> ( b C_ A <-> ( s \ U. ran ( (,) o. g ) ) C_ A ) )
186 185 anbi1d 
 |-  ( b = ( s \ U. ran ( (,) o. g ) ) -> ( ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) <-> ( ( s \ U. ran ( (,) o. g ) ) C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) ) )
187 fveq2 
 |-  ( ( s \ U. ran ( (,) o. g ) ) = b -> ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) )
188 187 eqcoms 
 |-  ( b = ( s \ U. ran ( (,) o. g ) ) -> ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) )
189 188 biantrud 
 |-  ( b = ( s \ U. ran ( (,) o. g ) ) -> ( ( s \ U. ran ( (,) o. g ) ) C_ A <-> ( ( s \ U. ran ( (,) o. g ) ) C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) ) )
190 186 189 bitr4d 
 |-  ( b = ( s \ U. ran ( (,) o. g ) ) -> ( ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) <-> ( s \ U. ran ( (,) o. g ) ) C_ A ) )
191 190 rspcev 
 |-  ( ( ( s \ U. ran ( (,) o. g ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s \ U. ran ( (,) o. g ) ) C_ A ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) )
192 177 184 191 syl2an 
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ s C_ U. ran ( (,) o. f ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) )
193 192 an12s 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ s C_ U. ran ( (,) o. f ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) )
194 193 adantrrr 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) )
195 194 adantlr 
 |-  ( ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) )
196 195 adantll 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) )
197 difss 
 |-  ( A \ ( s \ U. ran ( (,) o. g ) ) ) C_ A
198 ovolsscl 
 |-  ( ( ( A \ ( s \ U. ran ( (,) o. g ) ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) e. RR )
199 197 198 mp3an1 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) e. RR )
200 199 ad5antr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) e. RR )
201 simp-6r 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` A ) e. RR )
202 simpl 
 |-  ( ( u e. RR /\ u < ( vol* ` A ) ) -> u e. RR )
203 202 ad4antlr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> u e. RR )
204 difdif2 
 |-  ( A \ ( s \ U. ran ( (,) o. g ) ) ) = ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) )
205 204 fveq2i 
 |-  ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) = ( vol* ` ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) ) )
206 difss 
 |-  ( A \ s ) C_ A
207 inss1 
 |-  ( A i^i U. ran ( (,) o. g ) ) C_ A
208 206 207 unssi 
 |-  ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) ) C_ A
209 ovolsscl 
 |-  ( ( ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) ) ) e. RR )
210 208 209 mp3an1 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) ) ) e. RR )
211 210 ad5antr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) ) ) e. RR )
212 ovolsscl 
 |-  ( ( ( A \ s ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ s ) ) e. RR )
213 206 212 mp3an1 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ s ) ) e. RR )
214 213 ad5antr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( A \ s ) ) e. RR )
215 ovolsscl 
 |-  ( ( ( A i^i U. ran ( (,) o. g ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) e. RR )
216 207 215 mp3an1 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) e. RR )
217 216 ad5antr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) e. RR )
218 214 217 readdcld 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) ) e. RR )
219 3 202 98 syl2an 
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> ( ( vol* ` A ) - u ) e. RR )
220 219 ad3antrrr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` A ) - u ) e. RR )
221 ssdifss 
 |-  ( A C_ RR -> ( A \ s ) C_ RR )
222 221 adantr 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( A \ s ) C_ RR )
223 ssinss1 
 |-  ( A C_ RR -> ( A i^i U. ran ( (,) o. g ) ) C_ RR )
224 223 adantr 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( A i^i U. ran ( (,) o. g ) ) C_ RR )
225 ovolun 
 |-  ( ( ( ( A \ s ) C_ RR /\ ( vol* ` ( A \ s ) ) e. RR ) /\ ( ( A i^i U. ran ( (,) o. g ) ) C_ RR /\ ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) e. RR ) ) -> ( vol* ` ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) ) )
226 222 213 224 216 225 syl22anc 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) ) )
227 226 ad5antr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) ) )
228 124 ad2antrr 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( ( ( vol* ` A ) - u ) / 2 ) e. RR )
229 228 adantr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( ( vol* ` A ) - u ) / 2 ) e. RR )
230 150 ad2antrr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. RR )
231 simprl 
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) -> s C_ U. ran ( (,) o. f ) )
232 150 adantr 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. RR )
233 ovolsscl 
 |-  ( ( s C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` s ) e. RR )
234 64 233 mp3an2 
 |-  ( ( s C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` s ) e. RR )
235 231 232 234 syl2anr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` s ) e. RR )
236 230 235 resubcld 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` s ) ) e. RR )
237 ssdif 
 |-  ( A C_ U. ran ( (,) o. f ) -> ( A \ s ) C_ ( U. ran ( (,) o. f ) \ s ) )
238 difss 
 |-  ( U. ran ( (,) o. f ) \ s ) C_ U. ran ( (,) o. f )
239 238 64 sstri 
 |-  ( U. ran ( (,) o. f ) \ s ) C_ RR
240 ovolss 
 |-  ( ( ( A \ s ) C_ ( U. ran ( (,) o. f ) \ s ) /\ ( U. ran ( (,) o. f ) \ s ) C_ RR ) -> ( vol* ` ( A \ s ) ) <_ ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) )
241 237 239 240 sylancl 
 |-  ( A C_ U. ran ( (,) o. f ) -> ( vol* ` ( A \ s ) ) <_ ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) )
242 241 adantr 
 |-  ( ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) -> ( vol* ` ( A \ s ) ) <_ ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) )
243 242 ad3antlr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( A \ s ) ) <_ ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) )
244 eleq1w 
 |-  ( b = s -> ( b e. dom vol <-> s e. dom vol ) )
245 244 32 vtoclga 
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> s e. dom vol )
246 245 adantr 
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) -> s e. dom vol )
247 mblsplit 
 |-  ( ( s e. dom vol /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` U. ran ( (,) o. f ) ) = ( ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) ) )
248 64 247 mp3an2 
 |-  ( ( s e. dom vol /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` U. ran ( (,) o. f ) ) = ( ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) ) )
249 246 232 248 syl2anr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) = ( ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) ) )
250 249 eqcomd 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) )
251 230 recnd 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. CC )
252 inss1 
 |-  ( U. ran ( (,) o. f ) i^i s ) C_ U. ran ( (,) o. f )
253 ovolsscl 
 |-  ( ( ( U. ran ( (,) o. f ) i^i s ) 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 s ) ) e. RR )
254 252 64 253 mp3an12 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) e. RR )
255 150 254 syl 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) e. RR )
256 255 ad2antrr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) e. RR )
257 256 recnd 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) e. CC )
258 ovolsscl 
 |-  ( ( ( U. ran ( (,) o. f ) \ s ) C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) e. RR )
259 238 64 258 mp3an12 
 |-  ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) e. RR )
260 150 259 syl 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) e. RR )
261 260 recnd 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) e. CC )
262 261 ad2antrr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) e. CC )
263 251 257 262 subaddd 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) <-> ( ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) ) )
264 250 263 mpbird 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) )
265 sseqin2 
 |-  ( s C_ U. ran ( (,) o. f ) <-> ( U. ran ( (,) o. f ) i^i s ) = s )
266 265 biimpi 
 |-  ( s C_ U. ran ( (,) o. f ) -> ( U. ran ( (,) o. f ) i^i s ) = s )
267 266 fveq2d 
 |-  ( s C_ U. ran ( (,) o. f ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) = ( vol* ` s ) )
268 267 oveq2d 
 |-  ( s C_ U. ran ( (,) o. f ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) ) = ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` s ) ) )
269 268 adantr 
 |-  ( ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) ) = ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` s ) ) )
270 269 ad2antll 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i s ) ) ) = ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` s ) ) )
271 264 270 eqtr3d 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ s ) ) = ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` s ) ) )
272 243 271 breqtrd 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( A \ s ) ) <_ ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` s ) ) )
273 simprrr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) )
274 230 229 235 273 ltsub23d 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` s ) ) < ( ( ( vol* ` A ) - u ) / 2 ) )
275 214 236 229 272 274 lelttrd 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( A \ s ) ) < ( ( ( vol* ` A ) - u ) / 2 ) )
276 216 ad4antr 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) e. RR )
277 126 132 jctil 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> ( ( vol* ` U. ran ( (,) o. g ) ) e. RR* /\ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) e. RR ) )
278 simpr 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) -> ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) )
279 ovolge0 
 |-  ( U. ran ( (,) o. g ) C_ RR -> 0 <_ ( vol* ` U. ran ( (,) o. g ) ) )
280 130 279 ax-mp 
 |-  0 <_ ( vol* ` U. ran ( (,) o. g ) )
281 278 280 jctil 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) -> ( 0 <_ ( vol* ` U. ran ( (,) o. g ) ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
282 xrrege0 
 |-  ( ( ( ( vol* ` U. ran ( (,) o. g ) ) e. RR* /\ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) e. RR ) /\ ( 0 <_ ( vol* ` U. ran ( (,) o. g ) ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` U. ran ( (,) o. g ) ) e. RR )
283 277 281 282 syl2an 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` U. ran ( (,) o. g ) ) e. RR )
284 difss 
 |-  ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) C_ U. ran ( (,) o. g )
285 ovolsscl 
 |-  ( ( ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) C_ U. ran ( (,) o. g ) /\ U. ran ( (,) o. g ) C_ RR /\ ( vol* ` U. ran ( (,) o. g ) ) e. RR ) -> ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) e. RR )
286 284 130 285 mp3an12 
 |-  ( ( vol* ` U. ran ( (,) o. g ) ) e. RR -> ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) e. RR )
287 283 286 syl 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) e. RR )
288 ssun2 
 |-  ( U. ran ( (,) o. g ) i^i A ) C_ ( ( U. ran ( (,) o. g ) \ U. ran ( (,) o. f ) ) u. ( U. ran ( (,) o. g ) i^i A ) )
289 incom 
 |-  ( A i^i U. ran ( (,) o. g ) ) = ( U. ran ( (,) o. g ) i^i A )
290 difdif2 
 |-  ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) = ( ( U. ran ( (,) o. g ) \ U. ran ( (,) o. f ) ) u. ( U. ran ( (,) o. g ) i^i A ) )
291 288 289 290 3sstr4i 
 |-  ( A i^i U. ran ( (,) o. g ) ) C_ ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) )
292 284 130 sstri 
 |-  ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) C_ RR
293 291 292 pm3.2i 
 |-  ( ( A i^i U. ran ( (,) o. g ) ) C_ ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) /\ ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) C_ RR )
294 ovolss 
 |-  ( ( ( A i^i U. ran ( (,) o. g ) ) C_ ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) /\ ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) C_ RR ) -> ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) <_ ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) )
295 293 294 mp1i 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) <_ ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) )
296 opnmbl 
 |-  ( U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) -> U. ran ( (,) o. f ) e. dom vol )
297 159 296 ax-mp 
 |-  U. ran ( (,) o. f ) e. dom vol
298 difmbl 
 |-  ( ( U. ran ( (,) o. f ) e. dom vol /\ A e. dom vol ) -> ( U. ran ( (,) o. f ) \ A ) e. dom vol )
299 297 298 mpan 
 |-  ( A e. dom vol -> ( U. ran ( (,) o. f ) \ A ) e. dom vol )
300 299 ad4antlr 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( U. ran ( (,) o. f ) \ A ) e. dom vol )
301 mblsplit 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) e. dom vol /\ U. ran ( (,) o. g ) C_ RR /\ ( vol* ` U. ran ( (,) o. g ) ) e. RR ) -> ( vol* ` U. ran ( (,) o. g ) ) = ( ( vol* ` ( U. ran ( (,) o. g ) i^i ( U. ran ( (,) o. f ) \ A ) ) ) + ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) ) )
302 130 301 mp3an2 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) e. dom vol /\ ( vol* ` U. ran ( (,) o. g ) ) e. RR ) -> ( vol* ` U. ran ( (,) o. g ) ) = ( ( vol* ` ( U. ran ( (,) o. g ) i^i ( U. ran ( (,) o. f ) \ A ) ) ) + ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) ) )
303 300 283 302 syl2anc 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` U. ran ( (,) o. g ) ) = ( ( vol* ` ( U. ran ( (,) o. g ) i^i ( U. ran ( (,) o. f ) \ A ) ) ) + ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) ) )
304 sseqin2 
 |-  ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) <-> ( U. ran ( (,) o. g ) i^i ( U. ran ( (,) o. f ) \ A ) ) = ( U. ran ( (,) o. f ) \ A ) )
305 304 biimpi 
 |-  ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) -> ( U. ran ( (,) o. g ) i^i ( U. ran ( (,) o. f ) \ A ) ) = ( U. ran ( (,) o. f ) \ A ) )
306 305 fveq2d 
 |-  ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) -> ( vol* ` ( U. ran ( (,) o. g ) i^i ( U. ran ( (,) o. f ) \ A ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) )
307 306 oveq1d 
 |-  ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) -> ( ( vol* ` ( U. ran ( (,) o. g ) i^i ( U. ran ( (,) o. f ) \ A ) ) ) + ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) ) = ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) ) )
308 307 ad2antrl 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( ( vol* ` ( U. ran ( (,) o. g ) i^i ( U. ran ( (,) o. f ) \ A ) ) ) + ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) ) = ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) ) )
309 303 308 eqtr2d 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) ) = ( vol* ` U. ran ( (,) o. g ) ) )
310 283 recnd 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` U. ran ( (,) o. g ) ) e. CC )
311 97 adantr 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. RR )
312 311 recnd 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) e. CC )
313 287 recnd 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) e. CC )
314 310 312 313 subaddd 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. g ) ) - ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) ) = ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) <-> ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) ) = ( vol* ` U. ran ( (,) o. g ) ) ) )
315 309 314 mpbird 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. g ) ) - ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) ) = ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) )
316 simprr 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) )
317 283 311 228 lesubadd2d 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. g ) ) - ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) ) <_ ( ( ( vol* ` A ) - u ) / 2 ) <-> ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) )
318 316 317 mpbird 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. g ) ) - ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) ) <_ ( ( ( vol* ` A ) - u ) / 2 ) )
319 315 318 eqbrtrrd 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. g ) \ ( U. ran ( (,) o. f ) \ A ) ) ) <_ ( ( ( vol* ` A ) - u ) / 2 ) )
320 276 287 228 295 319 letrd 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) <_ ( ( ( vol* ` A ) - u ) / 2 ) )
321 320 adantr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) <_ ( ( ( vol* ` A ) - u ) / 2 ) )
322 214 217 229 229 275 321 ltleaddd 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) ) < ( ( ( ( vol* ` A ) - u ) / 2 ) + ( ( ( vol* ` A ) - u ) / 2 ) ) )
323 98 recnd 
 |-  ( ( ( vol* ` A ) e. RR /\ u e. RR ) -> ( ( vol* ` A ) - u ) e. CC )
324 323 2halvesd 
 |-  ( ( ( vol* ` A ) e. RR /\ u e. RR ) -> ( ( ( ( vol* ` A ) - u ) / 2 ) + ( ( ( vol* ` A ) - u ) / 2 ) ) = ( ( vol* ` A ) - u ) )
325 324 adantll 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ u e. RR ) -> ( ( ( ( vol* ` A ) - u ) / 2 ) + ( ( ( vol* ` A ) - u ) / 2 ) ) = ( ( vol* ` A ) - u ) )
326 325 ad2ant2r 
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> ( ( ( ( vol* ` A ) - u ) / 2 ) + ( ( ( vol* ` A ) - u ) / 2 ) ) = ( ( vol* ` A ) - u ) )
327 326 ad3antrrr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( ( ( vol* ` A ) - u ) / 2 ) + ( ( ( vol* ` A ) - u ) / 2 ) ) = ( ( vol* ` A ) - u ) )
328 322 327 breqtrd 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( A i^i U. ran ( (,) o. g ) ) ) ) < ( ( vol* ` A ) - u ) )
329 211 218 220 227 328 lelttrd 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( A i^i U. ran ( (,) o. g ) ) ) ) < ( ( vol* ` A ) - u ) )
330 205 329 eqbrtrid 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) < ( ( vol* ` A ) - u ) )
331 200 201 203 330 ltsub13d 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> u < ( ( vol* ` A ) - ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) )
332 opnmbl 
 |-  ( U. ran ( (,) o. g ) e. ( topGen ` ran (,) ) -> U. ran ( (,) o. g ) e. dom vol )
333 172 332 ax-mp 
 |-  U. ran ( (,) o. g ) e. dom vol
334 difmbl 
 |-  ( ( s e. dom vol /\ U. ran ( (,) o. g ) e. dom vol ) -> ( s \ U. ran ( (,) o. g ) ) e. dom vol )
335 245 333 334 sylancl 
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s \ U. ran ( (,) o. g ) ) e. dom vol )
336 mblvol 
 |-  ( ( s \ U. ran ( (,) o. g ) ) e. dom vol -> ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. g ) ) ) )
337 335 336 syl 
 |-  ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. g ) ) ) )
338 337 ad2antrl 
 |-  ( ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. g ) ) ) )
339 sseqin2 
 |-  ( ( s \ U. ran ( (,) o. g ) ) C_ A <-> ( A i^i ( s \ U. ran ( (,) o. g ) ) ) = ( s \ U. ran ( (,) o. g ) ) )
340 184 339 sylib 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ s C_ U. ran ( (,) o. f ) ) -> ( A i^i ( s \ U. ran ( (,) o. g ) ) ) = ( s \ U. ran ( (,) o. g ) ) )
341 340 fveq2d 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ s C_ U. ran ( (,) o. f ) ) -> ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. g ) ) ) )
342 341 adantrr 
 |-  ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) -> ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. g ) ) ) )
343 342 ad2ant2rl 
 |-  ( ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. g ) ) ) )
344 338 343 eqtr4d 
 |-  ( ( ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) )
345 344 adantll 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) )
346 335 adantr 
 |-  ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) -> ( s \ U. ran ( (,) o. g ) ) e. dom vol )
347 simp-4l 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
348 mblsplit 
 |-  ( ( ( s \ U. ran ( (,) o. g ) ) e. dom vol /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` A ) = ( ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) + ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) )
349 348 3expb 
 |-  ( ( ( s \ U. ran ( (,) o. g ) ) e. dom vol /\ ( A C_ RR /\ ( vol* ` A ) e. RR ) ) -> ( vol* ` A ) = ( ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) + ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) )
350 349 eqcomd 
 |-  ( ( ( s \ U. ran ( (,) o. g ) ) e. dom vol /\ ( A C_ RR /\ ( vol* ` A ) e. RR ) ) -> ( ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) + ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) = ( vol* ` A ) )
351 346 347 350 syl2anr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) + ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) = ( vol* ` A ) )
352 recn 
 |-  ( ( vol* ` A ) e. RR -> ( vol* ` A ) e. CC )
353 352 adantl 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` A ) e. CC )
354 199 recnd 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) e. CC )
355 inss1 
 |-  ( A i^i ( s \ U. ran ( (,) o. g ) ) ) C_ A
356 ovolsscl 
 |-  ( ( ( A i^i ( s \ U. ran ( (,) o. g ) ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) e. RR )
357 355 356 mp3an1 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) e. RR )
358 357 recnd 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) e. CC )
359 353 354 358 subadd2d 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( ( vol* ` A ) - ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) = ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) <-> ( ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) + ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) = ( vol* ` A ) ) )
360 359 ad5antr 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( ( vol* ` A ) - ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) = ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) <-> ( ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) + ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) = ( vol* ` A ) ) )
361 351 360 mpbird 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( ( vol* ` A ) - ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) = ( vol* ` ( A i^i ( s \ U. ran ( (,) o. g ) ) ) ) )
362 345 361 eqtr4d 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( ( vol* ` A ) - ( vol* ` ( A \ ( s \ U. ran ( (,) o. g ) ) ) ) ) )
363 331 362 breqtrrd 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> u < ( vol ` ( s \ U. ran ( (,) o. g ) ) ) )
364 fvex 
 |-  ( vol ` ( s \ U. ran ( (,) o. g ) ) ) e. _V
365 eqeq1 
 |-  ( v = ( vol ` ( s \ U. ran ( (,) o. g ) ) ) -> ( v = ( vol ` b ) <-> ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) )
366 365 anbi2d 
 |-  ( v = ( vol ` ( s \ U. ran ( (,) o. g ) ) ) -> ( ( b C_ A /\ v = ( vol ` b ) ) <-> ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) ) )
367 366 rexbidv 
 |-  ( v = ( vol ` ( s \ U. ran ( (,) o. g ) ) ) -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) ) )
368 breq2 
 |-  ( v = ( vol ` ( s \ U. ran ( (,) o. g ) ) ) -> ( u < v <-> u < ( vol ` ( s \ U. ran ( (,) o. g ) ) ) ) )
369 367 368 anbi12d 
 |-  ( v = ( vol ` ( s \ U. ran ( (,) o. g ) ) ) -> ( ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ u < v ) <-> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) /\ u < ( vol ` ( s \ U. ran ( (,) o. g ) ) ) ) ) )
370 364 369 spcev 
 |-  ( ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ ( vol ` ( s \ U. ran ( (,) o. g ) ) ) = ( vol ` b ) ) /\ u < ( vol ` ( s \ U. ran ( (,) o. g ) ) ) ) -> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ u < v ) )
371 196 363 370 syl2anc 
 |-  ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s C_ U. ran ( (,) o. f ) /\ ( ( vol* ` U. ran ( (,) o. f ) ) - ( ( ( vol* ` A ) - u ) / 2 ) ) < ( vol* ` s ) ) ) ) -> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ u < v ) )
372 163 371 rexlimddv 
 |-  ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) /\ ( ( U. ran ( (,) o. f ) \ A ) C_ U. ran ( (,) o. g ) /\ ( vol* ` U. ran ( (,) o. g ) ) <_ ( ( vol* ` ( U. ran ( (,) o. f ) \ A ) ) + ( ( ( vol* ` A ) - u ) / 2 ) ) ) ) -> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ u < v ) )
373 142 372 exlimddv 
 |-  ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) /\ ( A C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` A ) + 1 ) ) ) -> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ u < v ) )
374 78 373 exlimddv 
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ u < v ) )
375 eqeq1 
 |-  ( y = v -> ( y = ( vol ` b ) <-> v = ( vol ` b ) ) )
376 375 anbi2d 
 |-  ( y = v -> ( ( b C_ A /\ y = ( vol ` b ) ) <-> ( b C_ A /\ v = ( vol ` b ) ) ) )
377 376 rexbidv 
 |-  ( y = v -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) ) )
378 377 rexab 
 |-  ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } u < v <-> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ u < v ) )
379 374 378 sylibr 
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) /\ ( u e. RR /\ u < ( vol* ` A ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } u < v )
380 2 3 42 379 eqsupd 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ A e. dom vol ) -> sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) = ( vol* ` A ) )
381 380 eqcomd 
 |-  ( ( ( 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 , < ) )