Metamath Proof Explorer

Theorem mbfdm

Description: The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbfdm 
|- ( F e. MblFn -> dom F e. dom vol )

Proof

Step Hyp Ref Expression
1 ref 
 |-  Re : CC --> RR
2 mbff 
 |-  ( F e. MblFn -> F : dom F --> CC )
3 fco 
 |-  ( ( Re : CC --> RR /\ F : dom F --> CC ) -> ( Re o. F ) : dom F --> RR )
4 1 2 3 sylancr 
 |-  ( F e. MblFn -> ( Re o. F ) : dom F --> RR )
5 fimacnv 
 |-  ( ( Re o. F ) : dom F --> RR -> ( `' ( Re o. F ) " RR ) = dom F )
6 4 5 syl 
 |-  ( F e. MblFn -> ( `' ( Re o. F ) " RR ) = dom F )
7 imaeq2 
 |-  ( x = RR -> ( `' ( Re o. F ) " x ) = ( `' ( Re o. F ) " RR ) )
8 7 eleq1d 
 |-  ( x = RR -> ( ( `' ( Re o. F ) " x ) e. dom vol <-> ( `' ( Re o. F ) " RR ) e. dom vol ) )
9 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 ) ) )
10 simpl 
 |-  ( ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) -> ( `' ( Re o. F ) " x ) e. dom vol )
11 10 ralimi 
 |-  ( A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) -> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol )
12 9 11 simplbiim 
 |-  ( F e. MblFn -> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol )
13 ioomax 
 |-  ( -oo (,) +oo ) = RR
14 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
15 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
16 14 15 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
17 mnfxr 
 |-  -oo e. RR*
18 pnfxr 
 |-  +oo e. RR*
19 fnovrn 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ -oo e. RR* /\ +oo e. RR* ) -> ( -oo (,) +oo ) e. ran (,) )
20 16 17 18 19 mp3an 
 |-  ( -oo (,) +oo ) e. ran (,)
21 13 20 eqeltrri 
 |-  RR e. ran (,)
22 21 a1i 
 |-  ( F e. MblFn -> RR e. ran (,) )
23 8 12 22 rspcdva 
 |-  ( F e. MblFn -> ( `' ( Re o. F ) " RR ) e. dom vol )
24 6 23 eqeltrrd 
 |-  ( F e. MblFn -> dom F e. dom vol )