Step |
Hyp |
Ref |
Expression |
1 |
|
ltso |
|- < Or RR |
2 |
1
|
a1i |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) -> < Or RR ) |
3 |
|
difss |
|- ( A \ B ) C_ A |
4 |
|
ovolsscl |
|- ( ( ( A \ B ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ B ) ) e. RR ) |
5 |
3 4
|
mp3an1 |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ B ) ) e. RR ) |
6 |
5
|
3ad2ant1 |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) -> ( vol* ` ( A \ B ) ) e. RR ) |
7 |
|
vex |
|- u e. _V |
8 |
|
eqeq1 |
|- ( y = u -> ( y = ( vol ` b ) <-> u = ( vol ` b ) ) ) |
9 |
8
|
anbi2d |
|- ( y = u -> ( ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) <-> ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) |
10 |
9
|
rexbidv |
|- ( y = u -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) |
11 |
7 10
|
elab |
|- ( u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) |
12 |
|
simprl |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) -> b C_ ( A \ B ) ) |
13 |
|
ssdifss |
|- ( A C_ RR -> ( A \ B ) C_ RR ) |
14 |
|
ovolss |
|- ( ( b C_ ( A \ B ) /\ ( A \ B ) C_ RR ) -> ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) ) |
15 |
12 13 14
|
syl2anr |
|- ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) -> ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) ) |
16 |
|
uniretop |
|- RR = U. ( topGen ` ran (,) ) |
17 |
16
|
cldss |
|- ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> b C_ RR ) |
18 |
|
ovolcl |
|- ( b C_ RR -> ( vol* ` b ) e. RR* ) |
19 |
17 18
|
syl |
|- ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol* ` b ) e. RR* ) |
20 |
|
ovolcl |
|- ( ( A \ B ) C_ RR -> ( vol* ` ( A \ B ) ) e. RR* ) |
21 |
13 20
|
syl |
|- ( A C_ RR -> ( vol* ` ( A \ B ) ) e. RR* ) |
22 |
|
xrlenlt |
|- ( ( ( vol* ` b ) e. RR* /\ ( vol* ` ( A \ B ) ) e. RR* ) -> ( ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) ) |
23 |
19 21 22
|
syl2anr |
|- ( ( A C_ RR /\ b e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) ) |
24 |
23
|
adantrr |
|- ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) -> ( ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) ) |
25 |
|
id |
|- ( u = ( vol ` b ) -> u = ( vol ` b ) ) |
26 |
|
dfss4 |
|- ( b C_ RR <-> ( RR \ ( RR \ b ) ) = b ) |
27 |
17 26
|
sylib |
|- ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ ( RR \ b ) ) = b ) |
28 |
|
rembl |
|- RR e. dom vol |
29 |
16
|
cldopn |
|- ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ b ) e. ( topGen ` ran (,) ) ) |
30 |
|
opnmbl |
|- ( ( RR \ b ) e. ( topGen ` ran (,) ) -> ( RR \ b ) e. dom vol ) |
31 |
29 30
|
syl |
|- ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ b ) e. dom vol ) |
32 |
|
difmbl |
|- ( ( RR e. dom vol /\ ( RR \ b ) e. dom vol ) -> ( RR \ ( RR \ b ) ) e. dom vol ) |
33 |
28 31 32
|
sylancr |
|- ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ ( RR \ b ) ) e. dom vol ) |
34 |
27 33
|
eqeltrrd |
|- ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> b e. dom vol ) |
35 |
|
mblvol |
|- ( b e. dom vol -> ( vol ` b ) = ( vol* ` b ) ) |
36 |
34 35
|
syl |
|- ( b e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` b ) = ( vol* ` b ) ) |
37 |
25 36
|
sylan9eqr |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ u = ( vol ` b ) ) -> u = ( vol* ` b ) ) |
38 |
37
|
breq2d |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ u = ( vol ` b ) ) -> ( ( vol* ` ( A \ B ) ) < u <-> ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) ) |
39 |
38
|
notbid |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ u = ( vol ` b ) ) -> ( -. ( vol* ` ( A \ B ) ) < u <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) ) |
40 |
39
|
adantrl |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) -> ( -. ( vol* ` ( A \ B ) ) < u <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) ) |
41 |
40
|
adantl |
|- ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) -> ( -. ( vol* ` ( A \ B ) ) < u <-> -. ( vol* ` ( A \ B ) ) < ( vol* ` b ) ) ) |
42 |
24 41
|
bitr4d |
|- ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) -> ( ( vol* ` b ) <_ ( vol* ` ( A \ B ) ) <-> -. ( vol* ` ( A \ B ) ) < u ) ) |
43 |
15 42
|
mpbid |
|- ( ( A C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) ) -> -. ( vol* ` ( A \ B ) ) < u ) |
44 |
43
|
rexlimdvaa |
|- ( A C_ RR -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) -> -. ( vol* ` ( A \ B ) ) < u ) ) |
45 |
44
|
imp |
|- ( ( A C_ RR /\ E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ u = ( vol ` b ) ) ) -> -. ( vol* ` ( A \ B ) ) < u ) |
46 |
11 45
|
sylan2b |
|- ( ( A C_ RR /\ u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } ) -> -. ( vol* ` ( A \ B ) ) < u ) |
47 |
46
|
adantlr |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } ) -> -. ( vol* ` ( A \ B ) ) < u ) |
48 |
47
|
3ad2antl1 |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) /\ u e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } ) -> -. ( vol* ` ( A \ B ) ) < u ) |
49 |
|
simplr |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( vol* ` A ) e. RR ) |
50 |
|
resubcl |
|- ( ( ( vol* ` ( A \ B ) ) e. RR /\ u e. RR ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR ) |
51 |
50
|
adantrr |
|- ( ( ( vol* ` ( A \ B ) ) e. RR /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR ) |
52 |
|
posdif |
|- ( ( u e. RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( u < ( vol* ` ( A \ B ) ) <-> 0 < ( ( vol* ` ( A \ B ) ) - u ) ) ) |
53 |
52
|
ancoms |
|- ( ( ( vol* ` ( A \ B ) ) e. RR /\ u e. RR ) -> ( u < ( vol* ` ( A \ B ) ) <-> 0 < ( ( vol* ` ( A \ B ) ) - u ) ) ) |
54 |
53
|
biimpd |
|- ( ( ( vol* ` ( A \ B ) ) e. RR /\ u e. RR ) -> ( u < ( vol* ` ( A \ B ) ) -> 0 < ( ( vol* ` ( A \ B ) ) - u ) ) ) |
55 |
54
|
impr |
|- ( ( ( vol* ` ( A \ B ) ) e. RR /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> 0 < ( ( vol* ` ( A \ B ) ) - u ) ) |
56 |
51 55
|
elrpd |
|- ( ( ( vol* ` ( A \ B ) ) e. RR /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR+ ) |
57 |
|
3nn |
|- 3 e. NN |
58 |
|
nnrp |
|- ( 3 e. NN -> 3 e. RR+ ) |
59 |
57 58
|
ax-mp |
|- 3 e. RR+ |
60 |
|
rpdivcl |
|- ( ( ( ( vol* ` ( A \ B ) ) - u ) e. RR+ /\ 3 e. RR+ ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ ) |
61 |
56 59 60
|
sylancl |
|- ( ( ( vol* ` ( A \ B ) ) e. RR /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ ) |
62 |
5 61
|
sylan |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ ) |
63 |
49 62
|
ltsubrpd |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol* ` A ) ) |
64 |
63
|
adantr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol* ` A ) ) |
65 |
|
simpr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) |
66 |
64 65
|
breqtrd |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) |
67 |
|
reex |
|- RR e. _V |
68 |
67
|
ssex |
|- ( A C_ RR -> A e. _V ) |
69 |
68
|
adantr |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> A e. _V ) |
70 |
|
sseq1 |
|- ( v = A -> ( v C_ RR <-> A C_ RR ) ) |
71 |
|
fveq2 |
|- ( v = A -> ( vol* ` v ) = ( vol* ` A ) ) |
72 |
71
|
eleq1d |
|- ( v = A -> ( ( vol* ` v ) e. RR <-> ( vol* ` A ) e. RR ) ) |
73 |
70 72
|
anbi12d |
|- ( v = A -> ( ( v C_ RR /\ ( vol* ` v ) e. RR ) <-> ( A C_ RR /\ ( vol* ` A ) e. RR ) ) ) |
74 |
|
sseq2 |
|- ( v = A -> ( b C_ v <-> b C_ A ) ) |
75 |
74
|
anbi1d |
|- ( v = A -> ( ( b C_ v /\ y = ( vol ` b ) ) <-> ( b C_ A /\ y = ( vol ` b ) ) ) ) |
76 |
75
|
rexbidv |
|- ( v = A -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) ) ) |
77 |
76
|
abbidv |
|- ( v = A -> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } = { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ) |
78 |
77
|
sseq1d |
|- ( v = A -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR <-> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR ) ) |
79 |
77
|
neeq1d |
|- ( v = A -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) <-> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) ) ) |
80 |
77
|
raleqdv |
|- ( v = A -> ( A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x <-> A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) ) |
81 |
80
|
rexbidv |
|- ( v = A -> ( E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x <-> E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) ) |
82 |
78 79 81
|
3anbi123d |
|- ( v = A -> ( ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) <-> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) ) ) |
83 |
73 82
|
imbi12d |
|- ( v = A -> ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) ) <-> ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) ) ) ) |
84 |
|
simpr |
|- ( ( b C_ v /\ y = ( vol ` b ) ) -> y = ( vol ` b ) ) |
85 |
84 36
|
sylan9eqr |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ y = ( vol ` b ) ) ) -> y = ( vol* ` b ) ) |
86 |
85
|
adantl |
|- ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ y = ( vol ` b ) ) ) ) -> y = ( vol* ` b ) ) |
87 |
|
simprl |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ y = ( vol ` b ) ) ) -> b C_ v ) |
88 |
|
ovolsscl |
|- ( ( b C_ v /\ v C_ RR /\ ( vol* ` v ) e. RR ) -> ( vol* ` b ) e. RR ) |
89 |
88
|
3expb |
|- ( ( b C_ v /\ ( v C_ RR /\ ( vol* ` v ) e. RR ) ) -> ( vol* ` b ) e. RR ) |
90 |
89
|
ancoms |
|- ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) /\ b C_ v ) -> ( vol* ` b ) e. RR ) |
91 |
87 90
|
sylan2 |
|- ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ y = ( vol ` b ) ) ) ) -> ( vol* ` b ) e. RR ) |
92 |
86 91
|
eqeltrd |
|- ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ y = ( vol ` b ) ) ) ) -> y e. RR ) |
93 |
92
|
rexlimdvaa |
|- ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) -> y e. RR ) ) |
94 |
93
|
abssdv |
|- ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR ) |
95 |
|
retop |
|- ( topGen ` ran (,) ) e. Top |
96 |
|
0cld |
|- ( ( topGen ` ran (,) ) e. Top -> (/) e. ( Clsd ` ( topGen ` ran (,) ) ) ) |
97 |
95 96
|
ax-mp |
|- (/) e. ( Clsd ` ( topGen ` ran (,) ) ) |
98 |
|
0ss |
|- (/) C_ v |
99 |
|
0mbl |
|- (/) e. dom vol |
100 |
|
mblvol |
|- ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) ) |
101 |
99 100
|
ax-mp |
|- ( vol ` (/) ) = ( vol* ` (/) ) |
102 |
|
ovol0 |
|- ( vol* ` (/) ) = 0 |
103 |
101 102
|
eqtr2i |
|- 0 = ( vol ` (/) ) |
104 |
98 103
|
pm3.2i |
|- ( (/) C_ v /\ 0 = ( vol ` (/) ) ) |
105 |
|
sseq1 |
|- ( b = (/) -> ( b C_ v <-> (/) C_ v ) ) |
106 |
|
fveq2 |
|- ( b = (/) -> ( vol ` b ) = ( vol ` (/) ) ) |
107 |
106
|
eqeq2d |
|- ( b = (/) -> ( 0 = ( vol ` b ) <-> 0 = ( vol ` (/) ) ) ) |
108 |
105 107
|
anbi12d |
|- ( b = (/) -> ( ( b C_ v /\ 0 = ( vol ` b ) ) <-> ( (/) C_ v /\ 0 = ( vol ` (/) ) ) ) ) |
109 |
108
|
rspcev |
|- ( ( (/) e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( (/) C_ v /\ 0 = ( vol ` (/) ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ 0 = ( vol ` b ) ) ) |
110 |
97 104 109
|
mp2an |
|- E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ 0 = ( vol ` b ) ) |
111 |
|
c0ex |
|- 0 e. _V |
112 |
|
eqeq1 |
|- ( y = 0 -> ( y = ( vol ` b ) <-> 0 = ( vol ` b ) ) ) |
113 |
112
|
anbi2d |
|- ( y = 0 -> ( ( b C_ v /\ y = ( vol ` b ) ) <-> ( b C_ v /\ 0 = ( vol ` b ) ) ) ) |
114 |
113
|
rexbidv |
|- ( y = 0 -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ 0 = ( vol ` b ) ) ) ) |
115 |
111 114
|
spcev |
|- ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ 0 = ( vol ` b ) ) -> E. y E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) ) |
116 |
110 115
|
ax-mp |
|- E. y E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) |
117 |
|
abn0 |
|- ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) <-> E. y E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) ) |
118 |
117
|
biimpri |
|- ( E. y E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) -> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) ) |
119 |
116 118
|
mp1i |
|- ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) ) |
120 |
|
simpr |
|- ( ( b C_ v /\ z = ( vol ` b ) ) -> z = ( vol ` b ) ) |
121 |
120 36
|
sylan9eqr |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ z = ( vol ` b ) ) ) -> z = ( vol* ` b ) ) |
122 |
121
|
adantl |
|- ( ( v C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ z = ( vol ` b ) ) ) ) -> z = ( vol* ` b ) ) |
123 |
|
simprl |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ z = ( vol ` b ) ) ) -> b C_ v ) |
124 |
|
ovolss |
|- ( ( b C_ v /\ v C_ RR ) -> ( vol* ` b ) <_ ( vol* ` v ) ) |
125 |
124
|
ancoms |
|- ( ( v C_ RR /\ b C_ v ) -> ( vol* ` b ) <_ ( vol* ` v ) ) |
126 |
123 125
|
sylan2 |
|- ( ( v C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ z = ( vol ` b ) ) ) ) -> ( vol* ` b ) <_ ( vol* ` v ) ) |
127 |
122 126
|
eqbrtrd |
|- ( ( v C_ RR /\ ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ v /\ z = ( vol ` b ) ) ) ) -> z <_ ( vol* ` v ) ) |
128 |
127
|
rexlimdvaa |
|- ( v C_ RR -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ z = ( vol ` b ) ) -> z <_ ( vol* ` v ) ) ) |
129 |
128
|
alrimiv |
|- ( v C_ RR -> A. z ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ z = ( vol ` b ) ) -> z <_ ( vol* ` v ) ) ) |
130 |
|
eqeq1 |
|- ( y = z -> ( y = ( vol ` b ) <-> z = ( vol ` b ) ) ) |
131 |
130
|
anbi2d |
|- ( y = z -> ( ( b C_ v /\ y = ( vol ` b ) ) <-> ( b C_ v /\ z = ( vol ` b ) ) ) ) |
132 |
131
|
rexbidv |
|- ( y = z -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ z = ( vol ` b ) ) ) ) |
133 |
132
|
ralab |
|- ( A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ ( vol* ` v ) <-> A. z ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ z = ( vol ` b ) ) -> z <_ ( vol* ` v ) ) ) |
134 |
129 133
|
sylibr |
|- ( v C_ RR -> A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ ( vol* ` v ) ) |
135 |
|
brralrspcev |
|- ( ( ( vol* ` v ) e. RR /\ A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ ( vol* ` v ) ) -> E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) |
136 |
134 135
|
sylan2 |
|- ( ( ( vol* ` v ) e. RR /\ v C_ RR ) -> E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) |
137 |
136
|
ancoms |
|- ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) |
138 |
94 119 137
|
3jca |
|- ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) ) |
139 |
83 138
|
vtoclg |
|- ( A e. _V -> ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) ) ) |
140 |
69 139
|
mpcom |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) ) |
141 |
140
|
adantr |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) ) |
142 |
62
|
rpred |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR ) |
143 |
49 142
|
resubcld |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) |
144 |
|
suprlub |
|- ( ( ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } z <_ x ) /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) ) |
145 |
141 143 144
|
syl2anc |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) ) |
146 |
145
|
adantr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) ) |
147 |
66 146
|
mpbid |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) |
148 |
|
eqeq1 |
|- ( y = v -> ( y = ( vol ` b ) <-> v = ( vol ` b ) ) ) |
149 |
148
|
anbi2d |
|- ( y = v -> ( ( b C_ A /\ y = ( vol ` b ) ) <-> ( b C_ A /\ v = ( vol ` b ) ) ) ) |
150 |
149
|
rexbidv |
|- ( y = v -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) ) ) |
151 |
150
|
rexab |
|- ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) ) |
152 |
|
breq2 |
|- ( v = ( vol ` b ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) |
153 |
152
|
ad2antll |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) |
154 |
|
sseq1 |
|- ( s = b -> ( s C_ A <-> b C_ A ) ) |
155 |
|
fveq2 |
|- ( s = b -> ( vol ` s ) = ( vol ` b ) ) |
156 |
155
|
breq2d |
|- ( s = b -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) <-> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) |
157 |
154 156
|
anbi12d |
|- ( s = b -> ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) <-> ( b C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) ) |
158 |
157
|
rspcev |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) |
159 |
158
|
expr |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ b C_ A ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) ) |
160 |
159
|
adantrr |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) ) |
161 |
153 160
|
sylbid |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ A /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) ) |
162 |
161
|
rexlimiva |
|- ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) -> ( ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) ) |
163 |
162
|
imp |
|- ( ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) |
164 |
163
|
exlimiv |
|- ( E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ v = ( vol ` b ) ) /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) |
165 |
151 164
|
sylbi |
|- ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) |
166 |
147 165
|
syl |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) |
167 |
166
|
ex |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) ) |
168 |
167
|
adantlr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) ) ) |
169 |
|
simplrr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( vol* ` B ) e. RR ) |
170 |
62
|
adantlr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ ) |
171 |
169 170
|
ltsubrpd |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol* ` B ) ) |
172 |
171
|
adantr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol* ` B ) ) |
173 |
|
simpr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) |
174 |
172 173
|
breqtrd |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) |
175 |
67
|
ssex |
|- ( B C_ RR -> B e. _V ) |
176 |
175
|
adantr |
|- ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> B e. _V ) |
177 |
|
sseq1 |
|- ( v = B -> ( v C_ RR <-> B C_ RR ) ) |
178 |
|
fveq2 |
|- ( v = B -> ( vol* ` v ) = ( vol* ` B ) ) |
179 |
178
|
eleq1d |
|- ( v = B -> ( ( vol* ` v ) e. RR <-> ( vol* ` B ) e. RR ) ) |
180 |
177 179
|
anbi12d |
|- ( v = B -> ( ( v C_ RR /\ ( vol* ` v ) e. RR ) <-> ( B C_ RR /\ ( vol* ` B ) e. RR ) ) ) |
181 |
|
sseq2 |
|- ( v = B -> ( b C_ v <-> b C_ B ) ) |
182 |
181
|
anbi1d |
|- ( v = B -> ( ( b C_ v /\ y = ( vol ` b ) ) <-> ( b C_ B /\ y = ( vol ` b ) ) ) ) |
183 |
182
|
rexbidv |
|- ( v = B -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) ) ) |
184 |
183
|
abbidv |
|- ( v = B -> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } = { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ) |
185 |
184
|
sseq1d |
|- ( v = B -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR <-> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR ) ) |
186 |
184
|
neeq1d |
|- ( v = B -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) <-> { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) ) ) |
187 |
184
|
raleqdv |
|- ( v = B -> ( A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x <-> A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) ) |
188 |
187
|
rexbidv |
|- ( v = B -> ( E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x <-> E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) ) |
189 |
185 186 188
|
3anbi123d |
|- ( v = B -> ( ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) <-> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) ) ) |
190 |
180 189
|
imbi12d |
|- ( v = B -> ( ( ( v C_ RR /\ ( vol* ` v ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ v /\ y = ( vol ` b ) ) } z <_ x ) ) <-> ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) ) ) ) |
191 |
190 138
|
vtoclg |
|- ( B e. _V -> ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) ) ) |
192 |
176 191
|
mpcom |
|- ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) ) |
193 |
192
|
ad2antlr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) ) |
194 |
142
|
adantlr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR ) |
195 |
169 194
|
resubcld |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) |
196 |
|
suprlub |
|- ( ( ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } C_ RR /\ { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } =/= (/) /\ E. x e. RR A. z e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } z <_ x ) /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) ) |
197 |
193 195 196
|
syl2anc |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) ) |
198 |
197
|
adantr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) <-> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) ) |
199 |
174 198
|
mpbid |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) |
200 |
148
|
anbi2d |
|- ( y = v -> ( ( b C_ B /\ y = ( vol ` b ) ) <-> ( b C_ B /\ v = ( vol ` b ) ) ) ) |
201 |
200
|
rexbidv |
|- ( y = v -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ v = ( vol ` b ) ) ) ) |
202 |
201
|
rexab |
|- ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ v = ( vol ` b ) ) /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) ) |
203 |
|
breq2 |
|- ( v = ( vol ` b ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) |
204 |
203
|
ad2antll |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ B /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v <-> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) |
205 |
|
sseq1 |
|- ( w = b -> ( w C_ B <-> b C_ B ) ) |
206 |
|
fveq2 |
|- ( w = b -> ( vol ` w ) = ( vol ` b ) ) |
207 |
206
|
breq2d |
|- ( w = b -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) <-> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) |
208 |
205 207
|
anbi12d |
|- ( w = b -> ( ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) <-> ( b C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) ) |
209 |
208
|
rspcev |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) ) ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) |
210 |
209
|
expr |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ b C_ B ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) |
211 |
210
|
adantrr |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ B /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` b ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) |
212 |
204 211
|
sylbid |
|- ( ( b e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( b C_ B /\ v = ( vol ` b ) ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) |
213 |
212
|
rexlimiva |
|- ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ v = ( vol ` b ) ) -> ( ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) |
214 |
213
|
imp |
|- ( ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ v = ( vol ` b ) ) /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) |
215 |
214
|
exlimiv |
|- ( E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ v = ( vol ` b ) ) /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) |
216 |
202 215
|
sylbi |
|- ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < v -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) |
217 |
199 216
|
syl |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) |
218 |
217
|
ex |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) -> E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) |
219 |
168 218
|
anim12d |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) ) |
220 |
|
reeanv |
|- ( E. s e. ( Clsd ` ( topGen ` ran (,) ) ) E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) <-> ( E. s e. ( Clsd ` ( topGen ` ran (,) ) ) ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) |
221 |
219 220
|
syl6ibr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. s e. ( Clsd ` ( topGen ` ran (,) ) ) E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) ) |
222 |
|
eqid |
|- seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) ) |
223 |
222
|
ovolgelb |
|- ( ( B C_ RR /\ ( vol* ` B ) e. RR /\ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
224 |
223
|
3expa |
|- ( ( ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
225 |
62 224
|
sylan2 |
|- ( ( ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
226 |
225
|
ancoms |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
227 |
226
|
an32s |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
228 |
|
elmapi |
|- ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) ) |
229 |
|
ssid |
|- U. ran ( (,) o. f ) C_ U. ran ( (,) o. f ) |
230 |
222
|
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* , < ) ) |
231 |
229 230
|
mpan2 |
|- ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) |
232 |
231
|
adantl |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ f : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) |
233 |
|
eqid |
|- ( ( abs o. - ) o. f ) = ( ( abs o. - ) o. f ) |
234 |
233 222
|
ovolsf |
|- ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) ) |
235 |
|
frn |
|- ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ ( 0 [,) +oo ) ) |
236 |
|
icossxr |
|- ( 0 [,) +oo ) C_ RR* |
237 |
235 236
|
sstrdi |
|- ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* ) |
238 |
|
supxrcl |
|- ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* ) |
239 |
234 237 238
|
3syl |
|- ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* ) |
240 |
|
simpr |
|- ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` B ) e. RR ) |
241 |
|
readdcl |
|- ( ( ( vol* ` B ) e. RR /\ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR ) -> ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) |
242 |
240 142 241
|
syl2anr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) |
243 |
242
|
rexrd |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR* ) |
244 |
243
|
an32s |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR* ) |
245 |
|
rncoss |
|- ran ( (,) o. f ) C_ ran (,) |
246 |
245
|
unissi |
|- U. ran ( (,) o. f ) C_ U. ran (,) |
247 |
|
unirnioo |
|- RR = U. ran (,) |
248 |
246 247
|
sseqtrri |
|- U. ran ( (,) o. f ) C_ RR |
249 |
|
ovolcl |
|- ( U. ran ( (,) o. f ) C_ RR -> ( vol* ` U. ran ( (,) o. f ) ) e. RR* ) |
250 |
248 249
|
ax-mp |
|- ( vol* ` U. ran ( (,) o. f ) ) e. RR* |
251 |
|
xrletr |
|- ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* /\ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR* ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
252 |
250 251
|
mp3an1 |
|- ( ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* /\ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR* ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
253 |
239 244 252
|
syl2anr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ f : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
254 |
232 253
|
mpand |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ f : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
255 |
228 254
|
sylan2 |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
256 |
255
|
anim2d |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) ) |
257 |
256
|
reximdva |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) ) |
258 |
227 257
|
mpd |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
259 |
|
rexex |
|- ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> E. f ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
260 |
258 259
|
syl |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> E. f ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
261 |
16
|
cldss |
|- ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> s C_ RR ) |
262 |
|
indif2 |
|- ( s i^i ( RR \ U. ran ( (,) o. f ) ) ) = ( ( s i^i RR ) \ U. ran ( (,) o. f ) ) |
263 |
|
df-ss |
|- ( s C_ RR <-> ( s i^i RR ) = s ) |
264 |
263
|
biimpi |
|- ( s C_ RR -> ( s i^i RR ) = s ) |
265 |
264
|
difeq1d |
|- ( s C_ RR -> ( ( s i^i RR ) \ U. ran ( (,) o. f ) ) = ( s \ U. ran ( (,) o. f ) ) ) |
266 |
262 265
|
syl5eq |
|- ( s C_ RR -> ( s i^i ( RR \ U. ran ( (,) o. f ) ) ) = ( s \ U. ran ( (,) o. f ) ) ) |
267 |
261 266
|
syl |
|- ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s i^i ( RR \ U. ran ( (,) o. f ) ) ) = ( s \ U. ran ( (,) o. f ) ) ) |
268 |
|
retopbas |
|- ran (,) e. TopBases |
269 |
|
bastg |
|- ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) ) |
270 |
268 269
|
ax-mp |
|- ran (,) C_ ( topGen ` ran (,) ) |
271 |
245 270
|
sstri |
|- ran ( (,) o. f ) C_ ( topGen ` ran (,) ) |
272 |
|
uniopn |
|- ( ( ( topGen ` ran (,) ) e. Top /\ ran ( (,) o. f ) C_ ( topGen ` ran (,) ) ) -> U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) ) |
273 |
95 271 272
|
mp2an |
|- U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) |
274 |
16
|
opncld |
|- ( ( ( topGen ` ran (,) ) e. Top /\ U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) ) -> ( RR \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) |
275 |
95 273 274
|
mp2an |
|- ( RR \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) |
276 |
|
incld |
|- ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( RR \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( s i^i ( RR \ U. ran ( (,) o. f ) ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) |
277 |
275 276
|
mpan2 |
|- ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s i^i ( RR \ U. ran ( (,) o. f ) ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) |
278 |
267 277
|
eqeltrrd |
|- ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) |
279 |
278
|
adantr |
|- ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) |
280 |
279
|
ad2antlr |
|- ( ( ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) |
281 |
|
simprll |
|- ( ( ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> s C_ A ) |
282 |
|
simplll |
|- ( ( ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> B C_ U. ran ( (,) o. f ) ) |
283 |
281 282
|
ssdif2d |
|- ( ( ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) ) |
284 |
|
fveq2 |
|- ( ( s \ U. ran ( (,) o. f ) ) = b -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) |
285 |
284
|
eqcoms |
|- ( b = ( s \ U. ran ( (,) o. f ) ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) |
286 |
285
|
biantrud |
|- ( b = ( s \ U. ran ( (,) o. f ) ) -> ( b C_ ( A \ B ) <-> ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) ) ) |
287 |
|
sseq1 |
|- ( b = ( s \ U. ran ( (,) o. f ) ) -> ( b C_ ( A \ B ) <-> ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) ) ) |
288 |
286 287
|
bitr3d |
|- ( b = ( s \ U. ran ( (,) o. f ) ) -> ( ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) <-> ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) ) ) |
289 |
288
|
rspcev |
|- ( ( ( s \ U. ran ( (,) o. f ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) ) |
290 |
280 283 289
|
syl2anc |
|- ( ( ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) ) |
291 |
290
|
adantlll |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) ) |
292 |
|
difss |
|- ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) C_ ( A \ B ) |
293 |
292 3
|
sstri |
|- ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) C_ A |
294 |
|
ovolsscl |
|- ( ( ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) e. RR ) |
295 |
293 294
|
mp3an1 |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) e. RR ) |
296 |
295
|
ad5antr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) e. RR ) |
297 |
5
|
ad5antr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A \ B ) ) e. RR ) |
298 |
|
simpl |
|- ( ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) -> u e. RR ) |
299 |
298
|
ad4antlr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> u e. RR ) |
300 |
|
difdif2 |
|- ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) = ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) |
301 |
300
|
fveq2i |
|- ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) = ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) |
302 |
|
difss |
|- ( ( A \ B ) \ s ) C_ ( A \ B ) |
303 |
302 3
|
sstri |
|- ( ( A \ B ) \ s ) C_ A |
304 |
|
inss1 |
|- ( ( A \ B ) i^i U. ran ( (,) o. f ) ) C_ ( A \ B ) |
305 |
304 3
|
sstri |
|- ( ( A \ B ) i^i U. ran ( (,) o. f ) ) C_ A |
306 |
303 305
|
unssi |
|- ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) C_ A |
307 |
|
ovolsscl |
|- ( ( ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) e. RR ) |
308 |
306 307
|
mp3an1 |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) e. RR ) |
309 |
308
|
ad5antr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) e. RR ) |
310 |
|
difss |
|- ( A \ s ) C_ A |
311 |
|
ovolsscl |
|- ( ( ( A \ s ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ s ) ) e. RR ) |
312 |
310 311
|
mp3an1 |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ s ) ) e. RR ) |
313 |
312
|
ad5antr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A \ s ) ) e. RR ) |
314 |
169 194
|
readdcld |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) |
315 |
314 250
|
jctil |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) ) |
316 |
|
simpr |
|- ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) |
317 |
|
ovolge0 |
|- ( U. ran ( (,) o. f ) C_ RR -> 0 <_ ( vol* ` U. ran ( (,) o. f ) ) ) |
318 |
248 317
|
ax-mp |
|- 0 <_ ( vol* ` U. ran ( (,) o. f ) ) |
319 |
316 318
|
jctil |
|- ( ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) -> ( 0 <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
320 |
|
xrrege0 |
|- ( ( ( ( vol* ` U. ran ( (,) o. f ) ) e. RR* /\ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) /\ ( 0 <_ ( vol* ` U. ran ( (,) o. f ) ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. RR ) |
321 |
315 319 320
|
syl2an |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. RR ) |
322 |
|
difss |
|- ( U. ran ( (,) o. f ) \ w ) C_ U. ran ( (,) o. f ) |
323 |
|
ovolsscl |
|- ( ( ( U. ran ( (,) o. f ) \ w ) C_ U. ran ( (,) o. f ) /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR ) |
324 |
322 248 323
|
mp3an12 |
|- ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR ) |
325 |
321 324
|
syl |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR ) |
326 |
325
|
ad2antrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR ) |
327 |
313 326
|
readdcld |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) e. RR ) |
328 |
5 50
|
sylan |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ u e. RR ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR ) |
329 |
328
|
adantrr |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR ) |
330 |
329
|
adantlr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR ) |
331 |
330
|
ad3antrrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. RR ) |
332 |
|
ssdifss |
|- ( A C_ RR -> ( A \ s ) C_ RR ) |
333 |
322 248
|
sstri |
|- ( U. ran ( (,) o. f ) \ w ) C_ RR |
334 |
|
unss |
|- ( ( ( A \ s ) C_ RR /\ ( U. ran ( (,) o. f ) \ w ) C_ RR ) <-> ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR ) |
335 |
332 333 334
|
sylanblc |
|- ( A C_ RR -> ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR ) |
336 |
|
ovolcl |
|- ( ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR* ) |
337 |
335 336
|
syl |
|- ( A C_ RR -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR* ) |
338 |
337
|
ad4antr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR* ) |
339 |
312
|
ad3antrrr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( A \ s ) ) e. RR ) |
340 |
339 325
|
readdcld |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) e. RR ) |
341 |
|
ovolge0 |
|- ( ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR -> 0 <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) ) |
342 |
335 341
|
syl |
|- ( A C_ RR -> 0 <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) ) |
343 |
342
|
ad4antr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> 0 <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) ) |
344 |
332
|
adantr |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( A \ s ) C_ RR ) |
345 |
344 312
|
jca |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( A \ s ) C_ RR /\ ( vol* ` ( A \ s ) ) e. RR ) ) |
346 |
345
|
ad3antrrr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( A \ s ) C_ RR /\ ( vol* ` ( A \ s ) ) e. RR ) ) |
347 |
325 333
|
jctil |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( U. ran ( (,) o. f ) \ w ) C_ RR /\ ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR ) ) |
348 |
|
ovolun |
|- ( ( ( ( A \ s ) C_ RR /\ ( vol* ` ( A \ s ) ) e. RR ) /\ ( ( U. ran ( (,) o. f ) \ w ) C_ RR /\ ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) ) |
349 |
346 347 348
|
syl2anc |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) ) |
350 |
|
xrrege0 |
|- ( ( ( ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR* /\ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) e. RR ) /\ ( 0 <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) /\ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR ) |
351 |
338 340 343 349 350
|
syl22anc |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR ) |
352 |
351
|
ad2antrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) e. RR ) |
353 |
|
ssdif |
|- ( ( A \ B ) C_ A -> ( ( A \ B ) \ s ) C_ ( A \ s ) ) |
354 |
3 353
|
ax-mp |
|- ( ( A \ B ) \ s ) C_ ( A \ s ) |
355 |
|
incom |
|- ( ( A \ B ) i^i U. ran ( (,) o. f ) ) = ( U. ran ( (,) o. f ) i^i ( A \ B ) ) |
356 |
|
indif2 |
|- ( U. ran ( (,) o. f ) i^i ( A \ B ) ) = ( ( U. ran ( (,) o. f ) i^i A ) \ B ) |
357 |
355 356
|
eqtri |
|- ( ( A \ B ) i^i U. ran ( (,) o. f ) ) = ( ( U. ran ( (,) o. f ) i^i A ) \ B ) |
358 |
|
inss1 |
|- ( U. ran ( (,) o. f ) i^i A ) C_ U. ran ( (,) o. f ) |
359 |
358
|
a1i |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( U. ran ( (,) o. f ) i^i A ) C_ U. ran ( (,) o. f ) ) |
360 |
|
simprrl |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> w C_ B ) |
361 |
359 360
|
ssdif2d |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( U. ran ( (,) o. f ) i^i A ) \ B ) C_ ( U. ran ( (,) o. f ) \ w ) ) |
362 |
357 361
|
eqsstrid |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( A \ B ) i^i U. ran ( (,) o. f ) ) C_ ( U. ran ( (,) o. f ) \ w ) ) |
363 |
|
unss12 |
|- ( ( ( ( A \ B ) \ s ) C_ ( A \ s ) /\ ( ( A \ B ) i^i U. ran ( (,) o. f ) ) C_ ( U. ran ( (,) o. f ) \ w ) ) -> ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) C_ ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) |
364 |
354 362 363
|
sylancr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) C_ ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) |
365 |
335
|
ad6antr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR ) |
366 |
|
ovolss |
|- ( ( ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) C_ ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) /\ ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) C_ RR ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) ) |
367 |
364 365 366
|
syl2anc |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) <_ ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) ) |
368 |
332
|
ad6antr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( A \ s ) C_ RR ) |
369 |
326 333
|
jctil |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( U. ran ( (,) o. f ) \ w ) C_ RR /\ ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. RR ) ) |
370 |
368 313 369 348
|
syl21anc |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ s ) u. ( U. ran ( (,) o. f ) \ w ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) ) |
371 |
309 352 327 367 370
|
letrd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) <_ ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) ) |
372 |
194
|
ad3antrrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR ) |
373 |
194 194
|
readdcld |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) |
374 |
373
|
ad3antrrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) e. RR ) |
375 |
|
eleq1w |
|- ( b = s -> ( b e. dom vol <-> s e. dom vol ) ) |
376 |
375 34
|
vtoclga |
|- ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> s e. dom vol ) |
377 |
|
mblvol |
|- ( s e. dom vol -> ( vol ` s ) = ( vol* ` s ) ) |
378 |
376 377
|
syl |
|- ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` s ) = ( vol* ` s ) ) |
379 |
378
|
adantr |
|- ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( vol ` s ) = ( vol* ` s ) ) |
380 |
|
sseqin2 |
|- ( s C_ A <-> ( A i^i s ) = s ) |
381 |
380
|
biimpi |
|- ( s C_ A -> ( A i^i s ) = s ) |
382 |
381
|
eqcomd |
|- ( s C_ A -> s = ( A i^i s ) ) |
383 |
382
|
fveq2d |
|- ( s C_ A -> ( vol* ` s ) = ( vol* ` ( A i^i s ) ) ) |
384 |
383
|
ad2antrr |
|- ( ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> ( vol* ` s ) = ( vol* ` ( A i^i s ) ) ) |
385 |
379 384
|
sylan9eq |
|- ( ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` s ) = ( vol* ` ( A i^i s ) ) ) |
386 |
385
|
oveq2d |
|- ( ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( vol ` s ) ) = ( ( vol* ` A ) - ( vol* ` ( A i^i s ) ) ) ) |
387 |
386
|
adantll |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( vol ` s ) ) = ( ( vol* ` A ) - ( vol* ` ( A i^i s ) ) ) ) |
388 |
376
|
adantr |
|- ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> s e. dom vol ) |
389 |
|
simplll |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( A C_ RR /\ ( vol* ` A ) e. RR ) ) |
390 |
|
mblsplit |
|- ( ( s e. dom vol /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` A ) = ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) ) |
391 |
390
|
eqcomd |
|- ( ( s e. dom vol /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) = ( vol* ` A ) ) |
392 |
391
|
3expb |
|- ( ( s e. dom vol /\ ( A C_ RR /\ ( vol* ` A ) e. RR ) ) -> ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) = ( vol* ` A ) ) |
393 |
388 389 392
|
syl2anr |
|- ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) = ( vol* ` A ) ) |
394 |
393
|
adantr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) = ( vol* ` A ) ) |
395 |
|
simp-6r |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` A ) e. RR ) |
396 |
395
|
recnd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` A ) e. CC ) |
397 |
|
inss1 |
|- ( A i^i s ) C_ A |
398 |
|
ovolsscl |
|- ( ( ( A i^i s ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i s ) ) e. RR ) |
399 |
397 398
|
mp3an1 |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i s ) ) e. RR ) |
400 |
399
|
recnd |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i s ) ) e. CC ) |
401 |
400
|
ad5antr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A i^i s ) ) e. CC ) |
402 |
312
|
recnd |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ s ) ) e. CC ) |
403 |
402
|
ad5antr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A \ s ) ) e. CC ) |
404 |
396 401 403
|
subaddd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` A ) - ( vol* ` ( A i^i s ) ) ) = ( vol* ` ( A \ s ) ) <-> ( ( vol* ` ( A i^i s ) ) + ( vol* ` ( A \ s ) ) ) = ( vol* ` A ) ) ) |
405 |
394 404
|
mpbird |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( vol* ` ( A i^i s ) ) ) = ( vol* ` ( A \ s ) ) ) |
406 |
387 405
|
eqtrd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( vol ` s ) ) = ( vol* ` ( A \ s ) ) ) |
407 |
379
|
ad2antlr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` s ) = ( vol* ` s ) ) |
408 |
|
simpll |
|- ( ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> s C_ A ) |
409 |
|
simp-4l |
|- ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( A C_ RR /\ ( vol* ` A ) e. RR ) ) |
410 |
|
ovolsscl |
|- ( ( s C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` s ) e. RR ) |
411 |
410
|
3expb |
|- ( ( s C_ A /\ ( A C_ RR /\ ( vol* ` A ) e. RR ) ) -> ( vol* ` s ) e. RR ) |
412 |
408 409 411
|
syl2anr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` s ) e. RR ) |
413 |
407 412
|
eqeltrd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` s ) e. RR ) |
414 |
|
simprlr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) |
415 |
395 372 413 414
|
ltsub23d |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` A ) - ( vol ` s ) ) < ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) |
416 |
406 415
|
eqbrtrrd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A \ s ) ) < ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) |
417 |
321
|
recnd |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. CC ) |
418 |
417
|
ad2antrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) e. CC ) |
419 |
240
|
ad5antlr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` B ) e. RR ) |
420 |
419
|
recnd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` B ) e. CC ) |
421 |
|
eleq1w |
|- ( b = w -> ( b e. dom vol <-> w e. dom vol ) ) |
422 |
421 34
|
vtoclga |
|- ( w e. ( Clsd ` ( topGen ` ran (,) ) ) -> w e. dom vol ) |
423 |
|
mblvol |
|- ( w e. dom vol -> ( vol ` w ) = ( vol* ` w ) ) |
424 |
422 423
|
syl |
|- ( w e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` w ) = ( vol* ` w ) ) |
425 |
424
|
adantl |
|- ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( vol ` w ) = ( vol* ` w ) ) |
426 |
425
|
ad2antlr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` w ) = ( vol* ` w ) ) |
427 |
|
simprl |
|- ( ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> w C_ B ) |
428 |
|
simp-4r |
|- ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( B C_ RR /\ ( vol* ` B ) e. RR ) ) |
429 |
|
ovolsscl |
|- ( ( w C_ B /\ B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` w ) e. RR ) |
430 |
429
|
3expb |
|- ( ( w C_ B /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` w ) e. RR ) |
431 |
427 428 430
|
syl2anr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` w ) e. RR ) |
432 |
426 431
|
eqeltrd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` w ) e. RR ) |
433 |
432
|
recnd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` w ) e. CC ) |
434 |
418 420 433
|
npncand |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) + ( ( vol* ` B ) - ( vol ` w ) ) ) = ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol ` w ) ) ) |
435 |
|
simplrl |
|- ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> B C_ U. ran ( (,) o. f ) ) |
436 |
427 435
|
sylan9ssr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> w C_ U. ran ( (,) o. f ) ) |
437 |
|
sseqin2 |
|- ( w C_ U. ran ( (,) o. f ) <-> ( U. ran ( (,) o. f ) i^i w ) = w ) |
438 |
436 437
|
sylib |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( U. ran ( (,) o. f ) i^i w ) = w ) |
439 |
438
|
fveq2d |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) = ( vol* ` w ) ) |
440 |
426 439
|
eqtr4d |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` w ) = ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) ) |
441 |
440
|
oveq2d |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol ` w ) ) = ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) ) ) |
442 |
422
|
adantl |
|- ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> w e. dom vol ) |
443 |
321 248
|
jctil |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) ) |
444 |
|
mblsplit |
|- ( ( w e. dom vol /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( vol* ` U. ran ( (,) o. f ) ) = ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) ) |
445 |
444
|
eqcomd |
|- ( ( w e. dom vol /\ U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) -> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) ) |
446 |
445
|
3expb |
|- ( ( w e. dom vol /\ ( U. ran ( (,) o. f ) C_ RR /\ ( vol* ` U. ran ( (,) o. f ) ) e. RR ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) ) |
447 |
442 443 446
|
syl2anr |
|- ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) ) |
448 |
447
|
adantr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) ) |
449 |
|
inss1 |
|- ( U. ran ( (,) o. f ) i^i w ) C_ U. ran ( (,) o. f ) |
450 |
|
ovolsscl |
|- ( ( ( U. ran ( (,) o. f ) i^i w ) 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 w ) ) e. RR ) |
451 |
449 248 450
|
mp3an12 |
|- ( ( vol* ` U. ran ( (,) o. f ) ) e. RR -> ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) e. RR ) |
452 |
321 451
|
syl |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) e. RR ) |
453 |
452
|
recnd |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) e. CC ) |
454 |
325
|
recnd |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) e. CC ) |
455 |
417 453 454
|
subaddd |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) <-> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) ) ) |
456 |
455
|
ad2antrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) <-> ( ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) = ( vol* ` U. ran ( (,) o. f ) ) ) ) |
457 |
448 456
|
mpbird |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` ( U. ran ( (,) o. f ) i^i w ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) |
458 |
434 441 457
|
3eqtrd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) + ( ( vol* ` B ) - ( vol ` w ) ) ) = ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) |
459 |
240
|
ad3antlr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` B ) e. RR ) |
460 |
321 459
|
resubcld |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) e. RR ) |
461 |
460
|
ad2antrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) e. RR ) |
462 |
419 432
|
resubcld |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` B ) - ( vol ` w ) ) e. RR ) |
463 |
|
simprr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) |
464 |
194
|
adantr |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. RR ) |
465 |
321 459 464
|
lesubadd2d |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) <_ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) <-> ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
466 |
463 465
|
mpbird |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) <_ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) |
467 |
466
|
ad2antrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) <_ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) |
468 |
|
simprrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) |
469 |
419 372 432 468
|
ltsub23d |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` B ) - ( vol ` w ) ) < ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) |
470 |
461 462 372 372 467 469
|
leltaddd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` U. ran ( (,) o. f ) ) - ( vol* ` B ) ) + ( ( vol* ` B ) - ( vol ` w ) ) ) < ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) |
471 |
458 470
|
eqbrtrrd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) < ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) |
472 |
313 326 372 374 416 471
|
lt2addd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) < ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
473 |
|
df-3 |
|- 3 = ( 2 + 1 ) |
474 |
|
2cn |
|- 2 e. CC |
475 |
|
ax-1cn |
|- 1 e. CC |
476 |
474 475
|
addcomi |
|- ( 2 + 1 ) = ( 1 + 2 ) |
477 |
473 476
|
eqtri |
|- 3 = ( 1 + 2 ) |
478 |
477
|
oveq1i |
|- ( 3 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( 1 + 2 ) x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) |
479 |
62
|
rpcnd |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. CC ) |
480 |
|
adddir |
|- ( ( 1 e. CC /\ 2 e. CC /\ ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. CC ) -> ( ( 1 + 2 ) x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( 1 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) + ( 2 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
481 |
475 474 480
|
mp3an12 |
|- ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) e. CC -> ( ( 1 + 2 ) x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( 1 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) + ( 2 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
482 |
479 481
|
syl |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( 1 + 2 ) x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( 1 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) + ( 2 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
483 |
479
|
mulid2d |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( 1 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) |
484 |
479
|
2timesd |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( 2 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) |
485 |
483 484
|
oveq12d |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( 1 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) + ( 2 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) = ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
486 |
482 485
|
eqtrd |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( 1 + 2 ) x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
487 |
478 486
|
syl5eq |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( 3 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) |
488 |
329
|
recnd |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - u ) e. CC ) |
489 |
|
3cn |
|- 3 e. CC |
490 |
|
3ne0 |
|- 3 =/= 0 |
491 |
|
divcan2 |
|- ( ( ( ( vol* ` ( A \ B ) ) - u ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( 3 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( vol* ` ( A \ B ) ) - u ) ) |
492 |
489 490 491
|
mp3an23 |
|- ( ( ( vol* ` ( A \ B ) ) - u ) e. CC -> ( 3 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( vol* ` ( A \ B ) ) - u ) ) |
493 |
488 492
|
syl |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( 3 x. ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) = ( ( vol* ` ( A \ B ) ) - u ) ) |
494 |
487 493
|
eqtr3d |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) = ( ( vol* ` ( A \ B ) ) - u ) ) |
495 |
494
|
adantlr |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) = ( ( vol* ` ( A \ B ) ) - u ) ) |
496 |
495
|
ad3antrrr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) = ( ( vol* ` ( A \ B ) ) - u ) ) |
497 |
472 496
|
breqtrd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A \ s ) ) + ( vol* ` ( U. ran ( (,) o. f ) \ w ) ) ) < ( ( vol* ` ( A \ B ) ) - u ) ) |
498 |
309 327 331 371 497
|
lelttrd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( ( A \ B ) \ s ) u. ( ( A \ B ) i^i U. ran ( (,) o. f ) ) ) ) < ( ( vol* ` ( A \ B ) ) - u ) ) |
499 |
301 498
|
eqbrtrid |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) < ( ( vol* ` ( A \ B ) ) - u ) ) |
500 |
296 297 299 499
|
ltsub13d |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> u < ( ( vol* ` ( A \ B ) ) - ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) ) |
501 |
283
|
adantlll |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) ) |
502 |
|
sseqin2 |
|- ( ( s \ U. ran ( (,) o. f ) ) C_ ( A \ B ) <-> ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) = ( s \ U. ran ( (,) o. f ) ) ) |
503 |
501 502
|
sylib |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) = ( s \ U. ran ( (,) o. f ) ) ) |
504 |
503
|
fveq2d |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) ) |
505 |
|
opnmbl |
|- ( U. ran ( (,) o. f ) e. ( topGen ` ran (,) ) -> U. ran ( (,) o. f ) e. dom vol ) |
506 |
273 505
|
ax-mp |
|- U. ran ( (,) o. f ) e. dom vol |
507 |
|
difmbl |
|- ( ( s e. dom vol /\ U. ran ( (,) o. f ) e. dom vol ) -> ( s \ U. ran ( (,) o. f ) ) e. dom vol ) |
508 |
376 506 507
|
sylancl |
|- ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. dom vol ) |
509 |
508
|
adantr |
|- ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. dom vol ) |
510 |
509
|
ad2antlr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( s \ U. ran ( (,) o. f ) ) e. dom vol ) |
511 |
13
|
adantr |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( A \ B ) C_ RR ) |
512 |
511 5
|
jca |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) ) |
513 |
512
|
ad5antr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) ) |
514 |
|
mblsplit |
|- ( ( ( s \ U. ran ( (,) o. f ) ) e. dom vol /\ ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) -> ( vol* ` ( A \ B ) ) = ( ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) + ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) ) |
515 |
514
|
3expb |
|- ( ( ( s \ U. ran ( (,) o. f ) ) e. dom vol /\ ( ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) ) -> ( vol* ` ( A \ B ) ) = ( ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) + ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) ) |
516 |
515
|
eqcomd |
|- ( ( ( s \ U. ran ( (,) o. f ) ) e. dom vol /\ ( ( A \ B ) C_ RR /\ ( vol* ` ( A \ B ) ) e. RR ) ) -> ( ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) + ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) = ( vol* ` ( A \ B ) ) ) |
517 |
510 513 516
|
syl2anc |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) + ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) = ( vol* ` ( A \ B ) ) ) |
518 |
297
|
recnd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( A \ B ) ) e. CC ) |
519 |
296
|
recnd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) e. CC ) |
520 |
|
inss1 |
|- ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) C_ ( A \ B ) |
521 |
520 3
|
sstri |
|- ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) C_ A |
522 |
|
ovolsscl |
|- ( ( ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) e. RR ) |
523 |
521 522
|
mp3an1 |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) e. RR ) |
524 |
523
|
ad5antr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) e. RR ) |
525 |
524
|
recnd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) e. CC ) |
526 |
518 519 525
|
subadd2d |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( ( vol* ` ( A \ B ) ) - ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) = ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) <-> ( ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) + ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) = ( vol* ` ( A \ B ) ) ) ) |
527 |
517 526
|
mpbird |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( ( vol* ` ( A \ B ) ) - ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) = ( vol* ` ( ( A \ B ) i^i ( s \ U. ran ( (,) o. f ) ) ) ) ) |
528 |
|
mblvol |
|- ( ( s \ U. ran ( (,) o. f ) ) e. dom vol -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) ) |
529 |
507 528
|
syl |
|- ( ( s e. dom vol /\ U. ran ( (,) o. f ) e. dom vol ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) ) |
530 |
376 506 529
|
sylancl |
|- ( s e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) ) |
531 |
530
|
adantr |
|- ( ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) ) |
532 |
531
|
ad2antlr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol* ` ( s \ U. ran ( (,) o. f ) ) ) ) |
533 |
504 527 532
|
3eqtr4rd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( ( vol* ` ( A \ B ) ) - ( vol* ` ( ( A \ B ) \ ( s \ U. ran ( (,) o. f ) ) ) ) ) ) |
534 |
500 533
|
breqtrrd |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> u < ( vol ` ( s \ U. ran ( (,) o. f ) ) ) ) |
535 |
|
fvex |
|- ( vol ` ( s \ U. ran ( (,) o. f ) ) ) e. _V |
536 |
|
eqeq1 |
|- ( v = ( vol ` ( s \ U. ran ( (,) o. f ) ) ) -> ( v = ( vol ` b ) <-> ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) ) |
537 |
536
|
anbi2d |
|- ( v = ( vol ` ( s \ U. ran ( (,) o. f ) ) ) -> ( ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) <-> ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) ) ) |
538 |
537
|
rexbidv |
|- ( v = ( vol ` ( s \ U. ran ( (,) o. f ) ) ) -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) ) ) |
539 |
|
breq2 |
|- ( v = ( vol ` ( s \ U. ran ( (,) o. f ) ) ) -> ( u < v <-> u < ( vol ` ( s \ U. ran ( (,) o. f ) ) ) ) ) |
540 |
538 539
|
anbi12d |
|- ( v = ( vol ` ( s \ U. ran ( (,) o. f ) ) ) -> ( ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) /\ u < v ) <-> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) /\ u < ( vol ` ( s \ U. ran ( (,) o. f ) ) ) ) ) ) |
541 |
535 540
|
spcev |
|- ( ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ ( vol ` ( s \ U. ran ( (,) o. f ) ) ) = ( vol ` b ) ) /\ u < ( vol ` ( s \ U. ran ( (,) o. f ) ) ) ) -> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) /\ u < v ) ) |
542 |
291 534 541
|
syl2anc |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) /\ u < v ) ) |
543 |
148
|
anbi2d |
|- ( y = v -> ( ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) <-> ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) ) ) |
544 |
543
|
rexbidv |
|- ( y = v -> ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) <-> E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) ) ) |
545 |
544
|
rexab |
|- ( E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v <-> E. v ( E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ v = ( vol ` b ) ) /\ u < v ) ) |
546 |
542 545
|
sylibr |
|- ( ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) /\ ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) |
547 |
546
|
ex |
|- ( ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) /\ ( s e. ( Clsd ` ( topGen ` ran (,) ) ) /\ w e. ( Clsd ` ( topGen ` ran (,) ) ) ) ) -> ( ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) ) |
548 |
547
|
rexlimdvva |
|- ( ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) /\ ( B C_ U. ran ( (,) o. f ) /\ ( vol* ` U. ran ( (,) o. f ) ) <_ ( ( vol* ` B ) + ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) ) ) -> ( E. s e. ( Clsd ` ( topGen ` ran (,) ) ) E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) ) |
549 |
260 548
|
exlimddv |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( E. s e. ( Clsd ` ( topGen ` ran (,) ) ) E. w e. ( Clsd ` ( topGen ` ran (,) ) ) ( ( s C_ A /\ ( ( vol* ` A ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` s ) ) /\ ( w C_ B /\ ( ( vol* ` B ) - ( ( ( vol* ` ( A \ B ) ) - u ) / 3 ) ) < ( vol ` w ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) ) |
550 |
221 549
|
syld |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> ( ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) ) |
551 |
550
|
exp31 |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) -> ( ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) ) ) ) |
552 |
551
|
com34 |
|- ( ( A C_ RR /\ ( vol* ` A ) e. RR ) -> ( ( B C_ RR /\ ( vol* ` B ) e. RR ) -> ( ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) -> ( ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) ) ) ) |
553 |
552
|
3imp1 |
|- ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) /\ ( u e. RR /\ u < ( vol* ` ( A \ B ) ) ) ) -> E. v e. { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } u < v ) |
554 |
2 6 48 553
|
eqsupd |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) /\ ( ( vol* ` A ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ A /\ y = ( vol ` b ) ) } , RR , < ) /\ ( vol* ` B ) = sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ B /\ y = ( vol ` b ) ) } , RR , < ) ) ) -> sup ( { y | E. b e. ( Clsd ` ( topGen ` ran (,) ) ) ( b C_ ( A \ B ) /\ y = ( vol ` b ) ) } , RR , < ) = ( vol* ` ( A \ B ) ) ) |