# 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 )`
` |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ -. ( B e. RR* /\ C e. RR* ) ) -> ( `' F " ( B (,) C ) ) e. dom vol )`
` |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( B (,) C ) ) e. dom vol )`