# Metamath Proof Explorer

## Theorem mbfmbfm

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

Ref Expression
Hypotheses mbfmbfm.1 ${⊢}{\phi }\to {M}\in \bigcup \mathrm{ran}\mathrm{measures}$
mbfmbfm.2 ${⊢}{\phi }\to {J}\in \mathrm{Top}$
mbfmbfm.3 ${⊢}{\phi }\to {F}\in \left(\mathrm{dom}{M}{\mathrm{MblFn}}_{\mu }𝛔\left({J}\right)\right)$
Assertion mbfmbfm ${⊢}{\phi }\to {F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$

### Proof

Step Hyp Ref Expression
1 mbfmbfm.1 ${⊢}{\phi }\to {M}\in \bigcup \mathrm{ran}\mathrm{measures}$
2 mbfmbfm.2 ${⊢}{\phi }\to {J}\in \mathrm{Top}$
3 mbfmbfm.3 ${⊢}{\phi }\to {F}\in \left(\mathrm{dom}{M}{\mathrm{MblFn}}_{\mu }𝛔\left({J}\right)\right)$
4 measbasedom ${⊢}{M}\in \bigcup \mathrm{ran}\mathrm{measures}↔{M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)$
5 4 biimpi ${⊢}{M}\in \bigcup \mathrm{ran}\mathrm{measures}\to {M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)$
6 measbase ${⊢}{M}\in \mathrm{measures}\left(\mathrm{dom}{M}\right)\to \mathrm{dom}{M}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
7 1 5 6 3syl ${⊢}{\phi }\to \mathrm{dom}{M}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
8 2 sgsiga ${⊢}{\phi }\to 𝛔\left({J}\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
9 7 8 3 isanmbfm ${⊢}{\phi }\to {F}\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$