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 φMranmeasures
mbfmbfm.2 φJTop
mbfmbfm.3 φFdomMMblFnμ𝛔J
Assertion mbfmbfm φFranMblFnμ

Proof

Step Hyp Ref Expression
1 mbfmbfm.1 φMranmeasures
2 mbfmbfm.2 φJTop
3 mbfmbfm.3 φFdomMMblFnμ𝛔J
4 measbasedom MranmeasuresMmeasuresdomM
5 4 biimpi MranmeasuresMmeasuresdomM
6 measbase MmeasuresdomMdomMransigAlgebra
7 1 5 6 3syl φdomMransigAlgebra
8 2 sgsiga φ𝛔JransigAlgebra
9 7 8 3 isanmbfm φFranMblFnμ