# Metamath Proof Explorer

## Theorem mbfima

Description: Definitional property of a measurable function: the preimage of an open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbfima ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to {{F}}^{-1}\left[\left({B},{C}\right)\right]\in \mathrm{dom}vol$

### Proof

Step Hyp Ref Expression
1 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)$
2 1 biimpac ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to \forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol$
3 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
4 ffn ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\to \left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
5 3 4 ax-mp ${⊢}\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
6 fnovrn ${⊢}\left(\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({B},{C}\right)\in \mathrm{ran}\left(.\right)$
7 5 6 mp3an1 ${⊢}\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({B},{C}\right)\in \mathrm{ran}\left(.\right)$
8 imaeq2 ${⊢}{x}=\left({B},{C}\right)\to {{F}}^{-1}\left[{x}\right]={{F}}^{-1}\left[\left({B},{C}\right)\right]$
9 8 eleq1d ${⊢}{x}=\left({B},{C}\right)\to \left({{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol↔{{F}}^{-1}\left[\left({B},{C}\right)\right]\in \mathrm{dom}vol\right)$
10 9 rspccva ${⊢}\left(\forall {x}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in \mathrm{dom}vol\wedge \left({B},{C}\right)\in \mathrm{ran}\left(.\right)\right)\to {{F}}^{-1}\left[\left({B},{C}\right)\right]\in \mathrm{dom}vol$
11 2 7 10 syl2an ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\wedge \left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\right)\to {{F}}^{-1}\left[\left({B},{C}\right)\right]\in \mathrm{dom}vol$
12 ndmioo ${⊢}¬\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to \left({B},{C}\right)=\varnothing$
13 12 imaeq2d ${⊢}¬\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to {{F}}^{-1}\left[\left({B},{C}\right)\right]={{F}}^{-1}\left[\varnothing \right]$
14 ima0 ${⊢}{{F}}^{-1}\left[\varnothing \right]=\varnothing$
15 13 14 syl6eq ${⊢}¬\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to {{F}}^{-1}\left[\left({B},{C}\right)\right]=\varnothing$
16 0mbl ${⊢}\varnothing \in \mathrm{dom}vol$
17 15 16 eqeltrdi ${⊢}¬\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to {{F}}^{-1}\left[\left({B},{C}\right)\right]\in \mathrm{dom}vol$
18 17 adantl ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\wedge ¬\left({B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\right)\to {{F}}^{-1}\left[\left({B},{C}\right)\right]\in \mathrm{dom}vol$
19 11 18 pm2.61dan ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to {{F}}^{-1}\left[\left({B},{C}\right)\right]\in \mathrm{dom}vol$