# Metamath Proof Explorer

## Theorem ismbf

Description: The predicate " F is a measurable function". A function is measurable iff the preimages of all open intervals are measurable sets in the sense of ismbl . (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion ismbf
|- ( F : A --> RR -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )

### Proof

Step Hyp Ref Expression
1 mbfdm
|-  ( F e. MblFn -> dom F e. dom vol )
2 fdm
|-  ( F : A --> RR -> dom F = A )
3 2 eleq1d
|-  ( F : A --> RR -> ( dom F e. dom vol <-> A e. dom vol ) )
4 1 3 syl5ib
|-  ( F : A --> RR -> ( F e. MblFn -> A e. dom vol ) )
5 ioomax
|-  ( -oo (,) +oo ) = RR
6 ioorebas
|-  ( -oo (,) +oo ) e. ran (,)
7 5 6 eqeltrri
|-  RR e. ran (,)
8 imaeq2
|-  ( x = RR -> ( `' F " x ) = ( `' F " RR ) )
9 8 eleq1d
|-  ( x = RR -> ( ( `' F " x ) e. dom vol <-> ( `' F " RR ) e. dom vol ) )
10 9 rspcv
|-  ( RR e. ran (,) -> ( A. x e. ran (,) ( `' F " x ) e. dom vol -> ( `' F " RR ) e. dom vol ) )
11 7 10 ax-mp
|-  ( A. x e. ran (,) ( `' F " x ) e. dom vol -> ( `' F " RR ) e. dom vol )
12 fimacnv
|-  ( F : A --> RR -> ( `' F " RR ) = A )
13 12 eleq1d
|-  ( F : A --> RR -> ( ( `' F " RR ) e. dom vol <-> A e. dom vol ) )
14 11 13 syl5ib
|-  ( F : A --> RR -> ( A. x e. ran (,) ( `' F " x ) e. dom vol -> A e. dom vol ) )
15 ffvelrn
|-  ( ( F : A --> RR /\ x e. A ) -> ( F ` x ) e. RR )
|-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( F ` x ) e. RR )
17 16 rered
|-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( Re ` ( F ` x ) ) = ( F ` x ) )
18 17 mpteq2dva
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( x e. A |-> ( Re ` ( F ` x ) ) ) = ( x e. A |-> ( F ` x ) ) )
19 16 recnd
|-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( F ` x ) e. CC )
20 simpl
|-  ( ( F : A --> RR /\ A e. dom vol ) -> F : A --> RR )
21 20 feqmptd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> F = ( x e. A |-> ( F ` x ) ) )
22 ref
|-  Re : CC --> RR
23 22 a1i
|-  ( ( F : A --> RR /\ A e. dom vol ) -> Re : CC --> RR )
24 23 feqmptd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> Re = ( y e. CC |-> ( Re ` y ) ) )
25 fveq2
|-  ( y = ( F ` x ) -> ( Re ` y ) = ( Re ` ( F ` x ) ) )
26 19 21 24 25 fmptco
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Re o. F ) = ( x e. A |-> ( Re ` ( F ` x ) ) ) )
27 18 26 21 3eqtr4rd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> F = ( Re o. F ) )
28 27 cnveqd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> `' F = `' ( Re o. F ) )
29 28 imaeq1d
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' F " x ) = ( `' ( Re o. F ) " x ) )
30 29 eleq1d
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( ( `' F " x ) e. dom vol <-> ( `' ( Re o. F ) " x ) e. dom vol ) )
31 imf
|-  Im : CC --> RR
32 31 a1i
|-  ( ( F : A --> RR /\ A e. dom vol ) -> Im : CC --> RR )
33 32 feqmptd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> Im = ( y e. CC |-> ( Im ` y ) ) )
34 fveq2
|-  ( y = ( F ` x ) -> ( Im ` y ) = ( Im ` ( F ` x ) ) )
35 19 21 33 34 fmptco
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Im o. F ) = ( x e. A |-> ( Im ` ( F ` x ) ) ) )
36 16 reim0d
|-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( Im ` ( F ` x ) ) = 0 )
37 36 mpteq2dva
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( x e. A |-> ( Im ` ( F ` x ) ) ) = ( x e. A |-> 0 ) )
38 35 37 eqtrd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Im o. F ) = ( x e. A |-> 0 ) )
39 fconstmpt
|-  ( A X. { 0 } ) = ( x e. A |-> 0 )
40 38 39 syl6eqr
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Im o. F ) = ( A X. { 0 } ) )
41 40 cnveqd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> `' ( Im o. F ) = `' ( A X. { 0 } ) )
42 41 imaeq1d
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' ( Im o. F ) " x ) = ( `' ( A X. { 0 } ) " x ) )
43 simpr
|-  ( ( F : A --> RR /\ A e. dom vol ) -> A e. dom vol )
44 0re
|-  0 e. RR
45 mbfconstlem
|-  ( ( A e. dom vol /\ 0 e. RR ) -> ( `' ( A X. { 0 } ) " x ) e. dom vol )
46 43 44 45 sylancl
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' ( A X. { 0 } ) " x ) e. dom vol )
47 42 46 eqeltrd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' ( Im o. F ) " x ) e. dom vol )
48 47 biantrud
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( ( `' ( Re o. F ) " x ) e. dom vol <-> ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
49 30 48 bitrd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( ( `' F " x ) e. dom vol <-> ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
50 49 ralbidv
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( A. x e. ran (,) ( `' F " x ) e. dom vol <-> A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
51 ax-resscn
|-  RR C_ CC
52 fss
|-  ( ( F : A --> RR /\ RR C_ CC ) -> F : A --> CC )
53 51 52 mpan2
|-  ( F : A --> RR -> F : A --> CC )
54 mblss
|-  ( A e. dom vol -> A C_ RR )
55 cnex
|-  CC e. _V
56 reex
|-  RR e. _V
57 elpm2r
|-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) )
58 55 56 57 mpanl12
|-  ( ( F : A --> CC /\ A C_ RR ) -> F e. ( CC ^pm RR ) )
59 53 54 58 syl2an
|-  ( ( F : A --> RR /\ A e. dom vol ) -> F e. ( CC ^pm RR ) )
60 59 biantrurd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) <-> ( F e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) ) )
61 50 60 bitrd
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( A. x e. ran (,) ( `' F " x ) e. dom vol <-> ( F e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) ) )
62 ismbf1
|-  ( F e. MblFn <-> ( F e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
63 61 62 syl6rbbr
|-  ( ( F : A --> RR /\ A e. dom vol ) -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
64 63 ex
|-  ( F : A --> RR -> ( A e. dom vol -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) ) )
65 4 14 64 pm5.21ndd
|-  ( F : A --> RR -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )