Step | Hyp | Ref
| Expression |
1 | | 1rp 12117 |
. . . . 5
⊢ 1 ∈
ℝ+ |
2 | 1 | ne0ii 4154 |
. . . 4
⊢
ℝ+ ≠ ∅ |
3 | | r19.2z 4283 |
. . . 4
⊢
((ℝ+ ≠ ∅ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥)) → ∃𝑥 ∈ ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥)) |
4 | 2, 3 | mpan 683 |
. . 3
⊢
(∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) → ∃𝑥 ∈ ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥)) |
5 | | simprl 789 |
. . . . . 6
⊢ ((𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥)) → 𝐴 ⊆ 𝑦) |
6 | | mblss 23698 |
. . . . . . 7
⊢ (𝑦 ∈ dom vol → 𝑦 ⊆
ℝ) |
7 | 6 | adantr 474 |
. . . . . 6
⊢ ((𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥)) → 𝑦 ⊆ ℝ) |
8 | 5, 7 | sstrd 3838 |
. . . . 5
⊢ ((𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥)) → 𝐴 ⊆ ℝ) |
9 | 8 | rexlimiva 3238 |
. . . 4
⊢
(∃𝑦 ∈ dom
vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) → 𝐴 ⊆ ℝ) |
10 | 9 | rexlimivw 3239 |
. . 3
⊢
(∃𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) → 𝐴 ⊆ ℝ) |
11 | 4, 10 | syl 17 |
. 2
⊢
(∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) → 𝐴 ⊆ ℝ) |
12 | | inss1 4058 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∩ 𝐴) ⊆ 𝑧 |
13 | 12 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) → (𝑧 ∩
𝐴) ⊆ 𝑧) |
14 | | elpwi 4389 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝒫 ℝ →
𝑧 ⊆
ℝ) |
15 | 14 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) → 𝑧 ⊆
ℝ) |
16 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) → (vol*‘𝑧) ∈ ℝ) |
17 | | ovolsscl 23653 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∩ 𝐴) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ) →
(vol*‘(𝑧 ∩ 𝐴)) ∈
ℝ) |
18 | 13, 15, 16, 17 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) → (vol*‘(𝑧 ∩ 𝐴)) ∈ ℝ) |
19 | | difssd 3966 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) → (𝑧 ∖
𝐴) ⊆ 𝑧) |
20 | | ovolsscl 23653 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∖ 𝐴) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ) →
(vol*‘(𝑧 ∖
𝐴)) ∈
ℝ) |
21 | 19, 15, 16, 20 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) → (vol*‘(𝑧 ∖ 𝐴)) ∈ ℝ) |
22 | 18, 21 | readdcld 10387 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ∈ ℝ) |
23 | 22 | ad2antrr 719 |
. . . . . . . . 9
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ∈ ℝ) |
24 | 16 | ad2antrr 719 |
. . . . . . . . . 10
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘𝑧) ∈ ℝ) |
25 | | difssd 3966 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (𝑦 ∖ 𝐴) ⊆ 𝑦) |
26 | 7 | adantl 475 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → 𝑦 ⊆ ℝ) |
27 | | rpre 12121 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
28 | 27 | ad2antlr 720 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → 𝑥 ∈ ℝ) |
29 | | simprrr 802 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘𝑦) ≤ 𝑥) |
30 | | ovollecl 23650 |
. . . . . . . . . . . 12
⊢ ((𝑦 ⊆ ℝ ∧ 𝑥 ∈ ℝ ∧
(vol*‘𝑦) ≤ 𝑥) → (vol*‘𝑦) ∈
ℝ) |
31 | 26, 28, 29, 30 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘𝑦) ∈ ℝ) |
32 | | ovolsscl 23653 |
. . . . . . . . . . 11
⊢ (((𝑦 ∖ 𝐴) ⊆ 𝑦 ∧ 𝑦 ⊆ ℝ ∧ (vol*‘𝑦) ∈ ℝ) →
(vol*‘(𝑦 ∖
𝐴)) ∈
ℝ) |
33 | 25, 26, 31, 32 | syl3anc 1496 |
. . . . . . . . . 10
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑦 ∖ 𝐴)) ∈ ℝ) |
34 | 24, 33 | readdcld 10387 |
. . . . . . . . 9
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((vol*‘𝑧) + (vol*‘(𝑦 ∖ 𝐴))) ∈ ℝ) |
35 | 24, 28 | readdcld 10387 |
. . . . . . . . 9
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((vol*‘𝑧) + 𝑥) ∈ ℝ) |
36 | 18 | ad2antrr 719 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑧 ∩ 𝐴)) ∈ ℝ) |
37 | 21 | ad2antrr 719 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑧 ∖ 𝐴)) ∈ ℝ) |
38 | | inss1 4058 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∩ 𝑦) ⊆ 𝑧 |
39 | 38 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (𝑧 ∩ 𝑦) ⊆ 𝑧) |
40 | 15 | ad2antrr 719 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → 𝑧 ⊆ ℝ) |
41 | | ovolsscl 23653 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∩ 𝑦) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ) →
(vol*‘(𝑧 ∩ 𝑦)) ∈
ℝ) |
42 | 39, 40, 24, 41 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑧 ∩ 𝑦)) ∈ ℝ) |
43 | | difssd 3966 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (𝑧 ∖ 𝑦) ⊆ 𝑧) |
44 | | ovolsscl 23653 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∖ 𝑦) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ) →
(vol*‘(𝑧 ∖
𝑦)) ∈
ℝ) |
45 | 43, 40, 24, 44 | syl3anc 1496 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑧 ∖ 𝑦)) ∈ ℝ) |
46 | 45, 33 | readdcld 10387 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((vol*‘(𝑧 ∖ 𝑦)) + (vol*‘(𝑦 ∖ 𝐴))) ∈ ℝ) |
47 | | simprrl 801 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → 𝐴 ⊆ 𝑦) |
48 | | sslin 4064 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝑦 → (𝑧 ∩ 𝐴) ⊆ (𝑧 ∩ 𝑦)) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (𝑧 ∩ 𝐴) ⊆ (𝑧 ∩ 𝑦)) |
50 | 38, 40 | syl5ss 3839 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (𝑧 ∩ 𝑦) ⊆ ℝ) |
51 | | ovolss 23652 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∩ 𝐴) ⊆ (𝑧 ∩ 𝑦) ∧ (𝑧 ∩ 𝑦) ⊆ ℝ) → (vol*‘(𝑧 ∩ 𝐴)) ≤ (vol*‘(𝑧 ∩ 𝑦))) |
52 | 49, 50, 51 | syl2anc 581 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑧 ∩ 𝐴)) ≤ (vol*‘(𝑧 ∩ 𝑦))) |
53 | 40 | ssdifssd 3976 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (𝑧 ∖ 𝑦) ⊆ ℝ) |
54 | 26 | ssdifssd 3976 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (𝑦 ∖ 𝐴) ⊆ ℝ) |
55 | 53, 54 | unssd 4017 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴)) ⊆ ℝ) |
56 | | ovolun 23666 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∖ 𝑦) ⊆ ℝ ∧ (vol*‘(𝑧 ∖ 𝑦)) ∈ ℝ) ∧ ((𝑦 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑦 ∖ 𝐴)) ∈ ℝ)) →
(vol*‘((𝑧 ∖
𝑦) ∪ (𝑦 ∖ 𝐴))) ≤ ((vol*‘(𝑧 ∖ 𝑦)) + (vol*‘(𝑦 ∖ 𝐴)))) |
57 | 53, 45, 54, 33, 56 | syl22anc 874 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴))) ≤ ((vol*‘(𝑧 ∖ 𝑦)) + (vol*‘(𝑦 ∖ 𝐴)))) |
58 | | ovollecl 23650 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴)) ⊆ ℝ ∧ ((vol*‘(𝑧 ∖ 𝑦)) + (vol*‘(𝑦 ∖ 𝐴))) ∈ ℝ ∧ (vol*‘((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴))) ≤ ((vol*‘(𝑧 ∖ 𝑦)) + (vol*‘(𝑦 ∖ 𝐴)))) → (vol*‘((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴))) ∈ ℝ) |
59 | 55, 46, 57, 58 | syl3anc 1496 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴))) ∈ ℝ) |
60 | | ssun1 4004 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ⊆ (𝑧 ∪ 𝑦) |
61 | | undif1 4267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∖ 𝑦) ∪ 𝑦) = (𝑧 ∪ 𝑦) |
62 | 60, 61 | sseqtr4i 3864 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ⊆ ((𝑧 ∖ 𝑦) ∪ 𝑦) |
63 | | ssdif 3973 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ⊆ ((𝑧 ∖ 𝑦) ∪ 𝑦) → (𝑧 ∖ 𝐴) ⊆ (((𝑧 ∖ 𝑦) ∪ 𝑦) ∖ 𝐴)) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∖ 𝐴) ⊆ (((𝑧 ∖ 𝑦) ∪ 𝑦) ∖ 𝐴) |
65 | | difundir 4111 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∖ 𝑦) ∪ 𝑦) ∖ 𝐴) = (((𝑧 ∖ 𝑦) ∖ 𝐴) ∪ (𝑦 ∖ 𝐴)) |
66 | 64, 65 | sseqtri 3863 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∖ 𝐴) ⊆ (((𝑧 ∖ 𝑦) ∖ 𝐴) ∪ (𝑦 ∖ 𝐴)) |
67 | | difun1 4118 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∖ (𝑦 ∪ 𝐴)) = ((𝑧 ∖ 𝑦) ∖ 𝐴) |
68 | | ssequn2 4014 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ⊆ 𝑦 ↔ (𝑦 ∪ 𝐴) = 𝑦) |
69 | 47, 68 | sylib 210 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (𝑦 ∪ 𝐴) = 𝑦) |
70 | 69 | difeq2d 3956 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (𝑧 ∖ (𝑦 ∪ 𝐴)) = (𝑧 ∖ 𝑦)) |
71 | 67, 70 | syl5eqr 2876 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((𝑧 ∖ 𝑦) ∖ 𝐴) = (𝑧 ∖ 𝑦)) |
72 | 71 | uneq1d 3994 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (((𝑧 ∖ 𝑦) ∖ 𝐴) ∪ (𝑦 ∖ 𝐴)) = ((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴))) |
73 | 66, 72 | syl5sseq 3879 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (𝑧 ∖ 𝐴) ⊆ ((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴))) |
74 | | ovolss 23652 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∖ 𝐴) ⊆ ((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴)) ∧ ((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴)) ⊆ ℝ) →
(vol*‘(𝑧 ∖
𝐴)) ≤
(vol*‘((𝑧 ∖
𝑦) ∪ (𝑦 ∖ 𝐴)))) |
75 | 73, 55, 74 | syl2anc 581 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑧 ∖ 𝐴)) ≤ (vol*‘((𝑧 ∖ 𝑦) ∪ (𝑦 ∖ 𝐴)))) |
76 | 37, 59, 46, 75, 57 | letrd 10514 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑧 ∖ 𝐴)) ≤ ((vol*‘(𝑧 ∖ 𝑦)) + (vol*‘(𝑦 ∖ 𝐴)))) |
77 | 36, 37, 42, 46, 52, 76 | le2addd 10972 |
. . . . . . . . . 10
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ ((vol*‘(𝑧 ∩ 𝑦)) + ((vol*‘(𝑧 ∖ 𝑦)) + (vol*‘(𝑦 ∖ 𝐴))))) |
78 | | simprl 789 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → 𝑦 ∈ dom vol) |
79 | | mblsplit 23699 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ dom vol ∧ 𝑧 ⊆ ℝ ∧
(vol*‘𝑧) ∈
ℝ) → (vol*‘𝑧) = ((vol*‘(𝑧 ∩ 𝑦)) + (vol*‘(𝑧 ∖ 𝑦)))) |
80 | 78, 40, 24, 79 | syl3anc 1496 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘𝑧) = ((vol*‘(𝑧 ∩ 𝑦)) + (vol*‘(𝑧 ∖ 𝑦)))) |
81 | 80 | oveq1d 6921 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((vol*‘𝑧) + (vol*‘(𝑦 ∖ 𝐴))) = (((vol*‘(𝑧 ∩ 𝑦)) + (vol*‘(𝑧 ∖ 𝑦))) + (vol*‘(𝑦 ∖ 𝐴)))) |
82 | 42 | recnd 10386 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑧 ∩ 𝑦)) ∈ ℂ) |
83 | 45 | recnd 10386 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑧 ∖ 𝑦)) ∈ ℂ) |
84 | 33 | recnd 10386 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑦 ∖ 𝐴)) ∈ ℂ) |
85 | 82, 83, 84 | addassd 10380 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (((vol*‘(𝑧 ∩ 𝑦)) + (vol*‘(𝑧 ∖ 𝑦))) + (vol*‘(𝑦 ∖ 𝐴))) = ((vol*‘(𝑧 ∩ 𝑦)) + ((vol*‘(𝑧 ∖ 𝑦)) + (vol*‘(𝑦 ∖ 𝐴))))) |
86 | 81, 85 | eqtrd 2862 |
. . . . . . . . . 10
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((vol*‘𝑧) + (vol*‘(𝑦 ∖ 𝐴))) = ((vol*‘(𝑧 ∩ 𝑦)) + ((vol*‘(𝑧 ∖ 𝑦)) + (vol*‘(𝑦 ∖ 𝐴))))) |
87 | 77, 86 | breqtrrd 4902 |
. . . . . . . . 9
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ ((vol*‘𝑧) + (vol*‘(𝑦 ∖ 𝐴)))) |
88 | | difss 3965 |
. . . . . . . . . . . 12
⊢ (𝑦 ∖ 𝐴) ⊆ 𝑦 |
89 | | ovolss 23652 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∖ 𝐴) ⊆ 𝑦 ∧ 𝑦 ⊆ ℝ) → (vol*‘(𝑦 ∖ 𝐴)) ≤ (vol*‘𝑦)) |
90 | 88, 26, 89 | sylancr 583 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑦 ∖ 𝐴)) ≤ (vol*‘𝑦)) |
91 | 33, 31, 28, 90, 29 | letrd 10514 |
. . . . . . . . . 10
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → (vol*‘(𝑦 ∖ 𝐴)) ≤ 𝑥) |
92 | 33, 28, 24, 91 | leadd2dd 10968 |
. . . . . . . . 9
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((vol*‘𝑧) + (vol*‘(𝑦 ∖ 𝐴))) ≤ ((vol*‘𝑧) + 𝑥)) |
93 | 23, 34, 35, 87, 92 | letrd 10514 |
. . . . . . . 8
⊢ ((((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ (𝑦 ∈ dom vol ∧ (𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥))) → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ ((vol*‘𝑧) + 𝑥)) |
94 | 93 | rexlimdvaa 3242 |
. . . . . . 7
⊢ (((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → (∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ ((vol*‘𝑧) + 𝑥))) |
95 | 94 | ralimdva 3172 |
. . . . . 6
⊢ ((𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ) → (∀𝑥
∈ ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) → ∀𝑥 ∈ ℝ+
((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ ((vol*‘𝑧) + 𝑥))) |
96 | 95 | impcom 398 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → ∀𝑥
∈ ℝ+ ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ ((vol*‘𝑧) + 𝑥)) |
97 | 22 | adantl 475 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ∈ ℝ) |
98 | 97 | rexrd 10407 |
. . . . . 6
⊢
((∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ∈
ℝ*) |
99 | | simprr 791 |
. . . . . 6
⊢
((∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (vol*‘𝑧) ∈ ℝ) |
100 | | xralrple 12325 |
. . . . . 6
⊢
((((vol*‘(𝑧
∩ 𝐴)) +
(vol*‘(𝑧 ∖
𝐴))) ∈
ℝ* ∧ (vol*‘𝑧) ∈ ℝ) → (((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ (vol*‘𝑧) ↔ ∀𝑥 ∈ ℝ+
((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ ((vol*‘𝑧) + 𝑥))) |
101 | 98, 99, 100 | syl2anc 581 |
. . . . 5
⊢
((∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → (((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ (vol*‘𝑧) ↔ ∀𝑥 ∈ ℝ+
((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ ((vol*‘𝑧) + 𝑥))) |
102 | 96, 101 | mpbird 249 |
. . . 4
⊢
((∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) ∧ (𝑧 ∈ 𝒫 ℝ ∧
(vol*‘𝑧) ∈
ℝ)) → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ (vol*‘𝑧)) |
103 | 102 | expr 450 |
. . 3
⊢
((∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) ∧ 𝑧 ∈ 𝒫 ℝ) →
((vol*‘𝑧) ∈
ℝ → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ (vol*‘𝑧))) |
104 | 103 | ralrimiva 3176 |
. 2
⊢
(∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) → ∀𝑧 ∈ 𝒫 ℝ((vol*‘𝑧) ∈ ℝ →
((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ (vol*‘𝑧))) |
105 | | ismbl2 23694 |
. 2
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧
∀𝑧 ∈ 𝒫
ℝ((vol*‘𝑧)
∈ ℝ → ((vol*‘(𝑧 ∩ 𝐴)) + (vol*‘(𝑧 ∖ 𝐴))) ≤ (vol*‘𝑧)))) |
106 | 11, 104, 105 | sylanbrc 580 |
1
⊢
(∀𝑥 ∈
ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) → 𝐴 ∈ dom vol) |