| Step | Hyp | Ref
| Expression |
| 1 | | elxr 13158 |
. 2
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
| 2 | | ioossre 13448 |
. . . . 5
⊢ (𝐴(,)+∞) ⊆
ℝ |
| 3 | 2 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℝ → (𝐴(,)+∞) ⊆
ℝ) |
| 4 | | elpwi 4607 |
. . . . . 6
⊢ (𝑥 ∈ 𝒫 ℝ →
𝑥 ⊆
ℝ) |
| 5 | | simplrl 777 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) → 𝑥 ⊆ ℝ) |
| 6 | | simplrr 778 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) → (vol*‘𝑥) ∈ ℝ) |
| 7 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) → 𝑦 ∈ ℝ+) |
| 8 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
| 9 | 8 | ovolgelb 25515 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ ∧ 𝑦 ∈
ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦))) |
| 10 | 5, 6, 7, 9 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦))) |
| 11 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐴(,)+∞) = (𝐴(,)+∞) |
| 12 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝐴 ∈ ℝ) |
| 13 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝑥 ⊆ ℝ) |
| 14 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → (vol*‘𝑥) ∈
ℝ) |
| 15 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝑦 ∈ ℝ+) |
| 16 | | eqid 2737 |
. . . . . . . . . . 11
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑚 ∈ ℕ ↦
〈if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))〉))) = seq1( + , ((abs ∘ −
) ∘ (𝑚 ∈ ℕ
↦ 〈if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))〉))) |
| 17 | | eqid 2737 |
. . . . . . . . . . 11
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑚 ∈ ℕ ↦ 〈(1st
‘(𝑓‘𝑚)), if(if((1st
‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚)))〉))) = seq1( + , ((abs ∘
− ) ∘ (𝑚 ∈
ℕ ↦ 〈(1st ‘(𝑓‘𝑚)), if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚)))〉))) |
| 18 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) |
| 19 | | elovolmlem 25509 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ↔ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
| 20 | 18, 19 | sylib 218 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
| 21 | | simprrl 781 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → 𝑥 ⊆ ∪ ran
((,) ∘ 𝑓)) |
| 22 | | simprrr 782 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → sup(ran seq1( + ,
((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)) |
| 23 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(1st ‘(𝑓‘𝑛)) = (1st ‘(𝑓‘𝑛)) |
| 24 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(2nd ‘(𝑓‘𝑛)) = (2nd ‘(𝑓‘𝑛)) |
| 25 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → (1st ‘(𝑓‘𝑚)) = (1st ‘(𝑓‘𝑛))) |
| 26 | 25 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑛 → ((1st ‘(𝑓‘𝑚)) ≤ 𝐴 ↔ (1st ‘(𝑓‘𝑛)) ≤ 𝐴)) |
| 27 | 26, 25 | ifbieq2d 4552 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) = if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛)))) |
| 28 | | 2fveq3 6911 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (2nd ‘(𝑓‘𝑚)) = (2nd ‘(𝑓‘𝑛))) |
| 29 | 27, 28 | breq12d 5156 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)) ↔ if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)))) |
| 30 | 29, 27, 28 | ifbieq12d 4554 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))) = if(if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛)))) |
| 31 | 30, 28 | opeq12d 4881 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → 〈if(if((1st
‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))〉 = 〈if(if((1st
‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛))〉) |
| 32 | 31 | cbvmptv 5255 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ ↦
〈if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚))〉) = (𝑛 ∈ ℕ ↦
〈if(if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛))〉) |
| 33 | 25, 30 | opeq12d 4881 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → 〈(1st ‘(𝑓‘𝑚)), if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚)))〉 = 〈(1st
‘(𝑓‘𝑛)), if(if((1st
‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛)))〉) |
| 34 | 33 | cbvmptv 5255 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ ↦
〈(1st ‘(𝑓‘𝑚)), if(if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))) ≤ (2nd ‘(𝑓‘𝑚)), if((1st ‘(𝑓‘𝑚)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑚))), (2nd ‘(𝑓‘𝑚)))〉) = (𝑛 ∈ ℕ ↦ 〈(1st
‘(𝑓‘𝑛)), if(if((1st
‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))) ≤ (2nd ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ 𝐴, 𝐴, (1st ‘(𝑓‘𝑛))), (2nd ‘(𝑓‘𝑛)))〉) |
| 35 | 11, 12, 13, 14, 15, 8, 16, 17, 20, 21, 22, 23, 24, 32, 34 | ioombl1lem4 25596 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ∧ (𝑥 ⊆ ∪ ran
((,) ∘ 𝑓) ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤
((vol*‘𝑥) + 𝑦)))) → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ ((vol*‘𝑥) + 𝑦)) |
| 36 | 10, 35 | rexlimddv 3161 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) ∧ 𝑦 ∈
ℝ+) → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ ((vol*‘𝑥) + 𝑦)) |
| 37 | 36 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ∀𝑦
∈ ℝ+ ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ ((vol*‘𝑥) + 𝑦)) |
| 38 | | inss1 4237 |
. . . . . . . . . . . 12
⊢ (𝑥 ∩ (𝐴(,)+∞)) ⊆ 𝑥 |
| 39 | | ovolsscl 25521 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∩ (𝐴(,)+∞)) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∩ (𝐴(,)+∞))) ∈
ℝ) |
| 40 | 38, 39 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ (𝐴(,)+∞))) ∈
ℝ) |
| 41 | 40 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∩ (𝐴(,)+∞))) ∈
ℝ) |
| 42 | | difss 4136 |
. . . . . . . . . . . 12
⊢ (𝑥 ∖ (𝐴(,)+∞)) ⊆ 𝑥 |
| 43 | | ovolsscl 25521 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∖ (𝐴(,)+∞)) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∖
(𝐴(,)+∞))) ∈
ℝ) |
| 44 | 42, 43 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ (𝐴(,)+∞))) ∈
ℝ) |
| 45 | 44 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∖ (𝐴(,)+∞))) ∈
ℝ) |
| 46 | 41, 45 | readdcld 11290 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ∈
ℝ) |
| 47 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘𝑥) ∈ ℝ) |
| 48 | | alrple 13248 |
. . . . . . . . 9
⊢
((((vol*‘(𝑥
∩ (𝐴(,)+∞))) +
(vol*‘(𝑥 ∖
(𝐴(,)+∞)))) ∈
ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥) ↔ ∀𝑦 ∈ ℝ+
((vol*‘(𝑥 ∩
(𝐴(,)+∞))) +
(vol*‘(𝑥 ∖
(𝐴(,)+∞)))) ≤
((vol*‘𝑥) + 𝑦))) |
| 49 | 46, 47, 48 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥) ↔ ∀𝑦 ∈ ℝ+
((vol*‘(𝑥 ∩
(𝐴(,)+∞))) +
(vol*‘(𝑥 ∖
(𝐴(,)+∞)))) ≤
((vol*‘𝑥) + 𝑦))) |
| 50 | 37, 49 | mpbird 257 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥)) |
| 51 | 50 | expr 456 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ⊆ ℝ) →
((vol*‘𝑥) ∈
ℝ → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥))) |
| 52 | 4, 51 | sylan2 593 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝒫 ℝ)
→ ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥))) |
| 53 | 52 | ralrimiva 3146 |
. . . 4
⊢ (𝐴 ∈ ℝ →
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴(,)+∞))) + (vol*‘(𝑥 ∖ (𝐴(,)+∞)))) ≤ (vol*‘𝑥))) |
| 54 | | ismbl2 25562 |
. . . 4
⊢ ((𝐴(,)+∞) ∈ dom vol
↔ ((𝐴(,)+∞)
⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ →
((vol*‘(𝑥 ∩
(𝐴(,)+∞))) +
(vol*‘(𝑥 ∖
(𝐴(,)+∞)))) ≤
(vol*‘𝑥)))) |
| 55 | 3, 53, 54 | sylanbrc 583 |
. . 3
⊢ (𝐴 ∈ ℝ → (𝐴(,)+∞) ∈ dom
vol) |
| 56 | | oveq1 7438 |
. . . . 5
⊢ (𝐴 = +∞ → (𝐴(,)+∞) =
(+∞(,)+∞)) |
| 57 | | iooid 13415 |
. . . . 5
⊢
(+∞(,)+∞) = ∅ |
| 58 | 56, 57 | eqtrdi 2793 |
. . . 4
⊢ (𝐴 = +∞ → (𝐴(,)+∞) =
∅) |
| 59 | | 0mbl 25574 |
. . . 4
⊢ ∅
∈ dom vol |
| 60 | 58, 59 | eqeltrdi 2849 |
. . 3
⊢ (𝐴 = +∞ → (𝐴(,)+∞) ∈ dom
vol) |
| 61 | | oveq1 7438 |
. . . . 5
⊢ (𝐴 = -∞ → (𝐴(,)+∞) =
(-∞(,)+∞)) |
| 62 | | ioomax 13462 |
. . . . 5
⊢
(-∞(,)+∞) = ℝ |
| 63 | 61, 62 | eqtrdi 2793 |
. . . 4
⊢ (𝐴 = -∞ → (𝐴(,)+∞) =
ℝ) |
| 64 | | rembl 25575 |
. . . 4
⊢ ℝ
∈ dom vol |
| 65 | 63, 64 | eqeltrdi 2849 |
. . 3
⊢ (𝐴 = -∞ → (𝐴(,)+∞) ∈ dom
vol) |
| 66 | 55, 60, 65 | 3jaoi 1430 |
. 2
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐴(,)+∞) ∈ dom
vol) |
| 67 | 1, 66 | sylbi 217 |
1
⊢ (𝐴 ∈ ℝ*
→ (𝐴(,)+∞)
∈ dom vol) |