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

Metamath Proof Explorer

Definition df-mbf

Description: Define the class of measurable functions on the reals. A real function is measurable if the preimage of every open interval is a measurable set (see ismbl ) and a complex function is measurable if the real and imaginary parts of the function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion df-mbf 
|- MblFn = { f e. ( CC ^pm RR ) | A. x e. ran (,) ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmbf 
 |-  MblFn
1 vf 
 |-  f
2 cc 
 |-  CC
3 cpm 
 |-  ^pm
4 cr 
 |-  RR
5 2 4 3 co 
 |-  ( CC ^pm RR )
6 vx 
 |-  x
7 cioo 
 |-  (,)
8 7 crn 
 |-  ran (,)
9 cre 
 |-  Re
10 1 cv 
 |-  f
11 9 10 ccom 
 |-  ( Re o. f )
12 11 ccnv 
 |-  `' ( Re o. f )
13 6 cv 
 |-  x
14 12 13 cima 
 |-  ( `' ( Re o. f ) " x )
15 cvol 
 |-  vol
16 15 cdm 
 |-  dom vol
17 14 16 wcel 
 |-  ( `' ( Re o. f ) " x ) e. dom vol
18 cim 
 |-  Im
19 18 10 ccom 
 |-  ( Im o. f )
20 19 ccnv 
 |-  `' ( Im o. f )
21 20 13 cima 
 |-  ( `' ( Im o. f ) " x )
22 21 16 wcel 
 |-  ( `' ( Im o. f ) " x ) e. dom vol
23 17 22 wa 
 |-  ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol )
24 23 6 8 wral 
 |-  A. x e. ran (,) ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol )
25 24 1 5 crab 
 |-  { f e. ( CC ^pm RR ) | A. x e. ran (,) ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol ) }
26 0 25 wceq 
 |-  MblFn = { f e. ( CC ^pm RR ) | A. x e. ran (,) ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol ) }