# Metamath Proof Explorer

## Theorem mbfmfun

Description: A measurable function is a function. (Contributed by Thierry Arnoux, 24-Jan-2017)

Ref Expression
Hypothesis mbfmfun.1 ${⊢}{\phi }\to {F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$
Assertion mbfmfun ${⊢}{\phi }\to \mathrm{Fun}{F}$

### Proof

Step Hyp Ref Expression
1 mbfmfun.1 ${⊢}{\phi }\to {F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$
2 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)$
3 2 biimpi ${⊢}{F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }\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)$
4 elmapfun ${⊢}{F}\in \left({\bigcup {t}}^{\bigcup {s}}\right)\to \mathrm{Fun}{F}$
5 4 adantr ${⊢}\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)\to \mathrm{Fun}{F}$
6 5 rexlimivw ${⊢}\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)\to \mathrm{Fun}{F}$
7 6 rexlimivw ${⊢}\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)\to \mathrm{Fun}{F}$
8 1 3 7 3syl ${⊢}{\phi }\to \mathrm{Fun}{F}$