Metamath Proof Explorer

Theorem iocmbl

Description: An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019)

Ref Expression
Assertion iocmbl 
|- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) e. dom vol )

Proof

Step Hyp Ref Expression
1 rexr 
 |-  ( B e. RR -> B e. RR* )
2 ioounsn 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
3 1 2 syl3an2 
 |-  ( ( A e. RR* /\ B e. RR /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
4 ioombl 
 |-  ( A (,) B ) e. dom vol
5 iccid 
 |-  ( B e. RR* -> ( B [,] B ) = { B } )
6 1 5 syl 
 |-  ( B e. RR -> ( B [,] B ) = { B } )
7 iccmbl 
 |-  ( ( B e. RR /\ B e. RR ) -> ( B [,] B ) e. dom vol )
8 7 anidms 
 |-  ( B e. RR -> ( B [,] B ) e. dom vol )
9 6 8 eqeltrrd 
 |-  ( B e. RR -> { B } e. dom vol )
10 9 adantl 
 |-  ( ( A e. RR* /\ B e. RR ) -> { B } e. dom vol )
11 unmbl 
 |-  ( ( ( A (,) B ) e. dom vol /\ { B } e. dom vol ) -> ( ( A (,) B ) u. { B } ) e. dom vol )
12 4 10 11 sylancr 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( A (,) B ) u. { B } ) e. dom vol )
13 12 3adant3 
 |-  ( ( A e. RR* /\ B e. RR /\ A < B ) -> ( ( A (,) B ) u. { B } ) e. dom vol )
14 3 13 eqeltrrd 
 |-  ( ( A e. RR* /\ B e. RR /\ A < B ) -> ( A (,] B ) e. dom vol )
15 14 3expa 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A < B ) -> ( A (,] B ) e. dom vol )
16 id 
 |-  ( A e. RR* -> A e. RR* )
17 xrlenlt 
 |-  ( ( B e. RR* /\ A e. RR* ) -> ( B <_ A <-> -. A < B ) )
18 1 16 17 syl2anr 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( B <_ A <-> -. A < B ) )
19 18 biimp3ar 
 |-  ( ( A e. RR* /\ B e. RR /\ -. A < B ) -> B <_ A )
20 ioc0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,] B ) = (/) <-> B <_ A ) )
21 20 biimp3ar 
 |-  ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> ( A (,] B ) = (/) )
22 1 21 syl3an2 
 |-  ( ( A e. RR* /\ B e. RR /\ B <_ A ) -> ( A (,] B ) = (/) )
23 0mbl 
 |-  (/) e. dom vol
24 22 23 eqeltrdi 
 |-  ( ( A e. RR* /\ B e. RR /\ B <_ A ) -> ( A (,] B ) e. dom vol )
25 19 24 syld3an3 
 |-  ( ( A e. RR* /\ B e. RR /\ -. A < B ) -> ( A (,] B ) e. dom vol )
26 25 3expa 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ -. A < B ) -> ( A (,] B ) e. dom vol )
27 15 26 pm2.61dan 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) e. dom vol )