# Metamath Proof Explorer

## Theorem smfpimioompt

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 smfpimioompt.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
smfpimioompt.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
smfpimioompt.a ${⊢}{\phi }\to {A}\in {V}$
smfpimioompt.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {W}$
smfpimioompt.m ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in \mathrm{SMblFn}\left({S}\right)$
smfpimioompt.l ${⊢}{\phi }\to {L}\in {ℝ}^{*}$
smfpimioompt.r ${⊢}{\phi }\to {R}\in {ℝ}^{*}$
Assertion smfpimioompt ${⊢}{\phi }\to \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}\in \left({S}{↾}_{𝑡}{A}\right)$

### Proof

Step Hyp Ref Expression
1 smfpimioompt.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 smfpimioompt.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
3 smfpimioompt.a ${⊢}{\phi }\to {A}\in {V}$
4 smfpimioompt.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {W}$
5 smfpimioompt.m ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in \mathrm{SMblFn}\left({S}\right)$
6 smfpimioompt.l ${⊢}{\phi }\to {L}\in {ℝ}^{*}$
7 smfpimioompt.r ${⊢}{\phi }\to {R}\in {ℝ}^{*}$
8 eqid ${⊢}\mathrm{dom}\left({x}\in {A}⟼{B}\right)=\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
9 2 5 8 smff ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right):\mathrm{dom}\left({x}\in {A}⟼{B}\right)⟶ℝ$
10 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
11 1 10 4 dmmptdf ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
12 11 feq2d ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right):\mathrm{dom}\left({x}\in {A}⟼{B}\right)⟶ℝ↔\left({x}\in {A}⟼{B}\right):{A}⟶ℝ\right)$
13 9 12 mpbid ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right):{A}⟶ℝ$
14 13 fvmptelrn ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
15 14 rexrd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {ℝ}^{*}$
16 1 6 7 15 pimiooltgt ${⊢}{\phi }\to \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}=\left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}$
17 eqid ${⊢}{S}{↾}_{𝑡}{A}={S}{↾}_{𝑡}{A}$
18 2 3 17 subsalsal ${⊢}{\phi }\to {S}{↾}_{𝑡}{A}\in \mathrm{SAlg}$
19 1 2 4 5 7 smfpimltxrmpt ${⊢}{\phi }\to \left\{{x}\in {A}|{B}<{R}\right\}\in \left({S}{↾}_{𝑡}{A}\right)$
20 1 2 4 5 6 smfpimgtxrmpt ${⊢}{\phi }\to \left\{{x}\in {A}|{L}<{B}\right\}\in \left({S}{↾}_{𝑡}{A}\right)$
21 18 19 20 salincld ${⊢}{\phi }\to \left\{{x}\in {A}|{B}<{R}\right\}\cap \left\{{x}\in {A}|{L}<{B}\right\}\in \left({S}{↾}_{𝑡}{A}\right)$
22 16 21 eqeltrd ${⊢}{\phi }\to \left\{{x}\in {A}|{B}\in \left({L},{R}\right)\right\}\in \left({S}{↾}_{𝑡}{A}\right)$