Metamath Proof Explorer


Theorem mbfima

Description: Definitional property of a measurable function: the preimage of an open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbfima
|- ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( B (,) C ) ) e. dom vol )

Proof

Step Hyp Ref Expression
1 ismbf
 |-  ( F : A --> RR -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
2 1 biimpac
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> A. x e. ran (,) ( `' F " x ) e. dom vol )
3 ioof
 |-  (,) : ( RR* X. RR* ) --> ~P RR
4 ffn
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
5 3 4 ax-mp
 |-  (,) Fn ( RR* X. RR* )
6 fnovrn
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ B e. RR* /\ C e. RR* ) -> ( B (,) C ) e. ran (,) )
7 5 6 mp3an1
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B (,) C ) e. ran (,) )
8 imaeq2
 |-  ( x = ( B (,) C ) -> ( `' F " x ) = ( `' F " ( B (,) C ) ) )
9 8 eleq1d
 |-  ( x = ( B (,) C ) -> ( ( `' F " x ) e. dom vol <-> ( `' F " ( B (,) C ) ) e. dom vol ) )
10 9 rspccva
 |-  ( ( A. x e. ran (,) ( `' F " x ) e. dom vol /\ ( B (,) C ) e. ran (,) ) -> ( `' F " ( B (,) C ) ) e. dom vol )
11 2 7 10 syl2an
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR* /\ C e. RR* ) ) -> ( `' F " ( B (,) C ) ) e. dom vol )
12 ndmioo
 |-  ( -. ( B e. RR* /\ C e. RR* ) -> ( B (,) C ) = (/) )
13 12 imaeq2d
 |-  ( -. ( B e. RR* /\ C e. RR* ) -> ( `' F " ( B (,) C ) ) = ( `' F " (/) ) )
14 ima0
 |-  ( `' F " (/) ) = (/)
15 13 14 syl6eq
 |-  ( -. ( B e. RR* /\ C e. RR* ) -> ( `' F " ( B (,) C ) ) = (/) )
16 0mbl
 |-  (/) e. dom vol
17 15 16 eqeltrdi
 |-  ( -. ( B e. RR* /\ C e. RR* ) -> ( `' F " ( B (,) C ) ) e. dom vol )
18 17 adantl
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ -. ( B e. RR* /\ C e. RR* ) ) -> ( `' F " ( B (,) C ) ) e. dom vol )
19 11 18 pm2.61dan
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( B (,) C ) ) e. dom vol )