Metamath Proof Explorer

Theorem inmbl

Description: An intersection of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion inmbl 
|- ( ( A e. dom vol /\ B e. dom vol ) -> ( A i^i B ) e. dom vol )

Proof

Step Hyp Ref Expression
1 difundi 
 |-  ( RR \ ( ( RR \ A ) u. ( RR \ B ) ) ) = ( ( RR \ ( RR \ A ) ) i^i ( RR \ ( RR \ B ) ) )
2 mblss 
 |-  ( A e. dom vol -> A C_ RR )
3 dfss4 
 |-  ( A C_ RR <-> ( RR \ ( RR \ A ) ) = A )
4 2 3 sylib 
 |-  ( A e. dom vol -> ( RR \ ( RR \ A ) ) = A )
5 mblss 
 |-  ( B e. dom vol -> B C_ RR )
6 dfss4 
 |-  ( B C_ RR <-> ( RR \ ( RR \ B ) ) = B )
7 5 6 sylib 
 |-  ( B e. dom vol -> ( RR \ ( RR \ B ) ) = B )
8 4 7 ineqan12d 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( ( RR \ ( RR \ A ) ) i^i ( RR \ ( RR \ B ) ) ) = ( A i^i B ) )
9 1 8 syl5eq 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( RR \ ( ( RR \ A ) u. ( RR \ B ) ) ) = ( A i^i B ) )
10 cmmbl 
 |-  ( A e. dom vol -> ( RR \ A ) e. dom vol )
11 cmmbl 
 |-  ( B e. dom vol -> ( RR \ B ) e. dom vol )
12 unmbl 
 |-  ( ( ( RR \ A ) e. dom vol /\ ( RR \ B ) e. dom vol ) -> ( ( RR \ A ) u. ( RR \ B ) ) e. dom vol )
13 10 11 12 syl2an 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( ( RR \ A ) u. ( RR \ B ) ) e. dom vol )
14 cmmbl 
 |-  ( ( ( RR \ A ) u. ( RR \ B ) ) e. dom vol -> ( RR \ ( ( RR \ A ) u. ( RR \ B ) ) ) e. dom vol )
15 13 14 syl 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( RR \ ( ( RR \ A ) u. ( RR \ B ) ) ) e. dom vol )
16 9 15 eqeltrrd 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( A i^i B ) e. dom vol )