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 ∈ ℝ → A B ∈ dom ⁡ vol

Proof

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