# Metamath Proof Explorer

## Theorem ismbf

Description: The predicate " F is a measurable function". A function is measurable iff the preimages of all open intervals are measurable sets in the sense of ismbl . (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion ismbf ${⊢}{F}:{A}⟶ℝ\to \left({F}\in MblFn↔\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)$

### Proof

Step Hyp Ref Expression
1 mbfdm ${⊢}{F}\in MblFn\to \mathrm{dom}{F}\in \mathrm{dom}vol$
2 fdm ${⊢}{F}:{A}⟶ℝ\to \mathrm{dom}{F}={A}$
3 2 eleq1d ${⊢}{F}:{A}⟶ℝ\to \left(\mathrm{dom}{F}\in \mathrm{dom}vol↔{A}\in \mathrm{dom}vol\right)$
4 1 3 syl5ib ${⊢}{F}:{A}⟶ℝ\to \left({F}\in MblFn\to {A}\in \mathrm{dom}vol\right)$
5 ioomax ${⊢}\left(\mathrm{-\infty },\mathrm{+\infty }\right)=ℝ$
6 ioorebas ${⊢}\left(\mathrm{-\infty },\mathrm{+\infty }\right)\in \mathrm{ran}\left(.\right)$
7 5 6 eqeltrri ${⊢}ℝ\in \mathrm{ran}\left(.\right)$
8 imaeq2 ${⊢}{x}=ℝ\to {{F}}^{-1}\left[{x}\right]={{F}}^{-1}\left[ℝ\right]$
9 8 eleq1d ${⊢}{x}=ℝ\to \left({{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol↔{{F}}^{-1}\left[ℝ\right]\in \mathrm{dom}vol\right)$
10 9 rspcv ${⊢}ℝ\in \mathrm{ran}\left(.\right)\to \left(\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol\to {{F}}^{-1}\left[ℝ\right]\in \mathrm{dom}vol\right)$
11 7 10 ax-mp ${⊢}\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol\to {{F}}^{-1}\left[ℝ\right]\in \mathrm{dom}vol$
12 fimacnv ${⊢}{F}:{A}⟶ℝ\to {{F}}^{-1}\left[ℝ\right]={A}$
13 12 eleq1d ${⊢}{F}:{A}⟶ℝ\to \left({{F}}^{-1}\left[ℝ\right]\in \mathrm{dom}vol↔{A}\in \mathrm{dom}vol\right)$
14 11 13 syl5ib ${⊢}{F}:{A}⟶ℝ\to \left(\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol\to {A}\in \mathrm{dom}vol\right)$
15 ffvelrn ${⊢}\left({F}:{A}⟶ℝ\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in ℝ$
16 15 adantlr ${⊢}\left(\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in ℝ$
17 16 rered ${⊢}\left(\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\wedge {x}\in {A}\right)\to \Re \left({F}\left({x}\right)\right)={F}\left({x}\right)$
18 17 mpteq2dva ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right)=\left({x}\in {A}⟼{F}\left({x}\right)\right)$
19 16 recnd ${⊢}\left(\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in ℂ$
20 simpl ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {F}:{A}⟶ℝ$
21 20 feqmptd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)$
22 ref ${⊢}\Re :ℂ⟶ℝ$
23 22 a1i ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \Re :ℂ⟶ℝ$
24 23 feqmptd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \Re =\left({y}\in ℂ⟼\Re \left({y}\right)\right)$
25 fveq2 ${⊢}{y}={F}\left({x}\right)\to \Re \left({y}\right)=\Re \left({F}\left({x}\right)\right)$
26 19 21 24 25 fmptco ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \Re \circ {F}=\left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right)$
27 18 26 21 3eqtr4rd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {F}=\Re \circ {F}$
28 27 cnveqd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {{F}}^{-1}={\left(\Re \circ {F}\right)}^{-1}$
29 28 imaeq1d ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {{F}}^{-1}\left[{x}\right]={\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]$
30 29 eleq1d ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \left({{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol↔{\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)$
31 imf ${⊢}\Im :ℂ⟶ℝ$
32 31 a1i ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \Im :ℂ⟶ℝ$
33 32 feqmptd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \Im =\left({y}\in ℂ⟼\Im \left({y}\right)\right)$
34 fveq2 ${⊢}{y}={F}\left({x}\right)\to \Im \left({y}\right)=\Im \left({F}\left({x}\right)\right)$
35 19 21 33 34 fmptco ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \Im \circ {F}=\left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right)$
36 16 reim0d ${⊢}\left(\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\wedge {x}\in {A}\right)\to \Im \left({F}\left({x}\right)\right)=0$
37 36 mpteq2dva ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right)=\left({x}\in {A}⟼0\right)$
38 35 37 eqtrd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \Im \circ {F}=\left({x}\in {A}⟼0\right)$
39 fconstmpt ${⊢}{A}×\left\{0\right\}=\left({x}\in {A}⟼0\right)$
40 38 39 syl6eqr ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \Im \circ {F}={A}×\left\{0\right\}$
41 40 cnveqd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {\left(\Im \circ {F}\right)}^{-1}={\left({A}×\left\{0\right\}\right)}^{-1}$
42 41 imaeq1d ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {\left(\Im \circ {F}\right)}^{-1}\left[{x}\right]={\left({A}×\left\{0\right\}\right)}^{-1}\left[{x}\right]$
43 simpr ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {A}\in \mathrm{dom}vol$
44 0re ${⊢}0\in ℝ$
45 mbfconstlem ${⊢}\left({A}\in \mathrm{dom}vol\wedge 0\in ℝ\right)\to {\left({A}×\left\{0\right\}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol$
46 43 44 45 sylancl ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {\left({A}×\left\{0\right\}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol$
47 42 46 eqeltrd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {\left(\Im \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol$
48 47 biantrud ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \left({\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol↔\left({\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\wedge {\left(\Im \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)\right)$
49 30 48 bitrd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \left({{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol↔\left({\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\wedge {\left(\Im \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)\right)$
50 49 ralbidv ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \left(\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol↔\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\wedge {\left(\Im \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)\right)$
51 ax-resscn ${⊢}ℝ\subseteq ℂ$
52 fss ${⊢}\left({F}:{A}⟶ℝ\wedge ℝ\subseteq ℂ\right)\to {F}:{A}⟶ℂ$
53 51 52 mpan2 ${⊢}{F}:{A}⟶ℝ\to {F}:{A}⟶ℂ$
54 mblss ${⊢}{A}\in \mathrm{dom}vol\to {A}\subseteq ℝ$
55 cnex ${⊢}ℂ\in \mathrm{V}$
56 reex ${⊢}ℝ\in \mathrm{V}$
57 elpm2r ${⊢}\left(\left(ℂ\in \mathrm{V}\wedge ℝ\in \mathrm{V}\right)\wedge \left({F}:{A}⟶ℂ\wedge {A}\subseteq ℝ\right)\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)$
58 55 56 57 mpanl12 ${⊢}\left({F}:{A}⟶ℂ\wedge {A}\subseteq ℝ\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)$
59 53 54 58 syl2an ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to {F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)$
60 59 biantrurd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \left(\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\wedge {\left(\Im \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)↔\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge \forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\wedge {\left(\Im \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)\right)\right)$
61 50 60 bitrd ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \left(\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol↔\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge \forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\wedge {\left(\Im \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)\right)\right)$
62 ismbf1 ${⊢}{F}\in MblFn↔\left({F}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge \forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\wedge {\left(\Im \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)\right)$
63 61 62 syl6rbbr ${⊢}\left({F}:{A}⟶ℝ\wedge {A}\in \mathrm{dom}vol\right)\to \left({F}\in MblFn↔\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)$
64 63 ex ${⊢}{F}:{A}⟶ℝ\to \left({A}\in \mathrm{dom}vol\to \left({F}\in MblFn↔\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)\right)$
65 4 14 64 pm5.21ndd ${⊢}{F}:{A}⟶ℝ\to \left({F}\in MblFn↔\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol\right)$