Proof of Theorem ismbl2
| Step | Hyp | Ref
| Expression |
| 1 | | ismbl 25561 |
. 2
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))))) |
| 2 | | elpwi 4607 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 ℝ →
𝑥 ⊆
ℝ) |
| 3 | | inundif 4479 |
. . . . . . . . . 10
⊢ ((𝑥 ∩ 𝐴) ∪ (𝑥 ∖ 𝐴)) = 𝑥 |
| 4 | 3 | fveq2i 6909 |
. . . . . . . . 9
⊢
(vol*‘((𝑥
∩ 𝐴) ∪ (𝑥 ∖ 𝐴))) = (vol*‘𝑥) |
| 5 | | inss1 4237 |
. . . . . . . . . . 11
⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥 |
| 6 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → 𝑥 ⊆
ℝ) |
| 7 | 5, 6 | sstrid 3995 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (𝑥 ∩
𝐴) ⊆
ℝ) |
| 8 | | ovolsscl 25521 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∩ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∩ 𝐴)) ∈
ℝ) |
| 9 | 5, 8 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
| 10 | 9 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
| 11 | | difss 4136 |
. . . . . . . . . . 11
⊢ (𝑥 ∖ 𝐴) ⊆ 𝑥 |
| 12 | 11, 6 | sstrid 3995 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (𝑥 ∖
𝐴) ⊆
ℝ) |
| 13 | | ovolsscl 25521 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∖ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∖
𝐴)) ∈
ℝ) |
| 14 | 11, 13 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) |
| 15 | 14 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) |
| 16 | | ovolun 25534 |
. . . . . . . . . 10
⊢ ((((𝑥 ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) ∧ ((𝑥 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ)) →
(vol*‘((𝑥 ∩ 𝐴) ∪ (𝑥 ∖ 𝐴))) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
| 17 | 7, 10, 12, 15, 16 | syl22anc 839 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘((𝑥 ∩ 𝐴) ∪ (𝑥 ∖ 𝐴))) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
| 18 | 4, 17 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘𝑥) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
| 19 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘𝑥) ∈ ℝ) |
| 20 | 10, 15 | readdcld 11290 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ∈ ℝ) |
| 21 | 19, 20 | letri3d 11403 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ↔ ((vol*‘𝑥) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ∧ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
| 22 | 18, 21 | mpbirand 707 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ↔ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) |
| 23 | 22 | expr 456 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ⊆ ℝ) →
((vol*‘𝑥) ∈
ℝ → ((vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ↔ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
| 24 | 23 | pm5.74d 273 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ⊆ ℝ) →
(((vol*‘𝑥) ∈
ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) ↔ ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
| 25 | 2, 24 | sylan2 593 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝒫 ℝ)
→ (((vol*‘𝑥)
∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) ↔ ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
| 26 | 25 | ralbidva 3176 |
. . 3
⊢ (𝐴 ⊆ ℝ →
(∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) ↔ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ →
((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
| 27 | 26 | pm5.32i 574 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))))) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
| 28 | 1, 27 | bitri 275 |
1
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |