This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ ℂ ↑ 𝑝𝑚 ℝ | ∀ x ∈ ran ⁡ . ℜ ∘ f -1 x ∈ dom ⁡ vol ∧ ℑ ∘ f -1 x ∈ 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 ℜ ∘ f
12 11 ccnv class ℜ ∘ f -1
13 6 cv setvar x
14 12 13 cima class ℜ ∘ f -1 x
15 cvol class vol
16 15 cdm class dom ⁡ vol
17 14 16 wcel wff ℜ ∘ f -1 x ∈ dom ⁡ vol
18 cim class ℑ
19 18 10 ccom class ℑ ∘ f
20 19 ccnv class ℑ ∘ f -1
21 20 13 cima class ℑ ∘ f -1 x
22 21 16 wcel wff ℑ ∘ f -1 x ∈ dom ⁡ vol
23 17 22 wa wff ℜ ∘ f -1 x ∈ dom ⁡ vol ∧ ℑ ∘ f -1 x ∈ dom ⁡ vol
24 23 6 8 wral wff ∀ x ∈ ran ⁡ . ℜ ∘ f -1 x ∈ dom ⁡ vol ∧ ℑ ∘ f -1 x ∈ dom ⁡ vol
25 24 1 5 crab class f ∈ ℂ ↑ 𝑝𝑚 ℝ | ∀ x ∈ ran ⁡ . ℜ ∘ f -1 x ∈ dom ⁡ vol ∧ ℑ ∘ f -1 x ∈ dom ⁡ vol
26 0 25 wceq wff MblFn = f ∈ ℂ ↑ 𝑝𝑚 ℝ | ∀ x ∈ ran ⁡ . ℜ ∘ f -1 x ∈ dom ⁡ vol ∧ ℑ ∘ f -1 x ∈ dom ⁡ vol