Theorem bormflebmf

Description: A Borel measurable function is Lebesgue measurable. Proposition 121D (a) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	bormflebmf.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	bormflebmf.b	⊢ 𝐵 = ( SalGen ‘ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
	bormflebmf.l	⊢ 𝐿 = dom ( voln ‘ 𝑋 )
	bormflebmf.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝐵 ) )
Assertion	bormflebmf	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		bormflebmf.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		bormflebmf.b	⊢ 𝐵 = ( SalGen ‘ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
3		bormflebmf.l	⊢ 𝐿 = dom ( voln ‘ 𝑋 )
4		bormflebmf.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝐵 ) )
5		fvexd	⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ V )
6	5 2	salgencld	⊢ ( 𝜑 → 𝐵 ∈ SAlg )
7	1 3	dmovnsal	⊢ ( 𝜑 → 𝐿 ∈ SAlg )
8	1 3 2	borelmbl	⊢ ( 𝜑 → 𝐵 ⊆ 𝐿 )
9	6 7 8 4	smfsssmf	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝐿 ) )