Theorem mbfmbfm

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

	Ref	Expression
Hypotheses	mbfmbfm.1	|- ( ph -> M e. U. ran measures )
	mbfmbfm.2	|- ( ph -> J e. Top )
	mbfmbfm.3	|- ( ph -> F e. ( dom M MblFnM ( sigaGen ` J ) ) )
Assertion	mbfmbfm	|- ( ph -> F e. U. ran MblFnM )

Proof

Step	Hyp	Ref	Expression
1		mbfmbfm.1	|- ( ph -> M e. U. ran measures )
2		mbfmbfm.2	|- ( ph -> J e. Top )
3		mbfmbfm.3	|- ( ph -> F e. ( dom M MblFnM ( sigaGen ` J ) ) )
4		measbasedom	|- ( M e. U. ran measures <-> M e. ( measures ` dom M ) )
5	4	biimpi	|- ( M e. U. ran measures -> M e. ( measures ` dom M ) )
6		measbase	|- ( M e. ( measures ` dom M ) -> dom M e. U. ran sigAlgebra )
7	1 5 6	3syl	|- ( ph -> dom M e. U. ran sigAlgebra )
8	2	sgsiga	|- ( ph -> ( sigaGen ` J ) e. U. ran sigAlgebra )
9	7 8 3	isanmbfm	|- ( ph -> F e. U. ran MblFnM )