# Metamath Proof Explorer

## Theorem ioombl

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

Ref Expression
Assertion ioombl ${⊢}\left({A},{B}\right)\in \mathrm{dom}vol$

### Proof

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