Metamath Proof Explorer

Theorem mbfimasn

Description: The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion mbfimasn 
|- ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> ( `' F " { B } ) e. dom vol )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> B e. RR )
2 rexr 
 |-  ( B e. RR -> B e. RR* )
3 iccid 
 |-  ( B e. RR* -> ( B [,] B ) = { B } )
4 1 2 3 3syl 
 |-  ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> ( B [,] B ) = { B } )
5 4 imaeq2d 
 |-  ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> ( `' F " ( B [,] B ) ) = ( `' F " { B } ) )
6 mbfimaicc 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ B e. RR ) ) -> ( `' F " ( B [,] B ) ) e. dom vol )
7 6 anabsan2 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ B e. RR ) -> ( `' F " ( B [,] B ) ) e. dom vol )
8 7 3impa 
 |-  ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> ( `' F " ( B [,] B ) ) e. dom vol )
9 5 8 eqeltrrd 
 |-  ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> ( `' F " { B } ) e. dom vol )