Theorem mbfmbfm

Description: A measurable function to a Borel Set is measurable. (Contributed by Thierry Arnoux, 24-Jan-2017) Remove hypotheses. (Revised by SN, 13-Jan-2025)

	Ref	Expression
Hypothesis	mbfmbfm.1	$$⊢\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 F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }𝛔\left(J\right)\right)$$
2	1	isanmbfm	$$⊢\phi \to F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$$