Metamath Proof Explorer

Theorem ioombl

Description: An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion ioombl ( 𝐴 (,) 𝐵 ) ∈ dom vol

Proof

Step Hyp Ref Expression
1 snunioo ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
2 1 3expa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
3 2 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
4 lbico1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ( 𝐴 [,) 𝐵 ) )
5 4 3expa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ( 𝐴 [,) 𝐵 ) )
6 5 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → 𝐴 ∈ ( 𝐴 [,) 𝐵 ) )
7 6 snssd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → { 𝐴 } ⊆ ( 𝐴 [,) 𝐵 ) )
8 iccid ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
9 8 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
10 9 ineq1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( ( 𝐴 [,] 𝐴 ) ∩ ( 𝐴 (,) 𝐵 ) ) = ( { 𝐴 } ∩ ( 𝐴 (,) 𝐵 ) ) )
11 simpll ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → 𝐴 ∈ ℝ* )
12 simplr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → 𝐵 ∈ ℝ* )
13 df-icc ⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
14 df-ioo ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
15 xrltnle ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤 ↔ ¬ 𝑤 ≤ 𝐴 ) )
16 13 14 15 ixxdisj ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐴 ) ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
17 11 11 12 16 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( ( 𝐴 [,] 𝐴 ) ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
18 10 17 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( { 𝐴 } ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
19 uneqdifeq ⊢ ( ( { 𝐴 } ⊆ ( 𝐴 [,) 𝐵 ) ∧ ( { 𝐴 } ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ) → ( ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) ↔ ( ( 𝐴 [,) 𝐵 ) ∖ { 𝐴 } ) = ( 𝐴 (,) 𝐵 ) ) )
20 7 18 19 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) ↔ ( ( 𝐴 [,) 𝐵 ) ∖ { 𝐴 } ) = ( 𝐴 (,) 𝐵 ) ) )
21 3 20 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( ( 𝐴 [,) 𝐵 ) ∖ { 𝐴 } ) = ( 𝐴 (,) 𝐵 ) )
22 mnfxr ⊢ -∞ ∈ ℝ*
23 22 a1i ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → -∞ ∈ ℝ* )
24 simprr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → -∞ < 𝐴 )
25 simprl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → 𝐴 < 𝐵 )
26 xrre2 ⊢ ( ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( -∞ < 𝐴 ∧ 𝐴 < 𝐵 ) ) → 𝐴 ∈ ℝ )
27 23 11 12 24 25 26 syl32anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → 𝐴 ∈ ℝ )
28 icombl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
29 27 12 28 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
30 27 snssd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → { 𝐴 } ⊆ ℝ )
31 ovolsn ⊢ ( 𝐴 ∈ ℝ → ( vol* ‘ { 𝐴 } ) = 0 )
32 27 31 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( vol* ‘ { 𝐴 } ) = 0 )
33 nulmbl ⊢ ( ( { 𝐴 } ⊆ ℝ ∧ ( vol* ‘ { 𝐴 } ) = 0 ) → { 𝐴 } ∈ dom vol )
34 30 32 33 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → { 𝐴 } ∈ dom vol )
35 difmbl ⊢ ( ( ( 𝐴 [,) 𝐵 ) ∈ dom vol ∧ { 𝐴 } ∈ dom vol ) → ( ( 𝐴 [,) 𝐵 ) ∖ { 𝐴 } ) ∈ dom vol )
36 29 34 35 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( ( 𝐴 [,) 𝐵 ) ∖ { 𝐴 } ) ∈ dom vol )
37 21 36 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ -∞ < 𝐴 ) ) → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
38 37 expr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( -∞ < 𝐴 → ( 𝐴 (,) 𝐵 ) ∈ dom vol ) )
39 uncom ⊢ ( ( 𝐵 [,) +∞ ) ∪ ( -∞ (,) 𝐵 ) ) = ( ( -∞ (,) 𝐵 ) ∪ ( 𝐵 [,) +∞ ) )
40 22 a1i ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → -∞ ∈ ℝ* )
41 simplr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ* )
42 pnfxr ⊢ +∞ ∈ ℝ*
43 42 a1i ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → +∞ ∈ ℝ* )
44 simpll ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ* )
45 mnfle ⊢ ( 𝐴 ∈ ℝ* → -∞ ≤ 𝐴 )
46 45 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → -∞ ≤ 𝐴 )
47 simpr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
48 40 44 41 46 47 xrlelttrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → -∞ < 𝐵 )
49 pnfge ⊢ ( 𝐵 ∈ ℝ* → 𝐵 ≤ +∞ )
50 41 49 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐵 ≤ +∞ )
51 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
52 xrlenlt ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐵 ≤ 𝑤 ↔ ¬ 𝑤 < 𝐵 ) )
53 xrltletr ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝑤 < 𝐵 ∧ 𝐵 ≤ +∞ ) → 𝑤 < +∞ ) )
54 xrltletr ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( -∞ < 𝐵 ∧ 𝐵 ≤ 𝑤 ) → -∞ < 𝑤 ) )
55 14 51 52 14 53 54 ixxun ⊢ ( ( ( -∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( -∞ < 𝐵 ∧ 𝐵 ≤ +∞ ) ) → ( ( -∞ (,) 𝐵 ) ∪ ( 𝐵 [,) +∞ ) ) = ( -∞ (,) +∞ ) )
56 40 41 43 48 50 55 syl32anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( -∞ (,) 𝐵 ) ∪ ( 𝐵 [,) +∞ ) ) = ( -∞ (,) +∞ ) )
57 39 56 syl5eq ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 [,) +∞ ) ∪ ( -∞ (,) 𝐵 ) ) = ( -∞ (,) +∞ ) )
58 ioomax ⊢ ( -∞ (,) +∞ ) = ℝ
59 57 58 eqtrdi ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 [,) +∞ ) ∪ ( -∞ (,) 𝐵 ) ) = ℝ )
60 ssun1 ⊢ ( 𝐵 [,) +∞ ) ⊆ ( ( 𝐵 [,) +∞ ) ∪ ( -∞ (,) 𝐵 ) )
61 60 59 sseqtrid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 [,) +∞ ) ⊆ ℝ )
62 incom ⊢ ( ( 𝐵 [,) +∞ ) ∩ ( -∞ (,) 𝐵 ) ) = ( ( -∞ (,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) )
63 14 51 52 ixxdisj ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( -∞ (,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) ) = ∅ )
64 40 41 43 63 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( -∞ (,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) ) = ∅ )
65 62 64 syl5eq ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 [,) +∞ ) ∩ ( -∞ (,) 𝐵 ) ) = ∅ )
66 uneqdifeq ⊢ ( ( ( 𝐵 [,) +∞ ) ⊆ ℝ ∧ ( ( 𝐵 [,) +∞ ) ∩ ( -∞ (,) 𝐵 ) ) = ∅ ) → ( ( ( 𝐵 [,) +∞ ) ∪ ( -∞ (,) 𝐵 ) ) = ℝ ↔ ( ℝ ∖ ( 𝐵 [,) +∞ ) ) = ( -∞ (,) 𝐵 ) ) )
67 61 65 66 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( ( 𝐵 [,) +∞ ) ∪ ( -∞ (,) 𝐵 ) ) = ℝ ↔ ( ℝ ∖ ( 𝐵 [,) +∞ ) ) = ( -∞ (,) 𝐵 ) ) )
68 59 67 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ℝ ∖ ( 𝐵 [,) +∞ ) ) = ( -∞ (,) 𝐵 ) )
69 rembl ⊢ ℝ ∈ dom vol
70 xrleloe ⊢ ( ( 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐵 ≤ +∞ ↔ ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) ) )
71 41 42 70 sylancl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 ≤ +∞ ↔ ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) ) )
72 50 71 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) )
73 xrre2 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < +∞ ) ) → 𝐵 ∈ ℝ )
74 73 expr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 < +∞ → 𝐵 ∈ ℝ ) )
75 42 74 mp3anl3 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 < +∞ → 𝐵 ∈ ℝ ) )
76 75 orim1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) ) )
77 72 76 mpd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) )
78 icombl1 ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 [,) +∞ ) ∈ dom vol )
79 oveq1 ⊢ ( 𝐵 = +∞ → ( 𝐵 [,) +∞ ) = ( +∞ [,) +∞ ) )
80 pnfge ⊢ ( +∞ ∈ ℝ* → +∞ ≤ +∞ )
81 42 80 ax-mp ⊢ +∞ ≤ +∞
82 ico0 ⊢ ( ( +∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( +∞ [,) +∞ ) = ∅ ↔ +∞ ≤ +∞ ) )
83 42 42 82 mp2an ⊢ ( ( +∞ [,) +∞ ) = ∅ ↔ +∞ ≤ +∞ )
84 81 83 mpbir ⊢ ( +∞ [,) +∞ ) = ∅
85 79 84 eqtrdi ⊢ ( 𝐵 = +∞ → ( 𝐵 [,) +∞ ) = ∅ )
86 0mbl ⊢ ∅ ∈ dom vol
87 85 86 eqeltrdi ⊢ ( 𝐵 = +∞ → ( 𝐵 [,) +∞ ) ∈ dom vol )
88 78 87 jaoi ⊢ ( ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) → ( 𝐵 [,) +∞ ) ∈ dom vol )
89 77 88 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 [,) +∞ ) ∈ dom vol )
90 difmbl ⊢ ( ( ℝ ∈ dom vol ∧ ( 𝐵 [,) +∞ ) ∈ dom vol ) → ( ℝ ∖ ( 𝐵 [,) +∞ ) ) ∈ dom vol )
91 69 89 90 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ℝ ∖ ( 𝐵 [,) +∞ ) ) ∈ dom vol )
92 68 91 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( -∞ (,) 𝐵 ) ∈ dom vol )
93 oveq1 ⊢ ( -∞ = 𝐴 → ( -∞ (,) 𝐵 ) = ( 𝐴 (,) 𝐵 ) )
94 93 eleq1d ⊢ ( -∞ = 𝐴 → ( ( -∞ (,) 𝐵 ) ∈ dom vol ↔ ( 𝐴 (,) 𝐵 ) ∈ dom vol ) )
95 92 94 syl5ibcom ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( -∞ = 𝐴 → ( 𝐴 (,) 𝐵 ) ∈ dom vol ) )
96 xrleloe ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -∞ ≤ 𝐴 ↔ ( -∞ < 𝐴 ∨ -∞ = 𝐴 ) ) )
97 22 44 96 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( -∞ ≤ 𝐴 ↔ ( -∞ < 𝐴 ∨ -∞ = 𝐴 ) ) )
98 46 97 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( -∞ < 𝐴 ∨ -∞ = 𝐴 ) )
99 38 95 98 mpjaod ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
100 ioo0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
101 xrlenlt ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
102 101 ancoms ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
103 100 102 bitrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ ¬ 𝐴 < 𝐵 ) )
104 103 biimpar ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 (,) 𝐵 ) = ∅ )
105 104 86 eqeltrdi ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
106 99 105 pm2.61dan ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
107 ndmioo ⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = ∅ )
108 107 86 eqeltrdi ⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
109 106 108 pm2.61i ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol