# Metamath Proof Explorer

## Theorem smfpimioo

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfpimioo.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
smfpimioo.f ${⊢}{\phi }\to {F}\in \mathrm{SMblFn}\left({S}\right)$
smfpimioo.d ${⊢}{D}=\mathrm{dom}{F}$
smfpimioo.a ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
smfpimioo.b ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
Assertion smfpimioo ${⊢}{\phi }\to {{F}}^{-1}\left[\left({A},{B}\right)\right]\in \left({S}{↾}_{𝑡}{D}\right)$

### Proof

Step Hyp Ref Expression
1 smfpimioo.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
2 smfpimioo.f ${⊢}{\phi }\to {F}\in \mathrm{SMblFn}\left({S}\right)$
3 smfpimioo.d ${⊢}{D}=\mathrm{dom}{F}$
4 smfpimioo.a ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
5 smfpimioo.b ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
6 1 2 3 smff ${⊢}{\phi }\to {F}:{D}⟶ℝ$
7 6 feqmptd ${⊢}{\phi }\to {F}=\left({x}\in {D}⟼{F}\left({x}\right)\right)$
8 7 cnveqd ${⊢}{\phi }\to {{F}}^{-1}={\left({x}\in {D}⟼{F}\left({x}\right)\right)}^{-1}$
9 8 imaeq1d ${⊢}{\phi }\to {{F}}^{-1}\left[\left({A},{B}\right)\right]={\left({x}\in {D}⟼{F}\left({x}\right)\right)}^{-1}\left[\left({A},{B}\right)\right]$
10 eqid ${⊢}\left({x}\in {D}⟼{F}\left({x}\right)\right)=\left({x}\in {D}⟼{F}\left({x}\right)\right)$
11 10 mptpreima ${⊢}{\left({x}\in {D}⟼{F}\left({x}\right)\right)}^{-1}\left[\left({A},{B}\right)\right]=\left\{{x}\in {D}|{F}\left({x}\right)\in \left({A},{B}\right)\right\}$
12 11 a1i ${⊢}{\phi }\to {\left({x}\in {D}⟼{F}\left({x}\right)\right)}^{-1}\left[\left({A},{B}\right)\right]=\left\{{x}\in {D}|{F}\left({x}\right)\in \left({A},{B}\right)\right\}$
13 9 12 eqtrd ${⊢}{\phi }\to {{F}}^{-1}\left[\left({A},{B}\right)\right]=\left\{{x}\in {D}|{F}\left({x}\right)\in \left({A},{B}\right)\right\}$
14 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
15 1 uniexd ${⊢}{\phi }\to \bigcup {S}\in \mathrm{V}$
16 1 2 3 smfdmss ${⊢}{\phi }\to {D}\subseteq \bigcup {S}$
17 15 16 ssexd ${⊢}{\phi }\to {D}\in \mathrm{V}$
18 6 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {D}\right)\to {F}\left({x}\right)\in ℝ$
19 7 2 eqeltrrd ${⊢}{\phi }\to \left({x}\in {D}⟼{F}\left({x}\right)\right)\in \mathrm{SMblFn}\left({S}\right)$
20 14 1 17 18 19 4 5 smfpimioompt ${⊢}{\phi }\to \left\{{x}\in {D}|{F}\left({x}\right)\in \left({A},{B}\right)\right\}\in \left({S}{↾}_{𝑡}{D}\right)$
21 13 20 eqeltrd ${⊢}{\phi }\to {{F}}^{-1}\left[\left({A},{B}\right)\right]\in \left({S}{↾}_{𝑡}{D}\right)$