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 \in (ℂ ↑_{𝑝𝑚} ℝ) \| \forall x \in ran (.) ({(ℜ \circ f)}^{-1} [x] \in dom vol \land {(ℑ \circ f)}^{-1} [x] \in dom vol)\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmbf	$class MblFn$
1		vf	$setvar f$
2		cc	$class ℂ$
3		cpm	$class ↑_{𝑝𝑚}$
4		cr	$class ℝ$
5	2 4 3	co	$class (ℂ ↑_{𝑝𝑚} ℝ)$
6		vx	$setvar x$
7		cioo	$class (.)$
8	7	crn	$class ran (.)$
9		cre	$class ℜ$
10	1	cv	$setvar f$
11	9 10	ccom	$class (ℜ \circ f)$
12	11	ccnv	$class {(ℜ \circ f)}^{-1}$
13	6	cv	$setvar x$
14	12 13	cima	$class {(ℜ \circ f)}^{-1} [x]$
15		cvol	$class vol$
16	15	cdm	$class dom vol$
17	14 16	wcel	$wff {(ℜ \circ f)}^{-1} [x] \in dom vol$
18		cim	$class ℑ$
19	18 10	ccom	$class (ℑ \circ f)$
20	19	ccnv	$class {(ℑ \circ f)}^{-1}$
21	20 13	cima	$class {(ℑ \circ f)}^{-1} [x]$
22	21 16	wcel	$wff {(ℑ \circ f)}^{-1} [x] \in dom vol$
23	17 22	wa	$wff ({(ℜ \circ f)}^{-1} [x] \in dom vol \land {(ℑ \circ f)}^{-1} [x] \in dom vol)$
24	23 6 8	wral	$wff \forall x \in ran (.) ({(ℜ \circ f)}^{-1} [x] \in dom vol \land {(ℑ \circ f)}^{-1} [x] \in dom vol)$
25	24 1 5	crab	$class \{f \in (ℂ ↑_{𝑝𝑚} ℝ) \| \forall x \in ran (.) ({(ℜ \circ f)}^{-1} [x] \in dom vol \land {(ℑ \circ f)}^{-1} [x] \in dom vol)\}$
26	0 25	wceq	$wff MblFn = \{f \in (ℂ ↑_{𝑝𝑚} ℝ) \| \forall x \in ran (.) ({(ℜ \circ f)}^{-1} [x] \in dom vol \land {(ℑ \circ f)}^{-1} [x] \in dom vol)\}$

Metamath Proof Explorer

Definition df-mbf

Detailed syntax breakdown