# Metamath Proof Explorer

## Theorem smfpimgtxrmpt

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

Ref Expression
Hypotheses smfpimgtxrmpt.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
smfpimgtxrmpt.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
smfpimgtxrmpt.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
smfpimgtxrmpt.f ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in \mathrm{SMblFn}\left({S}\right)$
smfpimgtxrmpt.l ${⊢}{\phi }\to {L}\in {ℝ}^{*}$
Assertion smfpimgtxrmpt ${⊢}{\phi }\to \left\{{x}\in {A}|{L}<{B}\right\}\in \left({S}{↾}_{𝑡}{A}\right)$

### Proof

Step Hyp Ref Expression
1 smfpimgtxrmpt.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 smfpimgtxrmpt.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
3 smfpimgtxrmpt.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
4 smfpimgtxrmpt.f ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in \mathrm{SMblFn}\left({S}\right)$
5 smfpimgtxrmpt.l ${⊢}{\phi }\to {L}\in {ℝ}^{*}$
6 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)$
7 6 nfdm ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
8 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
9 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)$
10 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{L}$
11 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}<$
12 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
13 6 12 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)\left({y}\right)$
14 10 11 13 nfbr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{L}<\left({x}\in {A}⟼{B}\right)\left({y}\right)$
15 fveq2 ${⊢}{x}={y}\to \left({x}\in {A}⟼{B}\right)\left({x}\right)=\left({x}\in {A}⟼{B}\right)\left({y}\right)$
16 15 breq2d ${⊢}{x}={y}\to \left({L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)↔{L}<\left({x}\in {A}⟼{B}\right)\left({y}\right)\right)$
17 7 8 9 14 16 cbvrabw ${⊢}\left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)\right\}=\left\{{y}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|{L}<\left({x}\in {A}⟼{B}\right)\left({y}\right)\right\}$
18 17 a1i ${⊢}{\phi }\to \left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)\right\}=\left\{{y}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|{L}<\left({x}\in {A}⟼{B}\right)\left({y}\right)\right\}$
19 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)$
20 eqid ${⊢}\mathrm{dom}\left({x}\in {A}⟼{B}\right)=\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
21 19 2 4 20 5 smfpimgtxr ${⊢}{\phi }\to \left\{{y}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|{L}<\left({x}\in {A}⟼{B}\right)\left({y}\right)\right\}\in \left({S}{↾}_{𝑡}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\right)$
22 18 21 eqeltrd ${⊢}{\phi }\to \left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)\right\}\in \left({S}{↾}_{𝑡}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\right)$
23 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
24 1 23 3 dmmptdf ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
25 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
26 7 25 rabeqf ${⊢}\mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}\to \left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)\right\}=\left\{{x}\in {A}|{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)\right\}$
27 24 26 syl ${⊢}{\phi }\to \left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)\right\}=\left\{{x}\in {A}|{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)\right\}$
28 23 a1i ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
29 28 3 fvmpt2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
30 29 breq2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)↔{L}<{B}\right)$
31 1 30 rabbida ${⊢}{\phi }\to \left\{{x}\in {A}|{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)\right\}=\left\{{x}\in {A}|{L}<{B}\right\}$
32 eqidd ${⊢}{\phi }\to \left\{{x}\in {A}|{L}<{B}\right\}=\left\{{x}\in {A}|{L}<{B}\right\}$
33 27 31 32 3eqtrrd ${⊢}{\phi }\to \left\{{x}\in {A}|{L}<{B}\right\}=\left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)\right\}$
34 24 eqcomd ${⊢}{\phi }\to {A}=\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
35 34 oveq2d ${⊢}{\phi }\to {S}{↾}_{𝑡}{A}={S}{↾}_{𝑡}\mathrm{dom}\left({x}\in {A}⟼{B}\right)$
36 33 35 eleq12d ${⊢}{\phi }\to \left(\left\{{x}\in {A}|{L}<{B}\right\}\in \left({S}{↾}_{𝑡}{A}\right)↔\left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|{L}<\left({x}\in {A}⟼{B}\right)\left({x}\right)\right\}\in \left({S}{↾}_{𝑡}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\right)\right)$
37 22 36 mpbird ${⊢}{\phi }\to \left\{{x}\in {A}|{L}<{B}\right\}\in \left({S}{↾}_{𝑡}{A}\right)$