Proof of Theorem ismbl3
| Step | Hyp | Ref
| Expression |
| 1 | | ismbl2 25562 |
. 2
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
| 2 | | inss1 4237 |
. . . . . . . . . . . 12
⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥 |
| 3 | 2 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (𝑥 ∩
𝐴) ⊆ 𝑥) |
| 4 | | elpwi 4607 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 ℝ →
𝑥 ⊆
ℝ) |
| 5 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) ∈
ℝ) → 𝑥 ⊆
ℝ) |
| 6 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘𝑥) ∈ ℝ) |
| 7 | | ovolsscl 25521 |
. . . . . . . . . . 11
⊢ (((𝑥 ∩ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∩ 𝐴)) ∈
ℝ) |
| 8 | 3, 5, 6, 7 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
| 9 | | difssd 4137 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (𝑥 ∖
𝐴) ⊆ 𝑥) |
| 10 | | ovolsscl 25521 |
. . . . . . . . . . 11
⊢ (((𝑥 ∖ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∖
𝐴)) ∈
ℝ) |
| 11 | 9, 5, 6, 10 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) |
| 12 | 8, 11 | rexaddd 13276 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) ∈
ℝ) → ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
| 13 | 12 | adantlr 715 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘𝑥) ∈
ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) ∧ (vol*‘𝑥) ∈ ℝ) → ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
| 14 | | id 22 |
. . . . . . . . . 10
⊢
(((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) → ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) |
| 15 | 14 | imp 406 |
. . . . . . . . 9
⊢
((((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) ∧ (vol*‘𝑥) ∈ ℝ) → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) |
| 16 | 15 | adantll 714 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘𝑥) ∈
ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) ∧ (vol*‘𝑥) ∈ ℝ) → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) |
| 17 | 13, 16 | eqbrtrd 5165 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘𝑥) ∈
ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) ∧ (vol*‘𝑥) ∈ ℝ) → ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) |
| 18 | 2, 4 | sstrid 3995 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝒫 ℝ →
(𝑥 ∩ 𝐴) ⊆ ℝ) |
| 19 | | ovolcl 25513 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ 𝐴) ⊆ ℝ → (vol*‘(𝑥 ∩ 𝐴)) ∈
ℝ*) |
| 20 | 18, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 ℝ →
(vol*‘(𝑥 ∩ 𝐴)) ∈
ℝ*) |
| 21 | 4 | ssdifssd 4147 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝒫 ℝ →
(𝑥 ∖ 𝐴) ⊆
ℝ) |
| 22 | | ovolcl 25513 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∖ 𝐴) ⊆ ℝ → (vol*‘(𝑥 ∖ 𝐴)) ∈
ℝ*) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 ℝ →
(vol*‘(𝑥 ∖
𝐴)) ∈
ℝ*) |
| 24 | 20, 23 | xaddcld 13343 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 ℝ →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ∈
ℝ*) |
| 25 | | pnfge 13172 |
. . . . . . . . . . 11
⊢
(((vol*‘(𝑥
∩ 𝐴))
+𝑒 (vol*‘(𝑥 ∖ 𝐴))) ∈ ℝ* →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤
+∞) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝒫 ℝ →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤
+∞) |
| 27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
¬ (vol*‘𝑥) ∈
ℝ) → ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ +∞) |
| 28 | | ovolf 25517 |
. . . . . . . . . . . . 13
⊢
vol*:𝒫 ℝ⟶(0[,]+∞) |
| 29 | 28 | ffvelcdmi 7103 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 ℝ →
(vol*‘𝑥) ∈
(0[,]+∞)) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
¬ (vol*‘𝑥) ∈
ℝ) → (vol*‘𝑥) ∈ (0[,]+∞)) |
| 31 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
¬ (vol*‘𝑥) ∈
ℝ) → ¬ (vol*‘𝑥) ∈ ℝ) |
| 32 | | xrge0nre 13493 |
. . . . . . . . . . 11
⊢
(((vol*‘𝑥)
∈ (0[,]+∞) ∧ ¬ (vol*‘𝑥) ∈ ℝ) → (vol*‘𝑥) = +∞) |
| 33 | 30, 31, 32 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
¬ (vol*‘𝑥) ∈
ℝ) → (vol*‘𝑥) = +∞) |
| 34 | 33 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
¬ (vol*‘𝑥) ∈
ℝ) → +∞ = (vol*‘𝑥)) |
| 35 | 27, 34 | breqtrd 5169 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
¬ (vol*‘𝑥) ∈
ℝ) → ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) |
| 36 | 35 | adantlr 715 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘𝑥) ∈
ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) ∧ ¬ (vol*‘𝑥) ∈ ℝ) →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥)) |
| 37 | 17, 36 | pm2.61dan 813 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘𝑥) ∈
ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) → ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) |
| 38 | 37 | ex 412 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 ℝ →
(((vol*‘𝑥) ∈
ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) → ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) |
| 39 | 12 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) ∈
ℝ) → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) = ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴)))) |
| 40 | 39 | 3adant2 1132 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥) ∧ (vol*‘𝑥) ∈ ℝ) →
((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) = ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴)))) |
| 41 | | simp2 1138 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥) ∧ (vol*‘𝑥) ∈ ℝ) →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥)) |
| 42 | 40, 41 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥) ∧ (vol*‘𝑥) ∈ ℝ) →
((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) |
| 43 | 42 | 3exp 1120 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 ℝ →
(((vol*‘(𝑥 ∩
𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥) → ((vol*‘𝑥) ∈ ℝ →
((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
| 44 | 38, 43 | impbid 212 |
. . . 4
⊢ (𝑥 ∈ 𝒫 ℝ →
(((vol*‘𝑥) ∈
ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) ↔ ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) |
| 45 | 44 | ralbiia 3091 |
. . 3
⊢
(∀𝑥 ∈
𝒫 ℝ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) ↔ ∀𝑥 ∈ 𝒫 ℝ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) |
| 46 | 45 | anbi2i 623 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫
ℝ((vol*‘(𝑥
∩ 𝐴))
+𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) |
| 47 | 1, 46 | bitri 275 |
1
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘(𝑥
∩ 𝐴))
+𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) |