# Metamath Proof Explorer

## Theorem isanmbfm

Description: The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-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)$
Assertion isanmbfm ${⊢}{\phi }\to {F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$

### 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 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)$
5 3 4 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)$
6 unieq ${⊢}{s}={S}\to \bigcup {s}=\bigcup {S}$
7 6 oveq2d ${⊢}{s}={S}\to {\bigcup {t}}^{\bigcup {s}}={\bigcup {t}}^{\bigcup {S}}$
8 7 eleq2d ${⊢}{s}={S}\to \left({F}\in \left({\bigcup {t}}^{\bigcup {s}}\right)↔{F}\in \left({\bigcup {t}}^{\bigcup {S}}\right)\right)$
9 eleq2 ${⊢}{s}={S}\to \left({{F}}^{-1}\left[{x}\right]\in {s}↔{{F}}^{-1}\left[{x}\right]\in {S}\right)$
10 9 ralbidv ${⊢}{s}={S}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {s}↔\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {S}\right)$
11 8 10 anbi12d ${⊢}{s}={S}\to \left(\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)↔\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)$
12 unieq ${⊢}{t}={T}\to \bigcup {t}=\bigcup {T}$
13 12 oveq1d ${⊢}{t}={T}\to {\bigcup {t}}^{\bigcup {S}}={\bigcup {T}}^{\bigcup {S}}$
14 13 eleq2d ${⊢}{t}={T}\to \left({F}\in \left({\bigcup {t}}^{\bigcup {S}}\right)↔{F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)\right)$
15 raleq ${⊢}{t}={T}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {S}↔\forall {x}\in {T}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{x}\right]\in {S}\right)$
16 14 15 anbi12d ${⊢}{t}={T}\to \left(\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)↔\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)$
17 11 16 rspc2ev ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \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)\to \exists {s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\exists {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\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)$
18 1 2 5 17 syl3anc ${⊢}{\phi }\to \exists {s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\exists {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\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)$
19 elunirnmbfm ${⊢}{F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }↔\exists {s}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\exists {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\phantom{\rule{.4em}{0ex}}\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)$
20 18 19 sylibr ${⊢}{\phi }\to {F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$