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}\leftrightarrow 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 }$$