Theorem iocmbl

Description: An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019)

	Ref	Expression
Assertion	iocmbl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ∈ dom vol )

Proof

Step	Hyp	Ref	Expression
1		rexr	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
2		ioounsn	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
3	1 2	syl3an2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
4		ioombl	⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
5		iccid	⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 [,] 𝐵 ) = { 𝐵 } )
6	1 5	syl	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 [,] 𝐵 ) = { 𝐵 } )
7		iccmbl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 [,] 𝐵 ) ∈ dom vol )
8	7	anidms	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 [,] 𝐵 ) ∈ dom vol )
9	6 8	eqeltrrd	⊢ ( 𝐵 ∈ ℝ → { 𝐵 } ∈ dom vol )
10	9	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → { 𝐵 } ∈ dom vol )
11		unmbl	⊢ ( ( ( 𝐴 (,) 𝐵 ) ∈ dom vol ∧ { 𝐵 } ∈ dom vol ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ dom vol )
12	4 10 11	sylancr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ dom vol )
13	12	3adant3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∈ dom vol )
14	3 13	eqeltrrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 (,] 𝐵 ) ∈ dom vol )
15	14	3expa	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → ( 𝐴 (,] 𝐵 ) ∈ dom vol )
16		id	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ∈ ℝ* )
17		xrlenlt	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
18	1 16 17	syl2anr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
19	18	biimp3ar	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ ¬ 𝐴 < 𝐵 ) → 𝐵 ≤ 𝐴 )
20		ioc0	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,] 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
21	20	biimp3ar	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐴 ) → ( 𝐴 (,] 𝐵 ) = ∅ )
22	1 21	syl3an2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≤ 𝐴 ) → ( 𝐴 (,] 𝐵 ) = ∅ )
23		0mbl	⊢ ∅ ∈ dom vol
24	22 23	eqeltrdi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≤ 𝐴 ) → ( 𝐴 (,] 𝐵 ) ∈ dom vol )
25	19 24	syld3an3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 (,] 𝐵 ) ∈ dom vol )
26	25	3expa	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 (,] 𝐵 ) ∈ dom vol )
27	15 26	pm2.61dan	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ∈ dom vol )