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 )