Metamath Proof Explorer

Theorem difmbl

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

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

Proof

Step Hyp Ref Expression
1 indif2 
 |-  ( A i^i ( RR \ B ) ) = ( ( A i^i RR ) \ B )
2 mblss 
 |-  ( A e. dom vol -> A C_ RR )
3 df-ss 
 |-  ( A C_ RR <-> ( A i^i RR ) = A )
4 2 3 sylib 
 |-  ( A e. dom vol -> ( A i^i RR ) = A )
5 4 difeq1d 
 |-  ( A e. dom vol -> ( ( A i^i RR ) \ B ) = ( A \ B ) )
6 1 5 syl5eq 
 |-  ( A e. dom vol -> ( A i^i ( RR \ B ) ) = ( A \ B ) )
7 6 adantr 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( A i^i ( RR \ B ) ) = ( A \ B ) )
8 cmmbl 
 |-  ( B e. dom vol -> ( RR \ B ) e. dom vol )
9 inmbl 
 |-  ( ( A e. dom vol /\ ( RR \ B ) e. dom vol ) -> ( A i^i ( RR \ B ) ) e. dom vol )
10 8 9 sylan2 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( A i^i ( RR \ B ) ) e. dom vol )
11 7 10 eqeltrrd 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( A \ B ) e. dom vol )