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	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
	mbfmbfmOLD.2	⊢ ( 𝜑 → 𝐽 ∈ Top )
	mbfmbfmOLD.3	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM ( sigaGen ‘ 𝐽 ) ) )
Assertion	mbfmbfmOLD	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )

Proof

Step	Hyp	Ref	Expression
1		mbfmbfmOLD.1	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
2		mbfmbfmOLD.2	⊢ ( 𝜑 → 𝐽 ∈ Top )
3		mbfmbfmOLD.3	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM ( sigaGen ‘ 𝐽 ) ) )
4	3	isanmbfm	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )