# Metamath Proof Explorer

## Theorem mbfmf

Description: A measurable function as a function with domain and codomain. (Contributed by Thierry Arnoux, 25-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 mbfmf ${⊢}{\phi }\to {F}:\bigcup {S}⟶\bigcup {T}$

### 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 5 simpld ${⊢}{\phi }\to {F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)$
7 elmapi ${⊢}{F}\in \left({\bigcup {T}}^{\bigcup {S}}\right)\to {F}:\bigcup {S}⟶\bigcup {T}$
8 6 7 syl ${⊢}{\phi }\to {F}:\bigcup {S}⟶\bigcup {T}$