| Step | Hyp | Ref
| Expression |
| 1 | | ioof 13487 |
. . . . 5
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 2 | | uniioombl.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 3 | | inss2 4238 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 4 | | rexpssxrxp 11306 |
. . . . . . 7
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 5 | 3, 4 | sstri 3993 |
. . . . . 6
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 6 | | fss 6752 |
. . . . . 6
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 7 | 2, 5, 6 | sylancl 586 |
. . . . 5
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* ×
ℝ*)) |
| 8 | | fco 6760 |
. . . . 5
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝐹:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
| 9 | 1, 7, 8 | sylancr 587 |
. . . 4
⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫
ℝ) |
| 10 | 9 | frnd 6744 |
. . 3
⊢ (𝜑 → ran ((,) ∘ 𝐹) ⊆ 𝒫
ℝ) |
| 11 | | sspwuni 5100 |
. . 3
⊢ (ran ((,)
∘ 𝐹) ⊆
𝒫 ℝ ↔ ∪ ran ((,) ∘ 𝐹) ⊆
ℝ) |
| 12 | 10, 11 | sylib 218 |
. 2
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ) |
| 13 | | elpwi 4607 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝒫 ℝ →
𝑧 ⊆
ℝ) |
| 14 | 13 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → 𝑧 ⊆
ℝ) |
| 15 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (vol*‘𝑧) ∈ ℝ) |
| 16 | | rphalfcl 13062 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ+) |
| 17 | 16 | rphalfcld 13089 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
→ ((𝑟 / 2) / 2) ∈
ℝ+) |
| 18 | | eqid 2737 |
. . . . . . . . . 10
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
| 19 | 18 | ovolgelb 25515 |
. . . . . . . . 9
⊢ ((𝑧 ⊆ ℝ ∧
(vol*‘𝑧) ∈
ℝ ∧ ((𝑟 / 2) / 2)
∈ ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2)))) |
| 20 | 14, 15, 17, 19 | syl2an3an 1424 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2)))) |
| 21 | 2 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
| 22 | | uniioombl.2 |
. . . . . . . . . 10
⊢ (𝜑 → Disj 𝑥 ∈ ℕ
((,)‘(𝐹‘𝑥))) |
| 23 | 22 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) →
Disj 𝑥 ∈
ℕ ((,)‘(𝐹‘𝑥))) |
| 24 | | uniioombl.3 |
. . . . . . . . 9
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
| 25 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,)
∘ 𝐹) |
| 26 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → (vol*‘𝑧) ∈ ℝ) |
| 27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) →
(vol*‘𝑧) ∈
ℝ) |
| 28 | 16 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → (𝑟 / 2) ∈
ℝ+) |
| 29 | 28 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → (𝑟 / 2) ∈
ℝ+) |
| 30 | 29 | rphalfcld 13089 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → ((𝑟 / 2) / 2) ∈
ℝ+) |
| 31 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
| 32 | 31 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → 𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
| 33 | | simprrl 781 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → 𝑧 ⊆ ∪ ran ((,) ∘ 𝑓)) |
| 34 | | simprrr 782 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))) |
| 35 | 21, 23, 24, 25, 27, 30, 32, 33, 18, 34 | uniioombllem6 25623 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑧 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑧) + ((𝑟 / 2) / 2))))) →
((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹)))) ≤
((vol*‘𝑧) + (4
· ((𝑟 / 2) /
2)))) |
| 36 | 20, 35 | rexlimddv 3161 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + (4 · ((𝑟 / 2) / 2)))) |
| 37 | | rpcn 13045 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℂ) |
| 38 | 37 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 𝑟 ∈ ℂ) |
| 39 | | 2cnd 12344 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 2 ∈ ℂ) |
| 40 | | 2ne0 12370 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
| 41 | 40 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 2 ≠ 0) |
| 42 | 38, 39, 39, 41, 41 | divdiv1d 12074 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((𝑟 / 2) / 2) = (𝑟 / (2 · 2))) |
| 43 | | 2t2e4 12430 |
. . . . . . . . . . . 12
⊢ (2
· 2) = 4 |
| 44 | 43 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ (𝑟 / (2 · 2)) = (𝑟 / 4) |
| 45 | 42, 44 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((𝑟 / 2) / 2) = (𝑟 / 4)) |
| 46 | 45 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → (4 · ((𝑟 / 2) / 2)) = (4 · (𝑟 / 4))) |
| 47 | | 4cn 12351 |
. . . . . . . . . . 11
⊢ 4 ∈
ℂ |
| 48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 4 ∈ ℂ) |
| 49 | | 4ne0 12374 |
. . . . . . . . . . 11
⊢ 4 ≠
0 |
| 50 | 49 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → 4 ≠ 0) |
| 51 | 38, 48, 50 | divcan2d 12045 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → (4 · (𝑟 / 4)) = 𝑟) |
| 52 | 46, 51 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → (4 · ((𝑟 / 2) / 2)) = 𝑟) |
| 53 | 52 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((vol*‘𝑧) + (4 · ((𝑟 / 2) / 2))) = ((vol*‘𝑧) + 𝑟)) |
| 54 | 36, 53 | breqtrd 5169 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) ∧ 𝑟 ∈
ℝ+) → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + 𝑟)) |
| 55 | 54 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → ∀𝑟
∈ ℝ+ ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + 𝑟)) |
| 56 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝑧 ∩ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧 |
| 57 | 56 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (𝑧 ∩
∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧) |
| 58 | | ovolsscl 25521 |
. . . . . . . 8
⊢ (((𝑧 ∩ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ) →
(vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) ∈ ℝ) |
| 59 | 57, 14, 15, 58 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) ∈
ℝ) |
| 60 | | difssd 4137 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (𝑧 ∖
∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧) |
| 61 | | ovolsscl 25521 |
. . . . . . . 8
⊢ (((𝑧 ∖ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ) →
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹))) ∈ ℝ) |
| 62 | 60, 14, 15, 61 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹))) ∈
ℝ) |
| 63 | 59, 62 | readdcld 11290 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ∈ ℝ) |
| 64 | | alrple 13248 |
. . . . . 6
⊢
((((vol*‘(𝑧
∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹)))) ∈
ℝ ∧ (vol*‘𝑧) ∈ ℝ) → (((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹)))) ≤
(vol*‘𝑧) ↔
∀𝑟 ∈
ℝ+ ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + 𝑟))) |
| 65 | 63, 15, 64 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧) ↔ ∀𝑟 ∈ ℝ+
((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹)))) ≤
((vol*‘𝑧) + 𝑟))) |
| 66 | 55, 65 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧)) |
| 67 | 66 | expr 456 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 ℝ) →
((vol*‘𝑧) ∈
ℝ → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧))) |
| 68 | 67 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝒫 ℝ((vol*‘𝑧) ∈ ℝ →
((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran
((,) ∘ 𝐹)))) ≤
(vol*‘𝑧))) |
| 69 | | ismbl2 25562 |
. 2
⊢ (∪ ran ((,) ∘ 𝐹) ∈ dom vol ↔ (∪ ran ((,) ∘ 𝐹) ⊆ ℝ ∧ ∀𝑧 ∈ 𝒫
ℝ((vol*‘𝑧)
∈ ℝ → ((vol*‘(𝑧 ∩ ∪ ran ((,)
∘ 𝐹))) +
(vol*‘(𝑧 ∖
∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧)))) |
| 70 | 12, 68, 69 | sylanbrc 583 |
1
⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ∈ dom vol) |