Metamath Proof Explorer

Theorem iccmbl

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

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

Proof

Step Hyp Ref Expression
1 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
2 dfss4 
 |-  ( ( A [,] B ) C_ RR <-> ( RR \ ( RR \ ( A [,] B ) ) ) = ( A [,] B ) )
3 1 2 sylib 
 |-  ( ( A e. RR /\ B e. RR ) -> ( RR \ ( RR \ ( A [,] B ) ) ) = ( A [,] B ) )
4 difreicc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
5 ioombl 
 |-  ( -oo (,) A ) e. dom vol
6 ioombl 
 |-  ( B (,) +oo ) e. dom vol
7 unmbl 
 |-  ( ( ( -oo (,) A ) e. dom vol /\ ( B (,) +oo ) e. dom vol ) -> ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. dom vol )
8 5 6 7 mp2an 
 |-  ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. dom vol
9 4 8 eqeltrdi 
 |-  ( ( A e. RR /\ B e. RR ) -> ( RR \ ( A [,] B ) ) e. dom vol )
10 cmmbl 
 |-  ( ( RR \ ( A [,] B ) ) e. dom vol -> ( RR \ ( RR \ ( A [,] B ) ) ) e. dom vol )
11 9 10 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( RR \ ( RR \ ( A [,] B ) ) ) e. dom vol )
12 3 11 eqeltrrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. dom vol )