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 
|- ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) e. dom vol )

Proof

Step Hyp Ref Expression
1 uncom 
 |-  ( ( B [,) +oo ) u. ( A [,) B ) ) = ( ( A [,) B ) u. ( B [,) +oo ) )
2 rexr 
 |-  ( A e. RR -> A e. RR* )
3 2 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> A e. RR* )
4 simplr 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> B e. RR* )
5 pnfxr 
 |-  +oo e. RR*
6 5 a1i 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> +oo e. RR* )
7 xrltle 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> A <_ B ) )
8 2 7 sylan 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( A < B -> A <_ B ) )
9 8 imp 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> A <_ B )
10 pnfge 
 |-  ( B e. RR* -> B <_ +oo )
11 4 10 syl 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> B <_ +oo )
12 icoun 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ +oo e. RR* ) /\ ( A <_ B /\ B <_ +oo ) ) -> ( ( A [,) B ) u. ( B [,) +oo ) ) = ( A [,) +oo ) )
13 3 4 6 9 11 12 syl32anc 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( ( A [,) B ) u. ( B [,) +oo ) ) = ( A [,) +oo ) )
14 1 13 syl5eq 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( ( B [,) +oo ) u. ( A [,) B ) ) = ( A [,) +oo ) )
15 ssun1 
 |-  ( B [,) +oo ) C_ ( ( B [,) +oo ) u. ( A [,) B ) )
16 15 14 sseqtrid 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( B [,) +oo ) C_ ( A [,) +oo ) )
17 incom 
 |-  ( ( B [,) +oo ) i^i ( A [,) B ) ) = ( ( A [,) B ) i^i ( B [,) +oo ) )
18 icodisj 
 |-  ( ( A e. RR* /\ B e. RR* /\ +oo e. RR* ) -> ( ( A [,) B ) i^i ( B [,) +oo ) ) = (/) )
19 5 18 mp3an3 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,) B ) i^i ( B [,) +oo ) ) = (/) )
20 3 4 19 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( ( A [,) B ) i^i ( B [,) +oo ) ) = (/) )
21 17 20 syl5eq 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( ( B [,) +oo ) i^i ( A [,) B ) ) = (/) )
22 uneqdifeq 
 |-  ( ( ( B [,) +oo ) C_ ( A [,) +oo ) /\ ( ( B [,) +oo ) i^i ( A [,) B ) ) = (/) ) -> ( ( ( B [,) +oo ) u. ( A [,) B ) ) = ( A [,) +oo ) <-> ( ( A [,) +oo ) \ ( B [,) +oo ) ) = ( A [,) B ) ) )
23 16 21 22 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( ( ( B [,) +oo ) u. ( A [,) B ) ) = ( A [,) +oo ) <-> ( ( A [,) +oo ) \ ( B [,) +oo ) ) = ( A [,) B ) ) )
24 14 23 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( ( A [,) +oo ) \ ( B [,) +oo ) ) = ( A [,) B ) )
25 icombl1 
 |-  ( A e. RR -> ( A [,) +oo ) e. dom vol )
26 25 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( A [,) +oo ) e. dom vol )
27 xrleloe 
 |-  ( ( B e. RR* /\ +oo e. RR* ) -> ( B <_ +oo <-> ( B < +oo \/ B = +oo ) ) )
28 4 6 27 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( B <_ +oo <-> ( B < +oo \/ B = +oo ) ) )
29 11 28 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( B < +oo \/ B = +oo ) )
30 simpr 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> A < B )
31 xrre2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ +oo e. RR* ) /\ ( A < B /\ B < +oo ) ) -> B e. RR )
32 31 expr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ +oo e. RR* ) /\ A < B ) -> ( B < +oo -> B e. RR ) )
33 3 4 6 30 32 syl31anc 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( B < +oo -> B e. RR ) )
34 33 orim1d 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( ( B < +oo \/ B = +oo ) -> ( B e. RR \/ B = +oo ) ) )
35 29 34 mpd 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( B e. RR \/ B = +oo ) )
36 icombl1 
 |-  ( B e. RR -> ( B [,) +oo ) e. dom vol )
37 oveq1 
 |-  ( B = +oo -> ( B [,) +oo ) = ( +oo [,) +oo ) )
38 pnfge 
 |-  ( +oo e. RR* -> +oo <_ +oo )
39 5 38 ax-mp 
 |-  +oo <_ +oo
40 ico0 
 |-  ( ( +oo e. RR* /\ +oo e. RR* ) -> ( ( +oo [,) +oo ) = (/) <-> +oo <_ +oo ) )
41 5 5 40 mp2an 
 |-  ( ( +oo [,) +oo ) = (/) <-> +oo <_ +oo )
42 39 41 mpbir 
 |-  ( +oo [,) +oo ) = (/)
43 37 42 eqtrdi 
 |-  ( B = +oo -> ( B [,) +oo ) = (/) )
44 0mbl 
 |-  (/) e. dom vol
45 43 44 eqeltrdi 
 |-  ( B = +oo -> ( B [,) +oo ) e. dom vol )
46 36 45 jaoi 
 |-  ( ( B e. RR \/ B = +oo ) -> ( B [,) +oo ) e. dom vol )
47 35 46 syl 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( B [,) +oo ) e. dom vol )
48 difmbl 
 |-  ( ( ( A [,) +oo ) e. dom vol /\ ( B [,) +oo ) e. dom vol ) -> ( ( A [,) +oo ) \ ( B [,) +oo ) ) e. dom vol )
49 26 47 48 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( ( A [,) +oo ) \ ( B [,) +oo ) ) e. dom vol )
50 24 49 eqeltrrd 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ A < B ) -> ( A [,) B ) e. dom vol )
51 ico0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
52 2 51 sylan 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
53 simpr 
 |-  ( ( A e. RR /\ B e. RR* ) -> B e. RR* )
54 2 adantr 
 |-  ( ( A e. RR /\ B e. RR* ) -> A e. RR* )
55 53 54 xrlenltd 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( B <_ A <-> -. A < B ) )
56 52 55 bitrd 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( ( A [,) B ) = (/) <-> -. A < B ) )
57 56 biimpar 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ -. A < B ) -> ( A [,) B ) = (/) )
58 57 44 eqeltrdi 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ -. A < B ) -> ( A [,) B ) e. dom vol )
59 50 58 pm2.61dan 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) e. dom vol )