# Metamath Proof Explorer

## Theorem mbfmcnvima

Description: The preimage by a measurable function is a measurable set. (Contributed by Thierry Arnoux, 23-Jan-2017)

Ref Expression
Hypotheses mbfmf.1 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
mbfmf.2 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
mbfmf.3 ${⊢}{\phi }\to {F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)$
mbfmcnvima.4 ${⊢}{\phi }\to {A}\in {T}$
Assertion mbfmcnvima ${⊢}{\phi }\to {{F}}^{-1}\left[{A}\right]\in {S}$

### Proof

Step Hyp Ref Expression
1 mbfmf.1 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
2 mbfmf.2 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
3 mbfmf.3 ${⊢}{\phi }\to {F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)$
4 mbfmcnvima.4 ${⊢}{\phi }\to {A}\in {T}$
5 imaeq2 ${⊢}{x}={A}\to {{F}}^{-1}\left[{x}\right]={{F}}^{-1}\left[{A}\right]$
6 5 eleq1d ${⊢}{x}={A}\to \left({{F}}^{-1}\left[{x}\right]\in {S}↔{{F}}^{-1}\left[{A}\right]\in {S}\right)$
7 1 2 ismbfm ${⊢}{\phi }\to \left({F}\in \left({S}{\mathrm{MblFn}}_{\mu }{T}\right)↔\left({F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)\wedge \forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {S}\right)\right)$
8 3 7 mpbid ${⊢}{\phi }\to \left({F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)\wedge \forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {S}\right)$
9 8 simprd ${⊢}{\phi }\to \forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {S}$
10 6 9 4 rspcdva ${⊢}{\phi }\to {{F}}^{-1}\left[{A}\right]\in {S}$