Metamath Proof Explorer

Theorem ioombl

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

Ref Expression
Assertion ioombl 
|- ( A (,) B ) e. dom vol

Proof

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