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