Step |
Hyp |
Ref |
Expression |
1 |
|
elxr |
⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ) |
2 |
|
ioossre |
⊢ ( 𝐴 (,) +∞ ) ⊆ ℝ |
3 |
2
|
a1i |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 (,) +∞ ) ⊆ ℝ ) |
4 |
|
elpwi |
⊢ ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ ) |
5 |
|
simplrl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑥 ⊆ ℝ ) |
6 |
|
simplrr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) → ( vol* ‘ 𝑥 ) ∈ ℝ ) |
7 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ ) |
8 |
|
eqid |
⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) |
9 |
8
|
ovolgelb |
⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) |
10 |
5 6 7 9
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) |
11 |
|
eqid |
⊢ ( 𝐴 (,) +∞ ) = ( 𝐴 (,) +∞ ) |
12 |
|
simplll |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) ) → 𝐴 ∈ ℝ ) |
13 |
5
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) ) → 𝑥 ⊆ ℝ ) |
14 |
6
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) ) → ( vol* ‘ 𝑥 ) ∈ ℝ ) |
15 |
|
simplr |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) ) → 𝑦 ∈ ℝ+ ) |
16 |
|
eqid |
⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑚 ∈ ℕ ↦ 〈 if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) 〉 ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑚 ∈ ℕ ↦ 〈 if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) 〉 ) ) ) |
17 |
|
eqid |
⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑚 ∈ ℕ ↦ 〈 ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) 〉 ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑚 ∈ ℕ ↦ 〈 ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) 〉 ) ) ) |
18 |
|
simprl |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) ) → 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) |
19 |
|
elovolmlem |
⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
20 |
18 19
|
sylib |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
21 |
|
simprrl |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) ) → 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) |
22 |
|
simprrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) |
23 |
|
eqid |
⊢ ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) |
24 |
|
eqid |
⊢ ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) |
25 |
|
2fveq3 |
⊢ ( 𝑚 = 𝑛 → ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) = ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) |
26 |
25
|
breq1d |
⊢ ( 𝑚 = 𝑛 → ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 ↔ ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 ) ) |
27 |
26 25
|
ifbieq2d |
⊢ ( 𝑚 = 𝑛 → if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) = if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) |
28 |
|
2fveq3 |
⊢ ( 𝑚 = 𝑛 → ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) |
29 |
27 28
|
breq12d |
⊢ ( 𝑚 = 𝑛 → ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ↔ if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) |
30 |
29 27 28
|
ifbieq12d |
⊢ ( 𝑚 = 𝑛 → if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) = if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) |
31 |
30 28
|
opeq12d |
⊢ ( 𝑚 = 𝑛 → 〈 if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) 〉 = 〈 if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) 〉 ) |
32 |
31
|
cbvmptv |
⊢ ( 𝑚 ∈ ℕ ↦ 〈 if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) 〉 ) = ( 𝑛 ∈ ℕ ↦ 〈 if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) 〉 ) |
33 |
25 30
|
opeq12d |
⊢ ( 𝑚 = 𝑛 → 〈 ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) 〉 = 〈 ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) 〉 ) |
34 |
33
|
cbvmptv |
⊢ ( 𝑚 ∈ ℕ ↦ 〈 ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) 〉 ) = ( 𝑛 ∈ ℕ ↦ 〈 ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) 〉 ) |
35 |
11 12 13 14 15 8 16 17 20 21 22 23 24 32 34
|
ioombl1lem4 |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) ) → ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) |
36 |
10 35
|
rexlimddv |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) |
37 |
36
|
ralrimiva |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ∀ 𝑦 ∈ ℝ+ ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) |
38 |
|
inss1 |
⊢ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ⊆ 𝑥 |
39 |
|
ovolsscl |
⊢ ( ( ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) ∈ ℝ ) |
40 |
38 39
|
mp3an1 |
⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) ∈ ℝ ) |
41 |
40
|
adantl |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) ∈ ℝ ) |
42 |
|
difss |
⊢ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ⊆ 𝑥 |
43 |
|
ovolsscl |
⊢ ( ( ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ∈ ℝ ) |
44 |
42 43
|
mp3an1 |
⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ∈ ℝ ) |
45 |
44
|
adantl |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ∈ ℝ ) |
46 |
41 45
|
readdcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ∈ ℝ ) |
47 |
|
simprr |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ 𝑥 ) ∈ ℝ ) |
48 |
|
alrple |
⊢ ( ( ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ∈ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( vol* ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ℝ+ ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) |
49 |
46 47 48
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( vol* ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ℝ+ ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( ( vol* ‘ 𝑥 ) + 𝑦 ) ) ) |
50 |
37 49
|
mpbird |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( vol* ‘ 𝑥 ) ) |
51 |
50
|
expr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ⊆ ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) |
52 |
4 51
|
sylan2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ 𝒫 ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) |
53 |
52
|
ralrimiva |
⊢ ( 𝐴 ∈ ℝ → ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) |
54 |
|
ismbl2 |
⊢ ( ( 𝐴 (,) +∞ ) ∈ dom vol ↔ ( ( 𝐴 (,) +∞ ) ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥 ∩ ( 𝐴 (,) +∞ ) ) ) + ( vol* ‘ ( 𝑥 ∖ ( 𝐴 (,) +∞ ) ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) ) |
55 |
3 53 54
|
sylanbrc |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 (,) +∞ ) ∈ dom vol ) |
56 |
|
oveq1 |
⊢ ( 𝐴 = +∞ → ( 𝐴 (,) +∞ ) = ( +∞ (,) +∞ ) ) |
57 |
|
iooid |
⊢ ( +∞ (,) +∞ ) = ∅ |
58 |
56 57
|
eqtrdi |
⊢ ( 𝐴 = +∞ → ( 𝐴 (,) +∞ ) = ∅ ) |
59 |
|
0mbl |
⊢ ∅ ∈ dom vol |
60 |
58 59
|
eqeltrdi |
⊢ ( 𝐴 = +∞ → ( 𝐴 (,) +∞ ) ∈ dom vol ) |
61 |
|
oveq1 |
⊢ ( 𝐴 = -∞ → ( 𝐴 (,) +∞ ) = ( -∞ (,) +∞ ) ) |
62 |
|
ioomax |
⊢ ( -∞ (,) +∞ ) = ℝ |
63 |
61 62
|
eqtrdi |
⊢ ( 𝐴 = -∞ → ( 𝐴 (,) +∞ ) = ℝ ) |
64 |
|
rembl |
⊢ ℝ ∈ dom vol |
65 |
63 64
|
eqeltrdi |
⊢ ( 𝐴 = -∞ → ( 𝐴 (,) +∞ ) ∈ dom vol ) |
66 |
55 60 65
|
3jaoi |
⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) → ( 𝐴 (,) +∞ ) ∈ dom vol ) |
67 |
1 66
|
sylbi |
⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 (,) +∞ ) ∈ dom vol ) |