# Metamath Proof Explorer

## Theorem mbfdm

Description: The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbfdm ${⊢}{F}\in MblFn\to \mathrm{dom}{F}\in \mathrm{dom}vol$

### Proof

Step Hyp Ref Expression
1 ref ${⊢}\Re :ℂ⟶ℝ$
2 mbff ${⊢}{F}\in MblFn\to {F}:\mathrm{dom}{F}⟶ℂ$
3 fco ${⊢}\left(\Re :ℂ⟶ℝ\wedge {F}:\mathrm{dom}{F}⟶ℂ\right)\to \left(\Re \circ {F}\right):\mathrm{dom}{F}⟶ℝ$
4 1 2 3 sylancr ${⊢}{F}\in MblFn\to \left(\Re \circ {F}\right):\mathrm{dom}{F}⟶ℝ$
5 fimacnv ${⊢}\left(\Re \circ {F}\right):\mathrm{dom}{F}⟶ℝ\to {\left(\Re \circ {F}\right)}^{-1}\left[ℝ\right]=\mathrm{dom}{F}$
6 4 5 syl ${⊢}{F}\in MblFn\to {\left(\Re \circ {F}\right)}^{-1}\left[ℝ\right]=\mathrm{dom}{F}$
7 imaeq2 ${⊢}{x}=ℝ\to {\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]={\left(\Re \circ {F}\right)}^{-1}\left[ℝ\right]$
8 7 eleq1d ${⊢}{x}=ℝ\to \left({\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol↔{\left(\Re \circ {F}\right)}^{-1}\left[ℝ\right]\in \mathrm{dom}vol\right)$
9 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)$
10 simpl ${⊢}\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)\to {\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol$
11 10 ralimi ${⊢}\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)\to \forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol$
12 9 11 simplbiim ${⊢}{F}\in MblFn\to \forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{\left(\Re \circ {F}\right)}^{-1}\left[{x}\right]\in \mathrm{dom}vol$
13 ioomax ${⊢}\left(\mathrm{-\infty },\mathrm{+\infty }\right)=ℝ$
14 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
15 ffn ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\to \left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
16 14 15 ax-mp ${⊢}\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
17 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
18 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
19 fnovrn ${⊢}\left(\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)\wedge \mathrm{-\infty }\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(\mathrm{-\infty },\mathrm{+\infty }\right)\in \mathrm{ran}\left(.\right)$
20 16 17 18 19 mp3an ${⊢}\left(\mathrm{-\infty },\mathrm{+\infty }\right)\in \mathrm{ran}\left(.\right)$
21 13 20 eqeltrri ${⊢}ℝ\in \mathrm{ran}\left(.\right)$
22 21 a1i ${⊢}{F}\in MblFn\to ℝ\in \mathrm{ran}\left(.\right)$
23 8 12 22 rspcdva ${⊢}{F}\in MblFn\to {\left(\Re \circ {F}\right)}^{-1}\left[ℝ\right]\in \mathrm{dom}vol$
24 6 23 eqeltrrd ${⊢}{F}\in MblFn\to \mathrm{dom}{F}\in \mathrm{dom}vol$