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*‘𝑥)))) |