This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem icombl

Description: A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion icombl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 uncom ⊢ ( ( 𝐵 [,) +∞ ) ∪ ( 𝐴 [,) 𝐵 ) ) = ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) +∞ ) )
2 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
3 2 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ* )
4 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ* )
5 pnfxr ⊢ +∞ ∈ ℝ*
6 5 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → +∞ ∈ ℝ* )
7 xrltle ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → 𝐴 ≤ 𝐵 ) )
8 2 7 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → 𝐴 ≤ 𝐵 ) )
9 8 imp ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
10 pnfge ⊢ ( 𝐵 ∈ ℝ* → 𝐵 ≤ +∞ )
11 4 10 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐵 ≤ +∞ )
12 icoun ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ +∞ ) ) → ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) +∞ ) ) = ( 𝐴 [,) +∞ ) )
13 3 4 6 9 11 12 syl32anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) +∞ ) ) = ( 𝐴 [,) +∞ ) )
14 1 13 eqtrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 [,) +∞ ) ∪ ( 𝐴 [,) 𝐵 ) ) = ( 𝐴 [,) +∞ ) )
15 ssun1 ⊢ ( 𝐵 [,) +∞ ) ⊆ ( ( 𝐵 [,) +∞ ) ∪ ( 𝐴 [,) 𝐵 ) )
16 15 14 sseqtrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 [,) +∞ ) ⊆ ( 𝐴 [,) +∞ ) )
17 incom ⊢ ( ( 𝐵 [,) +∞ ) ∩ ( 𝐴 [,) 𝐵 ) ) = ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) )
18 icodisj ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) ) = ∅ )
19 5 18 mp3an3 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) ) = ∅ )
20 3 4 19 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) ) = ∅ )
21 17 20 eqtrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 [,) +∞ ) ∩ ( 𝐴 [,) 𝐵 ) ) = ∅ )
22 uneqdifeq ⊢ ( ( ( 𝐵 [,) +∞ ) ⊆ ( 𝐴 [,) +∞ ) ∧ ( ( 𝐵 [,) +∞ ) ∩ ( 𝐴 [,) 𝐵 ) ) = ∅ ) → ( ( ( 𝐵 [,) +∞ ) ∪ ( 𝐴 [,) 𝐵 ) ) = ( 𝐴 [,) +∞ ) ↔ ( ( 𝐴 [,) +∞ ) ∖ ( 𝐵 [,) +∞ ) ) = ( 𝐴 [,) 𝐵 ) ) )
23 16 21 22 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( ( 𝐵 [,) +∞ ) ∪ ( 𝐴 [,) 𝐵 ) ) = ( 𝐴 [,) +∞ ) ↔ ( ( 𝐴 [,) +∞ ) ∖ ( 𝐵 [,) +∞ ) ) = ( 𝐴 [,) 𝐵 ) ) )
24 14 23 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 [,) +∞ ) ∖ ( 𝐵 [,) +∞ ) ) = ( 𝐴 [,) 𝐵 ) )
25 icombl1 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 [,) +∞ ) ∈ dom vol )
26 25 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐴 [,) +∞ ) ∈ dom vol )
27 xrleloe ⊢ ( ( 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐵 ≤ +∞ ↔ ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) ) )
28 4 6 27 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 ≤ +∞ ↔ ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) ) )
29 11 28 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) )
30 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
31 xrre2 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < +∞ ) ) → 𝐵 ∈ ℝ )
32 31 expr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 < +∞ → 𝐵 ∈ ℝ ) )
33 3 4 6 30 32 syl31anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 < +∞ → 𝐵 ∈ ℝ ) )
34 33 orim1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) ) )
35 29 34 mpd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) )
36 icombl1 ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 [,) +∞ ) ∈ dom vol )
37 oveq1 ⊢ ( 𝐵 = +∞ → ( 𝐵 [,) +∞ ) = ( +∞ [,) +∞ ) )
38 pnfge ⊢ ( +∞ ∈ ℝ* → +∞ ≤ +∞ )
39 5 38 ax-mp ⊢ +∞ ≤ +∞
40 ico0 ⊢ ( ( +∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( +∞ [,) +∞ ) = ∅ ↔ +∞ ≤ +∞ ) )
41 5 5 40 mp2an ⊢ ( ( +∞ [,) +∞ ) = ∅ ↔ +∞ ≤ +∞ )
42 39 41 mpbir ⊢ ( +∞ [,) +∞ ) = ∅
43 37 42 eqtrdi ⊢ ( 𝐵 = +∞ → ( 𝐵 [,) +∞ ) = ∅ )
44 0mbl ⊢ ∅ ∈ dom vol
45 43 44 eqeltrdi ⊢ ( 𝐵 = +∞ → ( 𝐵 [,) +∞ ) ∈ dom vol )
46 36 45 jaoi ⊢ ( ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) → ( 𝐵 [,) +∞ ) ∈ dom vol )
47 35 46 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 [,) +∞ ) ∈ dom vol )
48 difmbl ⊢ ( ( ( 𝐴 [,) +∞ ) ∈ dom vol ∧ ( 𝐵 [,) +∞ ) ∈ dom vol ) → ( ( 𝐴 [,) +∞ ) ∖ ( 𝐵 [,) +∞ ) ) ∈ dom vol )
49 26 47 48 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 [,) +∞ ) ∖ ( 𝐵 [,) +∞ ) ) ∈ dom vol )
50 24 49 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
51 ico0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
52 2 51 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
53 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → 𝐵 ∈ ℝ* )
54 2 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → 𝐴 ∈ ℝ* )
55 53 54 xrlenltd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
56 52 55 bitrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ ¬ 𝐴 < 𝐵 ) )
57 56 biimpar ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 [,) 𝐵 ) = ∅ )
58 57 44 eqeltrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
59 50 58 pm2.61dan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )