Metamath Proof Explorer


Theorem mbff

Description: A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbff
|- ( F e. MblFn -> F : dom F --> CC )

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 1 simplbi
 |-  ( F e. MblFn -> F e. ( CC ^pm RR ) )
3 cnex
 |-  CC e. _V
4 reex
 |-  RR e. _V
5 3 4 elpm2
 |-  ( F e. ( CC ^pm RR ) <-> ( F : dom F --> CC /\ dom F C_ RR ) )
6 5 simplbi
 |-  ( F e. ( CC ^pm RR ) -> F : dom F --> CC )
7 2 6 syl
 |-  ( F e. MblFn -> F : dom F --> CC )