Definition df-mbf 23388

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 23294) and a complex function is measurable if the real and imaginary parts of the function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)

Assertion

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

Distinct variable group:   x, f

Detailed syntax breakdown of Definition df-mbf

Step	Hyp	Ref	Expression
1		cmbf 23383	. 2 class MblFn
2		cre 13837	. . . . . . . . 9 class Re
3		vf	. . . . . . . . . 10 setvar f
4	3	cv 1482	. . . . . . . . 9 class f
5	2, 4	ccom 5118	. . . . . . . 8 class ( Re o. f )
6	5	ccnv 5113	. . . . . . 7 class `' ( Re o. f )
7		vx	. . . . . . . 8 setvar x
8	7	cv 1482	. . . . . . 7 class x
9	6, 8	cima 5117	. . . . . 6 class ( `' ( Re o. f ) " x )
10		cvol 23232	. . . . . . 7 class vol
11	10	cdm 5114	. . . . . 6 class dom vol
12	9, 11	wcel 1990	. . . . 5 wff ( `' ( Re o. f ) " x ) e. dom vol
13		cim 13838	. . . . . . . . 9 class Im
14	13, 4	ccom 5118	. . . . . . . 8 class ( Im o. f )
15	14	ccnv 5113	. . . . . . 7 class `' ( Im o. f )
16	15, 8	cima 5117	. . . . . 6 class ( `' ( Im o. f ) " x )
17	16, 11	wcel 1990	. . . . 5 wff ( `' ( Im o. f ) " x ) e. dom vol
18	12, 17	wa 384	. . . 4 wff ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol )
19		cioo 12175	. . . . 5 class (,)
20	19	crn 5115	. . . 4 class ran (,)
21	18, 7, 20	wral 2912	. . 3 wff A. x e. ran (,) ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol )
22		cc 9934	. . . 4 class CC
23		cr 9935	. . . 4 class RR
24		cpm 7858	. . . 4 class ^pm
25	22, 23, 24	co 6650	. . 3 class ( CC ^pm RR )
26	21, 3, 25	crab 2916	. 2 class { f e. ( CC ^pm RR ) | A. x e. ran (,) ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol ) }
27	1, 26	wceq 1483	1 wff MblFn = { f e. ( CC ^pm RR ) | A. x e. ran (,) ( ( `' ( Re o. f ) " x ) e. dom vol /\ ( `' ( Im o. f ) " x ) e. dom vol ) }

This definition is referenced by:  ismbf1  23393