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	|- ( ph -> X e. Fin )
	borelmbl.s	|- S = dom ( voln ` X )
	borelmbl.b	|- B = ( SalGen ` ( TopOpen ` ( RR^ ` X ) ) )
Assertion	borelmbl	|- ( ph -> B C_ S )

Proof

Step	Hyp	Ref	Expression
1		borelmbl.x	|- ( ph -> X e. Fin )
2		borelmbl.s	|- S = dom ( voln ` X )
3		borelmbl.b	|- B = ( SalGen ` ( TopOpen ` ( RR^ ` X ) ) )
4		fvexd	|- ( ph -> ( TopOpen ` ( RR^ ` X ) ) e. _V )
5	1 2	dmovnsal	|- ( ph -> S e. SAlg )
6	1	adantr	|- ( ( ph /\ y e. ( TopOpen ` ( RR^ ` X ) ) ) -> X e. Fin )
7		simpr	|- ( ( ph /\ y e. ( TopOpen ` ( RR^ ` X ) ) ) -> y e. ( TopOpen ` ( RR^ ` X ) ) )
8	6 2 7	opnvonmbl	|- ( ( ph /\ y e. ( TopOpen ` ( RR^ ` X ) ) ) -> y e. S )
9	8	ssd	|- ( ph -> ( TopOpen ` ( RR^ ` X ) ) C_ S )
10		eqid	|- dom ( voln ` X ) = dom ( voln ` X )
11	1 10	unidmvon	|- ( ph -> U. dom ( voln ` X ) = ( RR ^m X ) )
12	2	unieqi	|- U. S = U. dom ( voln ` X )
13	12	a1i	|- ( ph -> U. S = U. dom ( voln ` X ) )
14		rrxunitopnfi	|- ( X e. Fin -> U. ( TopOpen ` ( RR^ ` X ) ) = ( RR ^m X ) )
15	1 14	syl	|- ( ph -> U. ( TopOpen ` ( RR^ ` X ) ) = ( RR ^m X ) )
16	11 13 15	3eqtr4d	|- ( ph -> U. S = U. ( TopOpen ` ( RR^ ` X ) ) )
17	4 3 5 9 16	salgenss	|- ( ph -> B C_ S )