Definition df-mbf 24764

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 24671) 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 = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}

Distinct variable group:   𝑥,𝑓

Detailed syntax breakdown of Definition df-mbf

Step	Hyp	Ref	Expression
1		cmbf 24759	. 2 class MblFn
2		cre 14789	. . . . . . . . 9 class ℜ
3		vf	. . . . . . . . . 10 setvar 𝑓
4	3	cv 1540	. . . . . . . . 9 class 𝑓
5	2, 4	ccom 5592	. . . . . . . 8 class (ℜ ∘ 𝑓)
6	5	ccnv 5587	. . . . . . 7 class ◡(ℜ ∘ 𝑓)
7		vx	. . . . . . . 8 setvar 𝑥
8	7	cv 1540	. . . . . . 7 class 𝑥
9	6, 8	cima 5591	. . . . . 6 class (◡(ℜ ∘ 𝑓) “ 𝑥)
10		cvol 24608	. . . . . . 7 class vol
11	10	cdm 5588	. . . . . 6 class dom vol
12	9, 11	wcel 2109	. . . . 5 wff (◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol
13		cim 14790	. . . . . . . . 9 class ℑ
14	13, 4	ccom 5592	. . . . . . . 8 class (ℑ ∘ 𝑓)
15	14	ccnv 5587	. . . . . . 7 class ◡(ℑ ∘ 𝑓)
16	15, 8	cima 5591	. . . . . 6 class (◡(ℑ ∘ 𝑓) “ 𝑥)
17	16, 11	wcel 2109	. . . . 5 wff (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol
18	12, 17	wa 395	. . . 4 wff ((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)
19		cioo 13061	. . . . 5 class (,)
20	19	crn 5589	. . . 4 class ran (,)
21	18, 7, 20	wral 3065	. . 3 wff ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)
22		cc 10853	. . . 4 class ℂ
23		cr 10854	. . . 4 class ℝ
24		cpm 8590	. . . 4 class ↑pm
25	22, 23, 24	co 7268	. . 3 class (ℂ ↑pm ℝ)
26	21, 3, 25	crab 3069	. 2 class {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
27	1, 26	wceq 1541	1 wff MblFn = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}

This definition is referenced by:  ismbf1  24769