Metamath Proof Explorer

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	$⊢ φ \to X \in Fin$
		bormflebmf.b	$⊢ B = SalGen (TopOpen (X))$
		bormflebmf.l	$⊢ L = dom voln (X)$
		bormflebmf.f	$⊢ φ \to F \in SMblFn (B)$
	Assertion	bormflebmf	$⊢ φ \to F \in SMblFn (L)$

Proof

Step	Hyp	Ref	Expression
1		bormflebmf.x	$⊢ φ \to X \in Fin$
2		bormflebmf.b	$⊢ B = SalGen (TopOpen (X))$
3		bormflebmf.l	$⊢ L = dom voln (X)$
4		bormflebmf.f	$⊢ φ \to F \in SMblFn (B)$
5		fvexd	$⊢ φ \to TopOpen (X) \in V$
6	5 2	salgencld	$⊢ φ \to B \in SAlg$
7	1 3	dmovnsal	$⊢ φ \to L \in SAlg$
8	1 3 2	borelmbl	$⊢ φ \to B \subseteq L$
9	6 7 8 4	smfsssmf	$⊢ φ \to F \in SMblFn (L)$