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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	borelmbl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
	borelmbl.b	⊢ 𝐵 = ( SalGen ‘ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
Assertion	borelmbl	⊢ ( 𝜑 → 𝐵 ⊆ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		borelmbl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		borelmbl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
3		borelmbl.b	⊢ 𝐵 = ( SalGen ‘ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
4		fvexd	⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ V )
5	1 2	dmovnsal	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ) → 𝑋 ∈ Fin )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ) → 𝑦 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
8	6 2 7	opnvonmbl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ) → 𝑦 ∈ 𝑆 )
9	8	ssd	⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) ⊆ 𝑆 )
10		eqid	⊢ dom ( voln ‘ 𝑋 ) = dom ( voln ‘ 𝑋 )
11	1 10	unidmvon	⊢ ( 𝜑 → ∪ dom ( voln ‘ 𝑋 ) = ( ℝ ↑m 𝑋 ) )
12	2	unieqi	⊢ ∪ 𝑆 = ∪ dom ( voln ‘ 𝑋 )
13	12	a1i	⊢ ( 𝜑 → ∪ 𝑆 = ∪ dom ( voln ‘ 𝑋 ) )
14		rrxunitopnfi	⊢ ( 𝑋 ∈ Fin → ∪ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) = ( ℝ ↑m 𝑋 ) )
15	1 14	syl	⊢ ( 𝜑 → ∪ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) = ( ℝ ↑m 𝑋 ) )
16	11 13 15	3eqtr4d	⊢ ( 𝜑 → ∪ 𝑆 = ∪ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
17	4 3 5 9 16	salgenss	⊢ ( 𝜑 → 𝐵 ⊆ 𝑆 )