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