Step |
Hyp |
Ref |
Expression |
1 |
|
simpll |
⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ) |
2 |
|
simplr |
⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) |
3 |
|
simpr |
⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ ) |
4 |
1 2 3
|
ovolunlem2 |
⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) ∧ 𝑥 ∈ ℝ+ ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝑥 ) ) |
5 |
4
|
ralrimiva |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ ℝ+ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝑥 ) ) |
6 |
|
unss |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ℝ ) |
7 |
6
|
biimpi |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) → ( 𝐴 ∪ 𝐵 ) ⊆ ℝ ) |
8 |
7
|
ad2ant2r |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( 𝐴 ∪ 𝐵 ) ⊆ ℝ ) |
9 |
|
ovolcl |
⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ℝ → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ* ) |
10 |
8 9
|
syl |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ* ) |
11 |
|
readdcl |
⊢ ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ ) |
12 |
11
|
ad2ant2l |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ ) |
13 |
|
xralrple |
⊢ ( ( ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ* ∧ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ ) → ( ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ↔ ∀ 𝑥 ∈ ℝ+ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝑥 ) ) ) |
14 |
10 12 13
|
syl2anc |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ↔ ∀ 𝑥 ∈ ℝ+ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝑥 ) ) ) |
15 |
5 14
|
mpbird |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) |