# Metamath Proof Explorer

## Theorem mbfimaicc

Description: The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion mbfimaicc ${⊢}\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$

### Proof

Step Hyp Ref Expression
1 iccssre ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to \left[{B},{C}\right]\subseteq ℝ$
2 1 adantl ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\wedge \left({B}\in ℝ\wedge {C}\in ℝ\right)\right)\to \left[{B},{C}\right]\subseteq ℝ$
3 dfss4 ${⊢}\left[{B},{C}\right]\subseteq ℝ↔ℝ\setminus \left(ℝ\setminus \left[{B},{C}\right]\right)=\left[{B},{C}\right]$
4 2 3 sylib ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\wedge \left({B}\in ℝ\wedge {C}\in ℝ\right)\right)\to ℝ\setminus \left(ℝ\setminus \left[{B},{C}\right]\right)=\left[{B},{C}\right]$
5 difreicc ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to ℝ\setminus \left[{B},{C}\right]=\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)$
6 5 adantl ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\wedge \left({B}\in ℝ\wedge {C}\in ℝ\right)\right)\to ℝ\setminus \left[{B},{C}\right]=\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)$
7 6 difeq2d ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\wedge \left({B}\in ℝ\wedge {C}\in ℝ\right)\right)\to ℝ\setminus \left(ℝ\setminus \left[{B},{C}\right]\right)=ℝ\setminus \left(\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right)$
8 4 7 eqtr3d ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\wedge \left({B}\in ℝ\wedge {C}\in ℝ\right)\right)\to \left[{B},{C}\right]=ℝ\setminus \left(\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right)$
9 8 imaeq2d ${⊢}\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]={{F}}^{-1}\left[ℝ\setminus \left(\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right)\right]$
10 ffun ${⊢}{F}:{A}⟶ℝ\to \mathrm{Fun}{F}$
11 funcnvcnv ${⊢}\mathrm{Fun}{F}\to \mathrm{Fun}{{{F}}^{-1}}^{-1}$
12 10 11 syl ${⊢}{F}:{A}⟶ℝ\to \mathrm{Fun}{{{F}}^{-1}}^{-1}$
13 12 ad2antlr ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\wedge \left({B}\in ℝ\wedge {C}\in ℝ\right)\right)\to \mathrm{Fun}{{{F}}^{-1}}^{-1}$
14 imadif ${⊢}\mathrm{Fun}{{{F}}^{-1}}^{-1}\to {{F}}^{-1}\left[ℝ\setminus \left(\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right)\right]={{F}}^{-1}\left[ℝ\right]\setminus {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right]$
15 13 14 syl ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\wedge \left({B}\in ℝ\wedge {C}\in ℝ\right)\right)\to {{F}}^{-1}\left[ℝ\setminus \left(\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right)\right]={{F}}^{-1}\left[ℝ\right]\setminus {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right]$
16 9 15 eqtrd ${⊢}\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]={{F}}^{-1}\left[ℝ\right]\setminus {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right]$
17 fimacnv ${⊢}{F}:{A}⟶ℝ\to {{F}}^{-1}\left[ℝ\right]={A}$
18 17 adantl ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to {{F}}^{-1}\left[ℝ\right]={A}$
19 mbfdm ${⊢}{F}\in MblFn\to \mathrm{dom}{F}\in \mathrm{dom}vol$
20 fdm ${⊢}{F}:{A}⟶ℝ\to \mathrm{dom}{F}={A}$
21 20 eleq1d ${⊢}{F}:{A}⟶ℝ\to \left(\mathrm{dom}{F}\in \mathrm{dom}vol↔{A}\in \mathrm{dom}vol\right)$
22 21 biimpac ${⊢}\left(\mathrm{dom}{F}\in \mathrm{dom}vol\wedge {F}:{A}⟶ℝ\right)\to {A}\in \mathrm{dom}vol$
23 19 22 sylan ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to {A}\in \mathrm{dom}vol$
24 18 23 eqeltrd ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to {{F}}^{-1}\left[ℝ\right]\in \mathrm{dom}vol$
25 imaundi ${⊢}{{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right]={{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]\cup {{F}}^{-1}\left[\left({C},\mathrm{+\infty }\right)\right]$
26 mbfima ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]\in \mathrm{dom}vol$
27 mbfima ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to {{F}}^{-1}\left[\left({C},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
28 unmbl ${⊢}\left({{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]\in \mathrm{dom}vol\wedge {{F}}^{-1}\left[\left({C},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]\cup {{F}}^{-1}\left[\left({C},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
29 26 27 28 syl2anc ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\right]\cup {{F}}^{-1}\left[\left({C},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
30 25 29 eqeltrid ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
31 difmbl ${⊢}\left({{F}}^{-1}\left[ℝ\right]\in \mathrm{dom}vol\wedge {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol\right)\to {{F}}^{-1}\left[ℝ\right]\setminus {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
32 24 30 31 syl2anc ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\to {{F}}^{-1}\left[ℝ\right]\setminus {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
33 32 adantr ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶ℝ\right)\wedge \left({B}\in ℝ\wedge {C}\in ℝ\right)\right)\to {{F}}^{-1}\left[ℝ\right]\setminus {{F}}^{-1}\left[\left(\mathrm{-\infty },{B}\right)\cup \left({C},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
34 16 33 eqeltrd ${⊢}\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$