Step |
Hyp |
Ref |
Expression |
1 |
|
ismbl |
⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) ) |
2 |
|
elpwi |
⊢ ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ ) |
3 |
|
inundif |
⊢ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∖ 𝐴 ) ) = 𝑥 |
4 |
3
|
fveq2i |
⊢ ( vol* ‘ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∖ 𝐴 ) ) ) = ( vol* ‘ 𝑥 ) |
5 |
|
inss1 |
⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 |
6 |
|
simprl |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → 𝑥 ⊆ ℝ ) |
7 |
5 6
|
sstrid |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( 𝑥 ∩ 𝐴 ) ⊆ ℝ ) |
8 |
|
ovolsscl |
⊢ ( ( ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ ) |
9 |
5 8
|
mp3an1 |
⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ ) |
10 |
9
|
adantl |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ ) |
11 |
|
difss |
⊢ ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥 |
12 |
11 6
|
sstrid |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( 𝑥 ∖ 𝐴 ) ⊆ ℝ ) |
13 |
|
ovolsscl |
⊢ ( ( ( 𝑥 ∖ 𝐴 ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ ) |
14 |
11 13
|
mp3an1 |
⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ ) |
15 |
14
|
adantl |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ ) |
16 |
|
ovolun |
⊢ ( ( ( ( 𝑥 ∩ 𝐴 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) ∈ ℝ ) ∧ ( ( 𝑥 ∖ 𝐴 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) |
17 |
7 10 12 15 16
|
syl22anc |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) |
18 |
4 17
|
eqbrtrrid |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ 𝑥 ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) |
19 |
|
simprr |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ 𝑥 ) ∈ ℝ ) |
20 |
10 15
|
readdcld |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ∈ ℝ ) |
21 |
19 20
|
letri3d |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ↔ ( ( vol* ‘ 𝑥 ) ≤ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ∧ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) |
22 |
18 21
|
mpbirand |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ↔ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) |
23 |
22
|
expr |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ⊆ ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ↔ ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) |
24 |
23
|
pm5.74d |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ⊆ ℝ ) → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) |
25 |
2 24
|
sylan2 |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝒫 ℝ ) → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) |
26 |
25
|
ralbidva |
⊢ ( 𝐴 ⊆ ℝ → ( ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) |
27 |
26
|
pm5.32i |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) |
28 |
1 27
|
bitri |
⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) |