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	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
	mbfmbfmOLD.2	$$⊢\phi \to J\in \mathrm{Top}$$
	mbfmbfmOLD.3	$$⊢\phi \to F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }𝛔\left(J\right)\right)$$
Assertion	mbfmbfmOLD	$$⊢\phi \to F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$$

Proof

Step	Hyp	Ref	Expression
1		mbfmbfmOLD.1	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
2		mbfmbfmOLD.2	$$⊢\phi \to J\in \mathrm{Top}$$
3		mbfmbfmOLD.3	$$⊢\phi \to F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }𝛔\left(J\right)\right)$$
4	3	isanmbfm	$$⊢\phi \to F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$$