Step | Hyp | Ref
| Expression |
1 | | mblfinlem4 33449 |
. 2
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ 𝐴 ∈ dom
vol) → (vol*‘𝐴)
= sup({𝑦 ∣
∃𝑏 ∈
(Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) |
2 | | elpwi 4168 |
. . . . 5
⊢ (𝑤 ∈ 𝒫 ℝ →
𝑤 ⊆
ℝ) |
3 | | elmapi 7879 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
4 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∩ 𝐴) ⊆ 𝑤 |
5 | | ovolsscl 23254 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∩ 𝐴) ⊆ 𝑤 ∧ 𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) →
(vol*‘(𝑤 ∩ 𝐴)) ∈
ℝ) |
6 | 4, 5 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) → (vol*‘(𝑤 ∩ 𝐴)) ∈ ℝ) |
7 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∖ 𝐴) ⊆ 𝑤 |
8 | | ovolsscl 23254 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 ∖ 𝐴) ⊆ 𝑤 ∧ 𝑤 ⊆ ℝ ∧ (vol*‘𝑤) ∈ ℝ) →
(vol*‘(𝑤 ∖
𝐴)) ∈
ℝ) |
9 | 7, 8 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) → (vol*‘(𝑤 ∖ 𝐴)) ∈ ℝ) |
10 | 6, 9 | readdcld 10069 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈ ℝ) |
11 | 10 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈
ℝ*) |
12 | 11 | ad3antlr 767 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈
ℝ*) |
13 | | rncoss 5386 |
. . . . . . . . . . . . . . . . . . 19
⊢ ran ((,)
∘ 𝑓) ⊆ ran
(,) |
14 | 13 | unissi 4461 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran
(,) |
15 | | unirnioo 12273 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ =
∪ ran (,) |
16 | 14, 15 | sseqtr4i 3638 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ |
17 | | ovolcl 23246 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ ran ((,) ∘ 𝑓) ⊆ ℝ → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈
ℝ*) |
18 | 16, 17 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈
ℝ*) |
19 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((abs
∘ − ) ∘ 𝑓) = ((abs ∘ − ) ∘ 𝑓) |
20 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
21 | 19, 20 | ovolsf 23241 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝑓)):ℕ⟶(0[,)+∞)) |
22 | | frn 6053 |
. . . . . . . . . . . . . . . . . . 19
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) → ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ (0[,)+∞)) |
23 | | icossxr 12258 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0[,)+∞) ⊆ ℝ* |
24 | 22, 23 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . 18
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) → ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆
ℝ*) |
25 | | supxrcl 12145 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ* → sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈
ℝ*) |
26 | 21, 24, 25 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ) ∈ ℝ*) |
27 | 26 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) → sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < ) ∈ ℝ*) |
28 | | pnfge 11964 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((vol*‘(𝑤
∩ 𝐴)) +
(vol*‘(𝑤 ∖
𝐴))) ∈
ℝ* → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ +∞) |
29 | 11, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ +∞) |
30 | 29 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) = +∞) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ +∞) |
31 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) = +∞) → (vol*‘∪ ran ((,) ∘ 𝑓)) = +∞) |
32 | 30, 31 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) = +∞) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
33 | 32 | adantlll 754 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) = +∞) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
34 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(vol*‘∪ ran ((,) ∘ 𝑓)) ∈
ℝ* |
35 | | nltpnft 11995 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ*
→ ((vol*‘∪ ran ((,) ∘ 𝑓)) = +∞ ↔ ¬
(vol*‘∪ ran ((,) ∘ 𝑓)) < +∞)) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) = +∞ ↔ ¬
(vol*‘∪ ran ((,) ∘ 𝑓)) < +∞) |
37 | 36 | necon2abii 2844 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) < +∞ ↔
(vol*‘∪ ran ((,) ∘ 𝑓)) ≠ +∞) |
38 | | ovolge0 23249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∪ ran ((,) ∘ 𝑓) ⊆ ℝ → 0 ≤
(vol*‘∪ ran ((,) ∘ 𝑓))) |
39 | 16, 38 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ≤
(vol*‘∪ ran ((,) ∘ 𝑓)) |
40 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℝ |
41 | | xrre3 12002 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ*
∧ 0 ∈ ℝ) ∧ (0 ≤ (vol*‘∪
ran ((,) ∘ 𝑓)) ∧
(vol*‘∪ ran ((,) ∘ 𝑓)) < +∞)) → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) |
42 | 34, 40, 41 | mpanl12 718 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0 ≤
(vol*‘∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) < +∞) → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) |
43 | 39, 42 | mpan 706 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) < +∞ →
(vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) |
44 | 37, 43 | sylbir 225 |
. . . . . . . . . . . . . . . . . . 19
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ≠ +∞ →
(vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) |
45 | 10 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈ ℝ) |
46 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) → 𝑧 = (vol‘𝑎)) |
47 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 = 𝑎 → (𝑏 ∈ dom vol ↔ 𝑎 ∈ dom vol)) |
48 | | uniretop 22566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ℝ =
∪ (topGen‘ran (,)) |
49 | 48 | cldss 20833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑏 ∈
(Clsd‘(topGen‘ran (,))) → 𝑏 ⊆ ℝ) |
50 | | dfss4 3858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑏 ⊆ ℝ ↔ (ℝ
∖ (ℝ ∖ 𝑏)) = 𝑏) |
51 | 49, 50 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑏 ∈
(Clsd‘(topGen‘ran (,))) → (ℝ ∖ (ℝ ∖
𝑏)) = 𝑏) |
52 | | rembl 23308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ℝ
∈ dom vol |
53 | 48 | cldopn 20835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑏 ∈
(Clsd‘(topGen‘ran (,))) → (ℝ ∖ 𝑏) ∈ (topGen‘ran
(,))) |
54 | | opnmbl 23370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((ℝ
∖ 𝑏) ∈
(topGen‘ran (,)) → (ℝ ∖ 𝑏) ∈ dom vol) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑏 ∈
(Clsd‘(topGen‘ran (,))) → (ℝ ∖ 𝑏) ∈ dom vol) |
56 | | difmbl 23311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((ℝ
∈ dom vol ∧ (ℝ ∖ 𝑏) ∈ dom vol) → (ℝ ∖
(ℝ ∖ 𝑏)) ∈
dom vol) |
57 | 52, 55, 56 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑏 ∈
(Clsd‘(topGen‘ran (,))) → (ℝ ∖ (ℝ ∖
𝑏)) ∈ dom
vol) |
58 | 51, 57 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 ∈
(Clsd‘(topGen‘ran (,))) → 𝑏 ∈ dom vol) |
59 | 47, 58 | vtoclga 3272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) → 𝑎 ∈ dom vol) |
60 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑎 ∈ dom vol →
(vol‘𝑎) =
(vol*‘𝑎)) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) → (vol‘𝑎) = (vol*‘𝑎)) |
62 | 46, 61 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))) → 𝑧 = (vol*‘𝑎)) |
63 | 62 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)))) → 𝑧 = (vol*‘𝑎)) |
64 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ∪ ran
((,) ∘ 𝑓) |
65 | | sstr 3611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ⊆ ∪ ran ((,) ∘ 𝑓)) → 𝑎 ⊆ ∪ ran
((,) ∘ 𝑓)) |
66 | 64, 65 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) → 𝑎 ⊆ ∪ ran
((,) ∘ 𝑓)) |
67 | 66 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))) → 𝑎 ⊆ ∪ ran
((,) ∘ 𝑓)) |
68 | | ovolsscl 23254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,)
∘ 𝑓) ⊆ ℝ
∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) →
(vol*‘𝑎) ∈
ℝ) |
69 | 16, 68 | mp3an2 1412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑎) ∈
ℝ) |
70 | 69 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑎 ⊆ ∪ ran ((,) ∘ 𝑓)) → (vol*‘𝑎) ∈ ℝ) |
71 | 67, 70 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)))) → (vol*‘𝑎) ∈ ℝ) |
72 | 63, 71 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)))) → 𝑧 ∈ ℝ) |
73 | 72 | rexlimdvaa 3032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) → 𝑧 ∈ ℝ)) |
74 | 73 | abssdv 3676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ⊆ ℝ) |
75 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑦 → (𝑧 = (vol‘𝑎) ↔ 𝑦 = (vol‘𝑎))) |
76 | 75 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 𝑦 → ((𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)))) |
77 | 76 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑦 → (∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)))) |
78 | 77 | ralab 3367 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑦 ∈
{𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ∀𝑦(∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))) |
79 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)) → 𝑦 = (vol‘𝑎)) |
80 | 79, 61 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))) → 𝑦 = (vol*‘𝑎)) |
81 | | ovolss 23253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,)
∘ 𝑓) ⊆ ℝ)
→ (vol*‘𝑎) ≤
(vol*‘∪ ran ((,) ∘ 𝑓))) |
82 | 66, 16, 81 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) → (vol*‘𝑎) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
83 | 82 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))) → (vol*‘𝑎) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
84 | 80, 83 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎))) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
85 | 84 | rexlimiva 3028 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑦 = (vol‘𝑎)) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
86 | 78, 85 | mpgbir 1726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
∀𝑦 ∈
{𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) |
87 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (vol*‘∪ ran ((,) ∘ 𝑓)) → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))) |
88 | 87 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (vol*‘∪ ran ((,) ∘ 𝑓)) → (∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))) |
89 | 88 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧
∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ 𝑥) |
90 | 86, 89 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ 𝑥) |
91 | | retop 22565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(topGen‘ran (,)) ∈ Top |
92 | | 0cld 20842 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((topGen‘ran (,)) ∈ Top → ∅ ∈
(Clsd‘(topGen‘ran (,)))) |
93 | 91, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ∅
∈ (Clsd‘(topGen‘ran (,))) |
94 | | 0ss 3972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ∅
⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) |
95 | | 0mbl 23307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ∅
∈ dom vol |
96 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
97 | 95, 96 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(vol‘∅) = (vol*‘∅) |
98 | | ovol0 23261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(vol*‘∅) = 0 |
99 | 97, 98 | eqtr2i 2645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 =
(vol‘∅) |
100 | 94, 99 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (∅
⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 =
(vol‘∅)) |
101 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑎 = ∅ → (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ↔ ∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴))) |
102 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑎 = ∅ →
(vol‘𝑎) =
(vol‘∅)) |
103 | 102 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑎 = ∅ → (0 =
(vol‘𝑎) ↔ 0 =
(vol‘∅))) |
104 | 101, 103 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑎 = ∅ → ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎)) ↔ (∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 =
(vol‘∅)))) |
105 | 104 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((∅
∈ (Clsd‘(topGen‘ran (,))) ∧ (∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘∅))) →
∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎))) |
106 | 93, 100, 105 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎)) |
107 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
V |
108 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 = 0 → (𝑧 = (vol‘𝑎) ↔ 0 = (vol‘𝑎))) |
109 | 108 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 0 → ((𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎)))) |
110 | 109 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 0 → (∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎)))) |
111 | 107, 110 | elab 3350 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 ∈
{𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 0 = (vol‘𝑎))) |
112 | 106, 111 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
{𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} |
113 | 112 | ne0ii 3923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅ |
114 | | suprcl 10983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ 𝑥) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) ∈
ℝ) |
115 | 113, 114 | mp3an2 1412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (({𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}𝑦 ≤ 𝑥) → sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) ∈
ℝ) |
116 | 74, 90, 115 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
sup({𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) ∈
ℝ) |
117 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) → 𝑧 = (vol‘𝑐)) |
118 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 = 𝑐 → (𝑏 ∈ dom vol ↔ 𝑐 ∈ dom vol)) |
119 | 118, 58 | vtoclga 3272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) → 𝑐 ∈ dom vol) |
120 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ dom vol →
(vol‘𝑐) =
(vol*‘𝑐)) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) → (vol‘𝑐) = (vol*‘𝑐)) |
122 | 117, 121 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))) → 𝑧 = (vol*‘𝑐)) |
123 | 122 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐)))) → 𝑧 = (vol*‘𝑐)) |
124 | | difss2 3739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) → 𝑐 ⊆ ∪ ran
((,) ∘ 𝑓)) |
125 | 124 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))) → 𝑐 ⊆ ∪ ran
((,) ∘ 𝑓)) |
126 | | ovolsscl 23254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,)
∘ 𝑓) ⊆ ℝ
∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) →
(vol*‘𝑐) ∈
ℝ) |
127 | 16, 126 | mp3an2 1412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑐) ∈
ℝ) |
128 | 127 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑐 ⊆ ∪ ran ((,) ∘ 𝑓)) → (vol*‘𝑐) ∈ ℝ) |
129 | 125, 128 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐)))) → (vol*‘𝑐) ∈ ℝ) |
130 | 123, 129 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐)))) → 𝑧 ∈ ℝ) |
131 | 130 | rexlimdvaa 3032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐)) → 𝑧 ∈ ℝ)) |
132 | 131 | abssdv 3676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))} ⊆ ℝ) |
133 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑦 → (𝑧 = (vol‘𝑐) ↔ 𝑦 = (vol‘𝑐))) |
134 | 133 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 𝑦 → ((𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑦 = (vol‘𝑐)))) |
135 | 134 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑦 → (∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐)))) |
136 | 135 | ralab 3367 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑦 ∈
{𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ∀𝑦(∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐)) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))) |
137 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑦 = (vol‘𝑐)) → 𝑦 = (vol‘𝑐)) |
138 | 137, 121 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑦 = (vol‘𝑐))) → 𝑦 = (vol*‘𝑐)) |
139 | | ovolss 23253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,)
∘ 𝑓) ⊆ ℝ)
→ (vol*‘𝑐) ≤
(vol*‘∪ ran ((,) ∘ 𝑓))) |
140 | 124, 16, 139 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) → (vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
141 | 140 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑦 = (vol‘𝑐))) → (vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
142 | 138, 141 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑦 = (vol‘𝑐))) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
143 | 142 | rexlimiva 3028 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑦 = (vol‘𝑐)) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
144 | 136, 143 | mpgbir 1726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
∀𝑦 ∈
{𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) |
145 | 87 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (vol*‘∪ ran ((,) ∘ 𝑓)) → (∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))) |
146 | 145 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧
∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ 𝑥) |
147 | 144, 146 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ 𝑥) |
148 | | 0ss 3972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ∅
⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) |
149 | 148, 99 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (∅
⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 =
(vol‘∅)) |
150 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 = ∅ → (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ↔ ∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) |
151 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 = ∅ →
(vol‘𝑐) =
(vol‘∅)) |
152 | 151 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 = ∅ → (0 =
(vol‘𝑐) ↔ 0 =
(vol‘∅))) |
153 | 150, 152 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 = ∅ → ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐)) ↔ (∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 =
(vol‘∅)))) |
154 | 153 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((∅
∈ (Clsd‘(topGen‘ran (,))) ∧ (∅ ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘∅))) →
∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 0 =
(vol‘𝑐))) |
155 | 93, 149, 154 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 0 =
(vol‘𝑐)) |
156 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 = 0 → (𝑧 = (vol‘𝑐) ↔ 0 = (vol‘𝑐))) |
157 | 156 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 0 → ((𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 0 =
(vol‘𝑐)))) |
158 | 157 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 0 → (∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐)))) |
159 | 107, 158 | elab 3350 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 ∈
{𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))} ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 0 = (vol‘𝑐))) |
160 | 155, 159 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
{𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))} |
161 | 160 | ne0ii 3923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅ |
162 | | suprcl 10983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ 𝑥) → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) ∈
ℝ) |
163 | 161, 162 | mp3an2 1412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (({𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))} ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 ≤ 𝑥) → sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) ∈
ℝ) |
164 | 132, 147,
163 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
sup({𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) ∈
ℝ) |
165 | 116, 164 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(sup({𝑧 ∣
∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) ∈
ℝ) |
166 | 165 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (sup({𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) ∈
ℝ) |
167 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) |
168 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤 ∩ 𝐴)) ∈ ℝ) |
169 | 9 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤 ∖ 𝐴)) ∈ ℝ) |
170 | | ovolsscl 23254 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ∪ ran
((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) ∈ ℝ) |
171 | 64, 16, 170 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) ∈ ℝ) |
172 | 171 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) ∈ ℝ) |
173 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ∪ ran
((,) ∘ 𝑓) |
174 | | ovolsscl 23254 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ∪ ran
((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ) |
175 | 173, 16, 174 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ) |
176 | 175 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ) |
177 | | ssrin 3838 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) → (𝑤 ∩ 𝐴) ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴)) |
178 | 64, 16 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ℝ |
179 | | ovolss 23253 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∩ 𝐴) ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ⊆ ℝ) → (vol*‘(𝑤 ∩ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴))) |
180 | 177, 178,
179 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) → (vol*‘(𝑤 ∩ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴))) |
181 | 180 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤 ∩ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴))) |
182 | | ssdif 3745 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) → (𝑤 ∖ 𝐴) ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) |
183 | 173, 16 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ |
184 | | ovolss 23253 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑤 ∖ 𝐴) ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ) → (vol*‘(𝑤 ∖ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) |
185 | 182, 183,
184 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) → (vol*‘(𝑤 ∖ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) |
186 | 185 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(𝑤 ∖ 𝐴)) ≤ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) |
187 | 168, 169,
172, 176, 181, 186 | le2addd 10646 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ ((vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))) |
188 | | dfin4 3867 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) = (∪ ran ((,)
∘ 𝑓) ∖ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) |
189 | 188 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) = (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) |
190 | 189 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((vol*‘(∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) = ((vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) |
191 | 187, 190 | syl6breq 4694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ ((vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))) |
192 | 191 | adantlll 754 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ ((vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) + (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)))) |
193 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) → ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧
(vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈
(Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ))) |
194 | 188 | sseq2i 3630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ↔ 𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) |
195 | 194 | anbi1i 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎))) |
196 | 195 | rexbii 3041 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) ∧ 𝑧 = (vol‘𝑎))) |
197 | 196 | abbii 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ {𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} = {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) ∧ 𝑧 = (vol‘𝑎))} |
198 | 197 | supeq1i 8353 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
sup({𝑧 ∣
∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) |
199 | 16 | jctl 564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → (∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ)) |
200 | 199 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (∪ ran ((,) ∘ 𝑓) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ)) |
201 | 175, 183 | jctil 560 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → ((∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ)) |
202 | 201 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∈ ℝ)) |
203 | | ltso 10118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ < Or
ℝ |
204 | 203 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → < Or
ℝ) |
205 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) |
206 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 𝑥 ∈ V |
207 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 = 𝑥 → (𝑧 = (vol‘𝑐) ↔ 𝑥 = (vol‘𝑐))) |
208 | 207 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 = 𝑥 → ((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐)))) |
209 | 208 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 = 𝑥 → (∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐)))) |
210 | 206, 209 | elab 3350 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))} ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) |
211 | 16, 139 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) → (vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
212 | 211 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → (vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
213 | 48 | cldss 20833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) → 𝑐 ⊆ ℝ) |
214 | | ovolcl 23246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑐 ⊆ ℝ →
(vol*‘𝑐) ∈
ℝ*) |
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) → (vol*‘𝑐) ∈
ℝ*) |
216 | | xrlenlt 10103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((vol*‘𝑐)
∈ ℝ* ∧ (vol*‘∪ ran
((,) ∘ 𝑓)) ∈
ℝ*) → ((vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐))) |
217 | 215, 34, 216 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) → ((vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐))) |
218 | 217 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → ((vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐))) |
219 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑥 = (vol‘𝑐) → 𝑥 = (vol‘𝑐)) |
220 | 219, 121 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑥 = (vol‘𝑐)) → 𝑥 = (vol*‘𝑐)) |
221 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑥 = (vol*‘𝑐) → ((vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥 ↔ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐))) |
222 | 221 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑥 = (vol*‘𝑐) → (¬
(vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥 ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐))) |
223 | 220, 222 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑥 = (vol‘𝑐)) → (¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥 ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐))) |
224 | 223 | adantrl 752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → (¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥 ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < (vol*‘𝑐))) |
225 | 218, 224 | bitr4d 271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → ((vol*‘𝑐) ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥)) |
226 | 212, 225 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐))) → ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥) |
227 | 226 | rexlimiva 3028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑥 = (vol‘𝑐)) → ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥) |
228 | 210, 227 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))} → ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥) |
229 | 228 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑥 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}) → ¬ (vol*‘∪ ran ((,) ∘ 𝑓)) < 𝑥) |
230 | | retopbas 22564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ran (,)
∈ TopBases |
231 | | bastg 20770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (ran (,)
∈ TopBases → ran (,) ⊆ (topGen‘ran (,))) |
232 | 230, 231 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ran (,)
⊆ (topGen‘ran (,)) |
233 | 13, 232 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ran ((,)
∘ 𝑓) ⊆
(topGen‘ran (,)) |
234 | | uniopn 20702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((topGen‘ran (,)) ∈ Top ∧ ran ((,) ∘ 𝑓) ⊆ (topGen‘ran
(,))) → ∪ ran ((,) ∘ 𝑓) ∈ (topGen‘ran
(,))) |
235 | 91, 233, 234 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ∪ ran ((,) ∘ 𝑓) ∈ (topGen‘ran
(,)) |
236 | | mblfinlem2 33447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((∪ ran ((,) ∘ 𝑓) ∈ (topGen‘ran (,)) ∧ 𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐))) |
237 | 235, 236 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐))) |
238 | 121 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) → (vol*‘𝑐) = (vol‘𝑐)) |
239 | 238 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑐 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑥 < (vol*‘𝑐)) → ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐))) |
240 | 239 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) → (𝑥 < (vol*‘𝑐) → ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐)))) |
241 | 240 | anim2d 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) → ((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)) → (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
((vol*‘𝑐) =
(vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐))))) |
242 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(vol*‘𝑐)
∈ V |
243 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑦 = (vol*‘𝑐) → (𝑦 = (vol‘𝑐) ↔ (vol*‘𝑐) = (vol‘𝑐))) |
244 | 243 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 = (vol*‘𝑐) → ((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ↔ (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
(vol*‘𝑐) =
(vol‘𝑐)))) |
245 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 = (vol*‘𝑐) → (𝑥 < 𝑦 ↔ 𝑥 < (vol*‘𝑐))) |
246 | 244, 245 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 = (vol*‘𝑐) → (((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
(vol*‘𝑐) =
(vol‘𝑐)) ∧ 𝑥 < (vol*‘𝑐)))) |
247 | 242, 246 | spcev 3300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ (vol*‘𝑐) = (vol‘𝑐)) ∧ 𝑥 < (vol*‘𝑐)) → ∃𝑦((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦)) |
248 | 247 | anasss 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ((vol*‘𝑐) = (vol‘𝑐) ∧ 𝑥 < (vol*‘𝑐))) → ∃𝑦((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦)) |
249 | 241, 248 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 ∈
(Clsd‘(topGen‘ran (,))) → ((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)) → ∃𝑦((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦))) |
250 | 249 | reximia 3009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑥 < (vol*‘𝑐)) → ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦)) |
251 | 237, 250 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))∃𝑦((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦)) |
252 | | r19.41v 3089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ (∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦)) |
253 | 252 | exbii 1774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∃𝑦∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ∃𝑦(∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦)) |
254 | | rexcom4 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ∃𝑦∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦)) |
255 | 133 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 = 𝑦 → ((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)))) |
256 | 255 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 = 𝑦 → (∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)))) |
257 | 256 | rexab 3369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∃𝑦 ∈
{𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦 ↔ ∃𝑦(∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦)) |
258 | 253, 254,
257 | 3bitr4i 292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))∃𝑦((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = (vol‘𝑐)) ∧ 𝑥 < 𝑦) ↔ ∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦) |
259 | 251, 258 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦) |
260 | 259 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 𝑥 < (vol*‘∪ ran ((,) ∘ 𝑓)))) → ∃𝑦 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}𝑥 < 𝑦) |
261 | 204, 205,
229, 260 | eqsupd 8363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
sup({𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = (vol*‘∪ ran ((,) ∘ 𝑓))) |
262 | 261 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(vol*‘∪ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) |
263 | 262 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘∪ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) |
264 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 = 𝑎 → (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ↔
𝑎 ⊆ ∪ ran ((,) ∘ 𝑓))) |
265 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑐 = 𝑎 → (vol‘𝑐) = (vol‘𝑎)) |
266 | 265 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 = 𝑎 → (𝑧 = (vol‘𝑐) ↔ 𝑧 = (vol‘𝑎))) |
267 | 264, 266 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 = 𝑎 → ((𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑎 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎)))) |
268 | 267 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))) |
269 | 268 | abbii 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ {𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))} = {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))} |
270 | 269 | supeq1i 8353 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
sup({𝑧 ∣
∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) |
271 | 263, 270 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘∪ ran ((,) ∘ 𝑓)) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < )) |
272 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 = 𝑎 → (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ↔ 𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) |
273 | 272, 266 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 = 𝑎 → ((𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑎)))) |
274 | 273 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))) |
275 | 274 | abbii 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ {𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))} = {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))} |
276 | 275 | supeq1i 8353 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
sup({𝑧 ∣
∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) |
277 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈
ℝ)) |
278 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 = 𝑧 → (𝑦 = (vol‘𝑏) ↔ 𝑧 = (vol‘𝑏))) |
279 | 278 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 = 𝑧 → ((𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏)) ↔ (𝑏 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑏)))) |
280 | 279 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 = 𝑧 → (∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏)) ↔ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑏)))) |
281 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝐴 ↔ 𝑐 ⊆ 𝐴)) |
282 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑏 = 𝑐 → (vol‘𝑏) = (vol‘𝑐)) |
283 | 282 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑏 = 𝑐 → (𝑧 = (vol‘𝑏) ↔ 𝑧 = (vol‘𝑐))) |
284 | 281, 283 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑏 = 𝑐 → ((𝑏 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑏)) ↔ (𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐)))) |
285 | 284 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(∃𝑏 ∈
(Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑏)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))) |
286 | 280, 285 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = 𝑧 → (∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐)))) |
287 | 286 | cbvabv 2747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ {𝑦 ∣ ∃𝑏 ∈
(Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))} = {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))} |
288 | 287 | supeq1i 8353 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
sup({𝑦 ∣
∃𝑏 ∈
(Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) = sup({𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) |
289 | 288 | eqeq2i 2634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((vol*‘𝐴) =
sup({𝑦 ∣ ∃𝑏 ∈
(Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) ↔ (vol*‘𝐴) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) |
290 | 289 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((vol*‘𝐴) =
sup({𝑦 ∣ ∃𝑏 ∈
(Clsd‘(topGen‘ran (,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ) → (vol*‘𝐴) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) |
291 | 290 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝐴) = sup({𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ 𝐴 ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) |
292 | | mblfinlem3 33448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((∪ 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 ((,) ∘ 𝑓) ∖ 𝐴))) |
293 | 200, 277,
263, 291, 292 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → sup({𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < ) = (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) |
294 | 276, 293 | syl5reqr 2671 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) = sup({𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < )) |
295 | | mblfinlem3 33448 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((∪ 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
((,) ∘ 𝑓) ∖
𝐴)))) |
296 | 200, 202,
271, 294, 295 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → sup({𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
(∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) = (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)))) |
297 | 198, 296 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → sup({𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) = (vol*‘(∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)))) |
298 | 297, 293 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ⊆ ℝ ∧
(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 ((,) ∘ 𝑓) ∖ 𝐴)))) |
299 | 193, 298 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ⊆
ℝ ∧ (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 ((,) ∘ 𝑓) ∖ 𝐴)))) |
300 | 192, 299 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ⊆
ℝ ∧ (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‘𝑐))}, ℝ, < ))) |
301 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 ∈
{𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} → {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅) |
302 | 112, 301 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ≠ ∅) |
303 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 ∈
{𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))} → {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅) |
304 | 160, 303 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))} ≠ ∅) |
305 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} = {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} |
306 | 74, 302, 90, 132, 304, 147, 305 | supadd 10991 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((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‘𝑐))}𝑡 = (𝑢 + 𝑣)}, ℝ, < )) |
307 | | reeanv 3107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑣 = (vol‘𝑐))) ↔ (∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐)))) |
308 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 𝑢 ∈ V |
309 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 = 𝑢 → (𝑧 = (vol‘𝑎) ↔ 𝑢 = (vol‘𝑎))) |
310 | 309 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 = 𝑢 → ((𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ (𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)))) |
311 | 310 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 = 𝑢 → (∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎)) ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)))) |
312 | 308, 311 | elab 3350 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ↔ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎))) |
313 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 𝑣 ∈ V |
314 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 = 𝑣 → (𝑧 = (vol‘𝑐) ↔ 𝑣 = (vol‘𝑐))) |
315 | 314 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 = 𝑣 → ((𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑣 = (vol‘𝑐)))) |
316 | 315 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 = 𝑣 → (∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐)) ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐)))) |
317 | 313, 316 | elab 3350 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))} ↔ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐))) |
318 | 312, 317 | anbi12i 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}) ↔ (∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑣 = (vol‘𝑐)))) |
319 | 307, 318 | bitr4i 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑣 = (vol‘𝑐))) ↔ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) |
320 | | an4 865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ↔ ((𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑣 = (vol‘𝑐)))) |
321 | | oveq12 6659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐)) → (𝑢 + 𝑣) = ((vol‘𝑎) + (vol‘𝑐))) |
322 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))
→ 𝑎 ∈ dom
vol) |
323 | 322 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) → 𝑎 ∈ dom
vol) |
324 | 119 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))
→ 𝑐 ∈ dom
vol) |
325 | 324 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) → 𝑐 ∈ dom
vol) |
326 | | ss2in 3840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) → (𝑎 ∩ 𝑐) ⊆ ((∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∩ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) |
327 | 188 | ineq1i 3810 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∩ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) = ((∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) ∩ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) |
328 | | incom 3805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) ∩ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) = ((∪ ran ((,)
∘ 𝑓) ∖ 𝐴) ∩ (∪ ran ((,) ∘ 𝑓) ∖ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) |
329 | | disjdif 4040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∩ (∪ ran
((,) ∘ 𝑓) ∖
(∪ ran ((,) ∘ 𝑓) ∖ 𝐴))) = ∅ |
330 | 327, 328,
329 | 3eqtri 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∩ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) =
∅ |
331 | 326, 330 | syl6sseq 3651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) → (𝑎 ∩ 𝑐) ⊆ ∅) |
332 | | ss0 3974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ∩ 𝑐) ⊆ ∅ → (𝑎 ∩ 𝑐) = ∅) |
333 | 331, 332 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) → (𝑎 ∩ 𝑐) = ∅) |
334 | 333 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) → (𝑎 ∩ 𝑐) = ∅) |
335 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))
→ (vol‘𝑎) =
(vol*‘𝑎)) |
336 | 335 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) →
(vol‘𝑎) =
(vol*‘𝑎)) |
337 | 66, 16 | jctir 561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) → (𝑎 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ)) |
338 | 68 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,)
∘ 𝑓) ⊆ ℝ)
∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) →
(vol*‘𝑎) ∈
ℝ) |
339 | 337, 338 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑎) ∈
ℝ) |
340 | 339 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴)) → (vol*‘𝑎) ∈ ℝ) |
341 | 340 | ad2ant2r 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) →
(vol*‘𝑎) ∈
ℝ) |
342 | 336, 341 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) →
(vol‘𝑎) ∈
ℝ) |
343 | 121 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))
→ (vol‘𝑐) =
(vol*‘𝑐)) |
344 | 343 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) →
(vol‘𝑐) =
(vol*‘𝑐)) |
345 | 124, 16 | jctir 561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) → (𝑐 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ)) |
346 | 126 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑐 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ ∪ ran ((,)
∘ 𝑓) ⊆ ℝ)
∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) →
(vol*‘𝑐) ∈
ℝ) |
347 | 345, 346 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → (vol*‘𝑐) ∈
ℝ) |
348 | 347 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴)) → (vol*‘𝑐) ∈ ℝ) |
349 | 348 | ad2ant2rl 785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) →
(vol*‘𝑐) ∈
ℝ) |
350 | 344, 349 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) →
(vol‘𝑐) ∈
ℝ) |
351 | | volun 23313 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑎 ∈ dom vol ∧ 𝑐 ∈ dom vol ∧ (𝑎 ∩ 𝑐) = ∅) ∧ ((vol‘𝑎) ∈ ℝ ∧
(vol‘𝑐) ∈
ℝ)) → (vol‘(𝑎 ∪ 𝑐)) = ((vol‘𝑎) + (vol‘𝑐))) |
352 | 323, 325,
334, 342, 350, 351 | syl32anc 1334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) →
(vol‘(𝑎 ∪ 𝑐)) = ((vol‘𝑎) + (vol‘𝑐))) |
353 | | unmbl 23305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ∈ dom vol ∧ 𝑐 ∈ dom vol) → (𝑎 ∪ 𝑐) ∈ dom vol) |
354 | 59, 119, 353 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))
→ (𝑎 ∪ 𝑐) ∈ dom
vol) |
355 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ∪ 𝑐) ∈ dom vol → (vol‘(𝑎 ∪ 𝑐)) = (vol*‘(𝑎 ∪ 𝑐))) |
356 | 354, 355 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,))))
→ (vol‘(𝑎 ∪
𝑐)) = (vol*‘(𝑎 ∪ 𝑐))) |
357 | 356 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) →
(vol‘(𝑎 ∪ 𝑐)) = (vol*‘(𝑎 ∪ 𝑐))) |
358 | 352, 357 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) →
((vol‘𝑎) +
(vol‘𝑐)) =
(vol*‘(𝑎 ∪ 𝑐))) |
359 | 321, 358 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) → (𝑢 + 𝑣) = (vol*‘(𝑎 ∪ 𝑐))) |
360 | | eqtr 2641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 = (𝑢 + 𝑣) ∧ (𝑢 + 𝑣) = (vol*‘(𝑎 ∪ 𝑐))) → 𝑦 = (vol*‘(𝑎 ∪ 𝑐))) |
361 | 360 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑢 + 𝑣) = (vol*‘(𝑎 ∪ 𝑐)) ∧ 𝑦 = (𝑢 + 𝑣)) → 𝑦 = (vol*‘(𝑎 ∪ 𝑐))) |
362 | 359, 361 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ∧ 𝑦 = (𝑢 + 𝑣)) → 𝑦 = (vol*‘(𝑎 ∪ 𝑐))) |
363 | 66, 124 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) → (𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑐 ⊆ ∪ ran
((,) ∘ 𝑓))) |
364 | | unss 3787 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑎 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑐 ⊆ ∪ ran
((,) ∘ 𝑓)) ↔
(𝑎 ∪ 𝑐) ⊆ ∪ ran
((,) ∘ 𝑓)) |
365 | 363, 364 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) → (𝑎 ∪ 𝑐) ⊆ ∪ ran
((,) ∘ 𝑓)) |
366 | | ovolss 23253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑎 ∪ 𝑐) ⊆ ∪ ran
((,) ∘ 𝑓) ∧ ∪ ran ((,) ∘ 𝑓) ⊆ ℝ) → (vol*‘(𝑎 ∪ 𝑐)) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
367 | 365, 16, 366 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) →
(vol*‘(𝑎 ∪ 𝑐)) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
368 | 367 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ∧ 𝑦 = (𝑢 + 𝑣)) → (vol*‘(𝑎 ∪ 𝑐)) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
369 | 362, 368 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) ∧ 𝑦 = (𝑢 + 𝑣)) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
370 | 369 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
∧ (𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴))) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))) |
371 | 370 | expl 648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
→ (((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴)) ∧ (𝑢 = (vol‘𝑎) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))) |
372 | 320, 371 | syl5bir 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑎 ∈
(Clsd‘(topGen‘ran (,))) ∧ 𝑐 ∈ (Clsd‘(topGen‘ran (,)))))
→ (((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))) |
373 | 372 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))((𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑢 = (vol‘𝑎)) ∧ (𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑣 = (vol‘𝑐))) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))) |
374 | 319, 373 | syl5bir 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → ((𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}) → (𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))))) |
375 | 374 | rexlimdvv 3037 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))) |
376 | 375 | alrimiv 1855 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
∀𝑦(∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))) |
377 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑦 → (𝑡 = (𝑢 + 𝑣) ↔ 𝑦 = (𝑢 + 𝑣))) |
378 | 377 | 2rexbidv 3057 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑦 → (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣) ↔ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣))) |
379 | 378 | ralab 3367 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑦 ∈
{𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)) ↔ ∀𝑦(∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑦 = (𝑢 + 𝑣) → 𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))) |
380 | 376, 379 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
381 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) ∧ 𝑡 = (𝑢 + 𝑣)) → 𝑡 = (𝑢 + 𝑣)) |
382 | 74 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}) → 𝑢 ∈ ℝ) |
383 | 132 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}) → 𝑣 ∈ ℝ) |
384 | | readdcl 10019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢 + 𝑣) ∈ ℝ) |
385 | 382, 383,
384 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}) ∧ ((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) → (𝑢 + 𝑣) ∈ ℝ) |
386 | 385 | anandis 873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) → (𝑢 + 𝑣) ∈ ℝ) |
387 | 386 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) ∧ 𝑡 = (𝑢 + 𝑣)) → (𝑢 + 𝑣) ∈ ℝ) |
388 | 381, 387 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) ∧ 𝑡 = (𝑢 + 𝑣)) → 𝑡 ∈ ℝ) |
389 | 388 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧ (𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))} ∧ 𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))})) → (𝑡 = (𝑢 + 𝑣) → 𝑡 ∈ ℝ)) |
390 | 389 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣) → 𝑡 ∈ ℝ)) |
391 | 390 | abssdv 3676 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ⊆ ℝ) |
392 | | 00id 10211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (0 + 0) =
0 |
393 | 392 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 0 = (0 +
0) |
394 | | rspceov 6692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((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 = (𝑢 + 𝑣)) |
395 | 112, 160,
393, 394 | mp3an 1424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
∃𝑢 ∈
{𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}0 = (𝑢 + 𝑣) |
396 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑡 = 0 → (𝑡 = (𝑢 + 𝑣) ↔ 0 = (𝑢 + 𝑣))) |
397 | 396 | 2rexbidv 3057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 0 → (∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣) ↔ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}0 = (𝑢 + 𝑣))) |
398 | 107, 397 | spcev 3300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑢 ∈
{𝑧 ∣ ∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}0 = (𝑢 + 𝑣) → ∃𝑡∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)) |
399 | 395, 398 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
∃𝑡∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣) |
400 | | abn0 3954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅ ↔ ∃𝑡∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)) |
401 | 399, 400 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅ |
402 | 401 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ → {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)} ≠ ∅) |
403 | 87 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = (vol*‘∪ ran ((,) ∘ 𝑓)) → (∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓)))) |
404 | 403 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ ∧
∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ 𝑥) |
405 | 380, 404 | mpdan 702 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ {𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ 𝑥) |
406 | 391, 402,
405 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((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‘𝑐))}𝑡 = (𝑢 + 𝑣)}𝑦 ≤ 𝑥)) |
407 | | suprleub 10989 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (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 ((,) ∘ 𝑓)))) |
408 | 406, 407 | mpancom 703 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((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 ((,) ∘ 𝑓)))) |
409 | 380, 408 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
sup({𝑡 ∣ ∃𝑢 ∈ {𝑧 ∣ ∃𝑎 ∈ (Clsd‘(topGen‘ran
(,)))(𝑎 ⊆ (∪ ran ((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}∃𝑣 ∈ {𝑧 ∣ ∃𝑐 ∈ (Clsd‘(topGen‘ran
(,)))(𝑐 ⊆ (∪ ran ((,) ∘ 𝑓) ∖ 𝐴) ∧ 𝑧 = (vol‘𝑐))}𝑡 = (𝑢 + 𝑣)}, ℝ, < ) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
410 | 306, 409 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ →
(sup({𝑧 ∣
∃𝑎 ∈
(Clsd‘(topGen‘ran (,)))(𝑎 ⊆ (∪ ran
((,) ∘ 𝑓) ∩ 𝐴) ∧ 𝑧 = (vol‘𝑎))}, ℝ, < ) + sup({𝑧 ∣ ∃𝑐 ∈
(Clsd‘(topGen‘ran (,)))(𝑐 ⊆ (∪ ran
((,) ∘ 𝑓) ∖
𝐴) ∧ 𝑧 = (vol‘𝑐))}, ℝ, < )) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
411 | 410 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ⊆
ℝ ∧ (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 ((,) ∘ 𝑓))) |
412 | 45, 166, 167, 300, 411 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ∈ ℝ) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
413 | 44, 412 | sylan2 491 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ (vol*‘∪ ran ((,) ∘ 𝑓)) ≠ +∞) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
414 | 33, 413 | pm2.61dane 2881 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
415 | 414 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘∪ ran ((,) ∘ 𝑓))) |
416 | | ssid 3624 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran
((,) ∘ 𝑓) |
417 | 20 | ovollb 23247 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ∪ ran ((,) ∘
𝑓) ⊆ ∪ ran ((,) ∘ 𝑓)) → (vol*‘∪ ran ((,) ∘ 𝑓)) ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < )) |
418 | 416, 417 | mpan2 707 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (vol*‘∪ ran
((,) ∘ 𝑓)) ≤
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
)) |
419 | 418 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) → (vol*‘∪ ran ((,) ∘ 𝑓)) ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < )) |
420 | 12, 18, 27, 415, 419 | xrletrd 11993 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < )) |
421 | 420 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < )) |
422 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢
(((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → 𝑢 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) |
423 | 421, 422 | breqtrrd 4681 |
. . . . . . . . . . . . 13
⊢
(((((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) ∧ 𝑤 ⊆
∪ ran ((,) ∘ 𝑓)) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢) |
424 | 423 | expl 648 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) → ((𝑤
⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢)) |
425 | 3, 424 | sylan2 491 |
. . . . . . . . . . 11
⊢
(((((𝐴 ⊆
ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) ∧ 𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
→ ((𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢)) |
426 | 425 | rexlimdva 3031 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) → (∃𝑓
∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚
ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢)) |
427 | 426 | ralrimivw 2967 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) → ∀𝑢
∈ ℝ* (∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) →
((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢)) |
428 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑢 → (𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ) ↔ 𝑢 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))) |
429 | 428 | anbi2d 740 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑢 → ((𝑤 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) ↔
(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )))) |
430 | 429 | rexbidv 3052 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑢 → (∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) ↔
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )))) |
431 | 430 | ralrab 3368 |
. . . . . . . . 9
⊢
(∀𝑢 ∈
{𝑣 ∈
ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ))}
((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢 ↔ ∀𝑢 ∈ ℝ* (∃𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑢 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) →
((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢)) |
432 | 427, 431 | sylibr 224 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) → ∀𝑢
∈ {𝑣 ∈
ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ))}
((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢) |
433 | | ssrab2 3687 |
. . . . . . . . 9
⊢ {𝑣 ∈ ℝ*
∣ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} ⊆ ℝ* |
434 | 11 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈
ℝ*) |
435 | | infxrgelb 12165 |
. . . . . . . . 9
⊢ (({𝑣 ∈ ℝ*
∣ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} ⊆ ℝ* ∧
((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ∈ ℝ*) →
(((vol*‘(𝑤 ∩
𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ inf({𝑣 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))}, ℝ*, < ) ↔ ∀𝑢 ∈ {𝑣 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢)) |
436 | 433, 434,
435 | sylancr 695 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) → (((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ inf({𝑣 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))}, ℝ*, < ) ↔ ∀𝑢 ∈ {𝑣 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ 𝑢)) |
437 | 432, 436 | mpbird 247 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ inf({𝑣 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))}, ℝ*, < )) |
438 | | eqid 2622 |
. . . . . . . . 9
⊢ {𝑣 ∈ ℝ*
∣ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} = {𝑣 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} |
439 | 438 | ovolval 23242 |
. . . . . . . 8
⊢ (𝑤 ⊆ ℝ →
(vol*‘𝑤) = inf({𝑣 ∈ ℝ*
∣ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))}, ℝ*, < )) |
440 | 439 | ad2antrl 764 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) → (vol*‘𝑤) = inf({𝑣 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑤 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑣 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))}, ℝ*, < )) |
441 | 437, 440 | breqtrrd 4681 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ (𝑤 ⊆ ℝ ∧
(vol*‘𝑤) ∈
ℝ)) → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤)) |
442 | 441 | expr 643 |
. . . . 5
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ 𝑤 ⊆ ℝ) →
((vol*‘𝑤) ∈
ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤))) |
443 | 2, 442 | sylan2 491 |
. . . 4
⊢ ((((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) ∧ 𝑤 ∈ 𝒫 ℝ)
→ ((vol*‘𝑤)
∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤))) |
444 | 443 | ralrimiva 2966 |
. . 3
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) → ∀𝑤 ∈ 𝒫
ℝ((vol*‘𝑤)
∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤))) |
445 | | ismbl2 23295 |
. . . . 5
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧
∀𝑤 ∈ 𝒫
ℝ((vol*‘𝑤)
∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤)))) |
446 | 445 | baibr 945 |
. . . 4
⊢ (𝐴 ⊆ ℝ →
(∀𝑤 ∈ 𝒫
ℝ((vol*‘𝑤)
∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤)) ↔ 𝐴 ∈ dom vol)) |
447 | 446 | ad2antrr 762 |
. . 3
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) → (∀𝑤 ∈ 𝒫
ℝ((vol*‘𝑤)
∈ ℝ → ((vol*‘(𝑤 ∩ 𝐴)) + (vol*‘(𝑤 ∖ 𝐴))) ≤ (vol*‘𝑤)) ↔ 𝐴 ∈ dom vol)) |
448 | 444, 447 | mpbid 222 |
. 2
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < )) → 𝐴 ∈ dom
vol) |
449 | 1, 448 | impbida 877 |
1
⊢ ((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) → (𝐴 ∈
dom vol ↔ (vol*‘𝐴) = sup({𝑦 ∣ ∃𝑏 ∈ (Clsd‘(topGen‘ran
(,)))(𝑏 ⊆ 𝐴 ∧ 𝑦 = (vol‘𝑏))}, ℝ, < ))) |