Theorem mbfmbfmOLD

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

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

Proof

Step	Hyp	Ref	Expression
1		mbfmbfmOLD.1	|- ( ph -> M e. U. ran measures )
2		mbfmbfmOLD.2	|- ( ph -> J e. Top )
3		mbfmbfmOLD.3	|- ( ph -> F e. ( dom M MblFnM ( sigaGen ` J ) ) )
4	3	isanmbfm	|- ( ph -> F e. U. ran MblFnM )