Theorem mbfmbfm

Description: A measurable function to a Borel Set is measurable. (Contributed by Thierry Arnoux, 24-Jan-2017)

	Ref	Expression
Hypotheses	mbfmbfm.1	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
	mbfmbfm.2	⊢ ( 𝜑 → 𝐽 ∈ Top )
	mbfmbfm.3	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM ( sigaGen ‘ 𝐽 ) ) )
Assertion	mbfmbfm	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )

Proof

Step	Hyp	Ref	Expression
1		mbfmbfm.1	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
2		mbfmbfm.2	⊢ ( 𝜑 → 𝐽 ∈ Top )
3		mbfmbfm.3	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM ( sigaGen ‘ 𝐽 ) ) )
4		measbasedom	⊢ ( 𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
5	4	biimpi	⊢ ( 𝑀 ∈ ∪ ran measures → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
6		measbase	⊢ ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) → dom 𝑀 ∈ ∪ ran sigAlgebra )
7	1 5 6	3syl	⊢ ( 𝜑 → dom 𝑀 ∈ ∪ ran sigAlgebra )
8	2	sgsiga	⊢ ( 𝜑 → ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra )
9	7 8 3	isanmbfm	⊢ ( 𝜑 → 𝐹 ∈ ∪ ran MblFnM )