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 = { 𝑓 ∈ ( ℂ ↑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 ) }