Theorem borelmbl

Description: All Borel subsets of the n-dimensional Real numbers are Lebesgue measurable. This is Proposition 115G (b) of Fremlin1 p. 32. See also Definition 111G (d) of Fremlin1 p. 13. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	borelmbl.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	borelmbl.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
	borelmbl.b
Assertion	borelmbl	$$⊢\phi \to B\subseteq S$$

Proof

Step	Hyp	Ref	Expression
1		borelmbl.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		borelmbl.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
3		borelmbl.b
4		fvexd
5	1 2	dmovnsal	$$⊢\phi \to S\in \mathrm{SAlg}$$
6	1	adantr
7		simpr
8	6 2 7	opnvonmbl
9	8	ssd
10		eqid	$$⊢\mathrm{dom}\mathrm{voln}\left(X\right)=\mathrm{dom}\mathrm{voln}\left(X\right)$$
11	1 10	unidmvon	$$⊢\phi \to \bigcup \mathrm{dom}\mathrm{voln}\left(X\right)={ℝ}^X$$
12	2	unieqi	$$⊢\bigcup S=\bigcup \mathrm{dom}\mathrm{voln}\left(X\right)$$
13	12	a1i	$$⊢\phi \to \bigcup S=\bigcup \mathrm{dom}\mathrm{voln}\left(X\right)$$
14		rrxunitopnfi
15	1 14	syl
16	11 13 15	3eqtr4d
17	4 3 5 9 16	salgenss	$$⊢\phi \to B\subseteq S$$