# Metamath Proof Explorer

## Theorem smfpimltxrmpt

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

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

### Proof

Step Hyp Ref Expression
1 smfpimltxrmpt.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 smfpimltxrmpt.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
3 smfpimltxrmpt.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
4 smfpimltxrmpt.f ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in \mathrm{SMblFn}\left({S}\right)$
5 smfpimltxrmpt.r ${⊢}{\phi }\to {R}\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}}\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}$
10 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
11 6 10 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)\left({y}\right)$
12 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}<$
13 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{R}$
14 11 12 13 nfbr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)\left({y}\right)<{R}$
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 breq1d ${⊢}{x}={y}\to \left(\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}↔\left({x}\in {A}⟼{B}\right)\left({y}\right)<{R}\right)$
17 7 8 9 14 16 cbvrabw ${⊢}\left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}\right\}=\left\{{y}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({x}\in {A}⟼{B}\right)\left({y}\right)<{R}\right\}$
18 17 a1i ${⊢}{\phi }\to \left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}\right\}=\left\{{y}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({x}\in {A}⟼{B}\right)\left({y}\right)<{R}\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 smfpimltxr ${⊢}{\phi }\to \left\{{y}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({x}\in {A}⟼{B}\right)\left({y}\right)<{R}\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)|\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}\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)|\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}\right\}=\left\{{x}\in {A}|\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}\right\}$
27 24 26 syl ${⊢}{\phi }\to \left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}\right\}=\left\{{x}\in {A}|\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}\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 breq1d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}↔{B}<{R}\right)$
31 1 30 rabbida ${⊢}{\phi }\to \left\{{x}\in {A}|\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}\right\}=\left\{{x}\in {A}|{B}<{R}\right\}$
32 eqidd ${⊢}{\phi }\to \left\{{x}\in {A}|{B}<{R}\right\}=\left\{{x}\in {A}|{B}<{R}\right\}$
33 27 31 32 3eqtrrd ${⊢}{\phi }\to \left\{{x}\in {A}|{B}<{R}\right\}=\left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}\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}|{B}<{R}\right\}\in \left({S}{↾}_{𝑡}{A}\right)↔\left\{{x}\in \mathrm{dom}\left({x}\in {A}⟼{B}\right)|\left({x}\in {A}⟼{B}\right)\left({x}\right)<{R}\right\}\in \left({S}{↾}_{𝑡}\mathrm{dom}\left({x}\in {A}⟼{B}\right)\right)\right)$
37 22 36 mpbird ${⊢}{\phi }\to \left\{{x}\in {A}|{B}<{R}\right\}\in \left({S}{↾}_{𝑡}{A}\right)$