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 ) }