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 ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑚 ∈ ℕ ↦ ⟨ if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ ) ) )
17		eqid	⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑚 ∈ ℕ ↦ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) ⟩ ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑚 ∈ ℕ ↦ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) ⟩ ) ) )
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	⊢ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) )
24		eqid	⊢ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) )
25		2fveq3	⊢ ( 𝑚 = 𝑛 → ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) = ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) )
26	25	breq1d	⊢ ( 𝑚 = 𝑛 → ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 ↔ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 ) )
27	26 25	ifbieq2d	⊢ ( 𝑚 = 𝑛 → if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) = if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
28		2fveq3	⊢ ( 𝑚 = 𝑛 → ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) = ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
29	27 28	breq12d	⊢ ( 𝑚 = 𝑛 → ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ↔ if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
30	29 27 28	ifbieq12d	⊢ ( 𝑚 = 𝑛 → if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) = if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
31	30 28	opeq12d	⊢ ( 𝑚 = 𝑛 → ⟨ if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ = ⟨ if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
32	31	cbvmptv	⊢ ( 𝑚 ∈ ℕ ↦ ⟨ if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ⟩ ) = ( 𝑛 ∈ ℕ ↦ ⟨ if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ⟩ )
33	25 30	opeq12d	⊢ ( 𝑚 = 𝑛 → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ )
34	33	cbvmptv	⊢ ( 𝑚 ∈ ℕ ↦ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑚 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) ⟩ ) = ( 𝑛 ∈ ℕ ↦ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ 𝐴 , 𝐴 , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ )
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 )

Metamath Proof Explorer

Theorem ioombl1

Proof