Metamath Proof Explorer


Theorem ioombl1

Description: An open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014) (Proof shortened by Mario Carneiro, 25-Mar-2015)

Ref Expression
Assertion ioombl1 ( 𝐴 ∈ ℝ* → ( 𝐴 (,) +∞ ) ∈ dom vol )

Proof

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 )