Metamath Proof Explorer

Theorem iocmbl

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

Ref Expression
Assertion iocmbl ⊢A∈ℝ*∧B∈ℝ→AB∈dom⁡vol

Proof

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