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	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM ( sigaGen ‘ 𝐽 ) ) )
Assertion	mbfmbfm	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )

Proof

Step	Hyp	Ref	Expression
1		mbfmbfm.1	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM ( sigaGen ‘ 𝐽 ) ) )
2	1	isanmbfm	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )