MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mbf Structured version   Visualization version   GIF version

Definition df-mbf 23111
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 23018) 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
StepHypRef Expression
1 cmbf 23106 . 2 class MblFn
2 cre 13631 . . . . . . . . 9 class
3 vf . . . . . . . . . 10 setvar 𝑓
43cv 1473 . . . . . . . . 9 class 𝑓
52, 4ccom 5032 . . . . . . . 8 class (ℜ ∘ 𝑓)
65ccnv 5027 . . . . . . 7 class (ℜ ∘ 𝑓)
7 vx . . . . . . . 8 setvar 𝑥
87cv 1473 . . . . . . 7 class 𝑥
96, 8cima 5031 . . . . . 6 class ((ℜ ∘ 𝑓) “ 𝑥)
10 cvol 22956 . . . . . . 7 class vol
1110cdm 5028 . . . . . 6 class dom vol
129, 11wcel 1976 . . . . 5 wff ((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol
13 cim 13632 . . . . . . . . 9 class
1413, 4ccom 5032 . . . . . . . 8 class (ℑ ∘ 𝑓)
1514ccnv 5027 . . . . . . 7 class (ℑ ∘ 𝑓)
1615, 8cima 5031 . . . . . 6 class ((ℑ ∘ 𝑓) “ 𝑥)
1716, 11wcel 1976 . . . . 5 wff ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol
1812, 17wa 382 . . . 4 wff (((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)
19 cioo 12002 . . . . 5 class (,)
2019crn 5029 . . . 4 class ran (,)
2118, 7, 20wral 2895 . . 3 wff 𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)
22 cc 9790 . . . 4 class
23 cr 9791 . . . 4 class
24 cpm 7722 . . . 4 class pm
2522, 23, 24co 6527 . . 3 class (ℂ ↑pm ℝ)
2621, 3, 25crab 2899 . 2 class {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
271, 26wceq 1474 1 wff MblFn = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
Colors of variables: wff setvar class
This definition is referenced by:  ismbf1  23116
  Copyright terms: Public domain W3C validator