Step | Hyp | Ref
| Expression |
1 | | ioof 12271 |
. . . . 5
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
2 | | uniioombl.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
3 | | inss2 3834 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
4 | | rexpssxrxp 10084 |
. . . . . . 7
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
5 | 3, 4 | sstri 3612 |
. . . . . 6
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
6 | | fss 6056 |
. . . . . 6
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
7 | 2, 5, 6 | sylancl 694 |
. . . . 5
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
8 | | fco 6058 |
. . . . 5
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
9 | 1, 7, 8 | sylancr 695 |
. . . 4
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
10 | | frn 6053 |
. . . 4
⊢ (((,)
∘ 𝐹):ℕ⟶𝒫 ℝ →
ran ((,) ∘ 𝐹) ⊆
𝒫 ℝ) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝜑 → ran ((,) ∘ 𝐹) ⊆ 𝒫
ℝ) |
12 | | sspwuni 4611 |
. . 3
⊢ (ran ((,)
∘ 𝐹) ⊆
𝒫 ℝ ↔ ∪ ran ((,) ∘ 𝐹) ⊆
ℝ) |
13 | 11, 12 | sylib 208 |
. 2
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) |
14 | | elpwi 4168 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝒫 ℝ →
𝑧 ⊆
ℝ) |
15 | 14 | ad2antrl 764 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → 𝑧 ⊆
ℝ) |
16 | 15 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 𝑧 ⊆ ℝ) |
17 | | simprr 796 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (vol*‘𝑧) ∈ ℝ) |
18 | 17 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → (vol*‘𝑧) ∈ ℝ) |
19 | | rphalfcl 11858 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ+) |
20 | 19 | rphalfcld 11884 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ ((𝑟 / 2) / 2) ∈
ℝ+) |
21 | 20 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((𝑟 / 2) / 2) ∈
ℝ+) |
22 | | eqid 2622 |
. . . . . . . . . 10
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
23 | 22 | ovolgelb 23248 |
. . . . . . . . 9
⊢ ((𝑧 ⊆ ℝ ∧
(vol*‘𝑧) ∈
ℝ ∧ ((𝑟 / 2) / 2)
∈ ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2)))) |
24 | 16, 18, 21, 23 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2)))) |
25 | 2 | ad3antrrr 766 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
26 | | uniioombl.2 |
. . . . . . . . . 10
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
27 | 26 | ad3antrrr 766 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) →
Disj 𝑥 ∈
ℕ ((,)‘(𝐹‘𝑥))) |
28 | | uniioombl.3 |
. . . . . . . . 9
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
29 | | eqid 2622 |
. . . . . . . . 9
⊢ ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,)
∘ 𝐹) |
30 | 18 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) →
(vol*‘𝑧) ∈
ℝ) |
31 | 19 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → (𝑟 / 2) ∈
ℝ+) |
32 | 31 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → (𝑟 / 2) ∈
ℝ+) |
33 | 32 | rphalfcld 11884 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → ((𝑟 / 2) / 2) ∈
ℝ+) |
34 | | elmapi 7879 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
35 | 34 | ad2antrl 764 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → 𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
36 | | simprrl 804 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → 𝑧 ⊆ ∪ ran ((,) ∘ 𝑓)) |
37 | | simprrr 805 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))) |
38 | 25, 27, 28, 29, 30, 33, 35, 36, 22, 37 | uniioombllem6 23356 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) →
((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹)))) ≤
((vol*‘𝑧) + (4
· ((𝑟 / 2) /
2)))) |
39 | 24, 38 | rexlimddv 3035 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + (4 · ((𝑟 / 2) / 2)))) |
40 | | rpcn 11841 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℂ) |
41 | 40 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 𝑟 ∈ ℂ) |
42 | | 2cnd 11093 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 2 ∈ ℂ) |
43 | | 2ne0 11113 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
44 | 43 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 2 ≠ 0) |
45 | 41, 42, 42, 44, 44 | divdiv1d 10832 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((𝑟 / 2) / 2) = (𝑟 / (2 · 2))) |
46 | | 2t2e4 11177 |
. . . . . . . . . . . 12
⊢ (2
· 2) = 4 |
47 | 46 | oveq2i 6661 |
. . . . . . . . . . 11
⊢ (𝑟 / (2 · 2)) = (𝑟 / 4) |
48 | 45, 47 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((𝑟 / 2) / 2) = (𝑟 / 4)) |
49 | 48 | oveq2d 6666 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → (4 · ((𝑟 / 2) / 2)) = (4 · (𝑟 / 4))) |
50 | | 4cn 11098 |
. . . . . . . . . . 11
⊢ 4 ∈
ℂ |
51 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 4 ∈ ℂ) |
52 | | 4ne0 11117 |
. . . . . . . . . . 11
⊢ 4 ≠
0 |
53 | 52 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 4 ≠ 0) |
54 | 41, 51, 53 | divcan2d 10803 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → (4 · (𝑟 / 4)) = 𝑟) |
55 | 49, 54 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → (4 · ((𝑟 / 2) / 2)) = 𝑟) |
56 | 55 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((vol*‘𝑧) + (4 · ((𝑟 / 2) / 2))) = ((vol*‘𝑧) + 𝑟)) |
57 | 39, 56 | breqtrd 4679 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + 𝑟)) |
58 | 57 | ralrimiva 2966 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → ∀𝑟
∈ ℝ+ ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + 𝑟)) |
59 | | inss1 3833 |
. . . . . . . . 9
⊢ (𝑧 ∩ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧 |
60 | 59 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (𝑧 ∩
∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧) |
61 | | ovolsscl 23254 |
. . . . . . . 8
⊢ (((𝑧 ∩ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ) →
(vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) ∈ ℝ) |
62 | 60, 15, 17, 61 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) ∈
ℝ) |
63 | | difssd 3738 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (𝑧 ∖
∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧) |
64 | | ovolsscl 23254 |
. . . . . . . 8
⊢ (((𝑧 ∖ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ) →
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹))) ∈ ℝ) |
65 | 63, 15, 17, 64 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹))) ∈
ℝ) |
66 | 62, 65 | readdcld 10069 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ∈ ℝ) |
67 | | alrple 12037 |
. . . . . 6
⊢
((((vol*‘(𝑧
∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹)))) ∈
ℝ ∧ (vol*‘𝑧) ∈ ℝ) → (((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹)))) ≤
(vol*‘𝑧) ↔
∀𝑟 ∈
ℝ+ ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + 𝑟))) |
68 | 66, 17, 67 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧) ↔ ∀𝑟 ∈ ℝ+
((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹)))) ≤
((vol*‘𝑧) + 𝑟))) |
69 | 58, 68 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧)) |
70 | 69 | expr 643 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 ℝ) →
((vol*‘𝑧) ∈
ℝ → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧))) |
71 | 70 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝒫 ℝ((vol*‘𝑧) ∈ ℝ →
((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹)))) ≤
(vol*‘𝑧))) |
72 | | ismbl2 23295 |
. 2
⊢ (∪ ran ((,) ∘ 𝐹) ∈ dom vol ↔ (∪ ran ((,) ∘ 𝐹) ⊆ ℝ ∧ ∀𝑧 ∈ 𝒫
ℝ((vol*‘𝑧)
∈ ℝ → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧)))) |
73 | 13, 71, 72 | sylanbrc 698 |
1
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ∈ dom vol) |