This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrdi 
 |-  ( -. ( 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 )