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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmbf	⊢ MblFn
1		vf	⊢ 𝑓
2		cc	⊢ ℂ
3		cpm	⊢ ↑pm
4		cr	⊢ ℝ
5	2 4 3	co	⊢ ( ℂ ↑pm ℝ )
6		vx	⊢ 𝑥
7		cioo	⊢ (,)
8	7	crn	⊢ ran (,)
9		cre	⊢ ℜ
10	1	cv	⊢ 𝑓
11	9 10	ccom	⊢ ( ℜ ∘ 𝑓 )
12	11	ccnv	⊢ ◡ ( ℜ ∘ 𝑓 )
13	6	cv	⊢ 𝑥
14	12 13	cima	⊢ ( ◡ ( ℜ ∘ 𝑓 ) “ 𝑥 )
15		cvol	⊢ vol
16	15	cdm	⊢ dom vol
17	14 16	wcel	⊢ ( ◡ ( ℜ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol
18		cim	⊢ ℑ
19	18 10	ccom	⊢ ( ℑ ∘ 𝑓 )
20	19	ccnv	⊢ ◡ ( ℑ ∘ 𝑓 )
21	20 13	cima	⊢ ( ◡ ( ℑ ∘ 𝑓 ) “ 𝑥 )
22	21 16	wcel	⊢ ( ◡ ( ℑ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol
23	17 22	wa	⊢ ( ( ◡ ( ℜ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol )
24	23 6 8	wral	⊢ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol )
25	24 1 5	crab	⊢ { 𝑓 ∈ ( ℂ ↑pm ℝ ) ∣ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ) }
26	0 25	wceq	⊢ MblFn = { 𝑓 ∈ ( ℂ ↑pm ℝ ) ∣ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ) }