Theorem opnvonmbl

Description: An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	opnvonmbl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	opnvonmbl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
	opnvonmbl.g	⊢ ( 𝜑 → 𝐺 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
Assertion	opnvonmbl	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		opnvonmbl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		opnvonmbl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
3		opnvonmbl.g	⊢ ( 𝜑 → 𝐺 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
4		fveq2	⊢ ( 𝑘 = 𝑖 → ( ( [,) ∘ 𝑓 ) ‘ 𝑘 ) = ( ( [,) ∘ 𝑓 ) ‘ 𝑖 ) )
5	4	cbvixpv	⊢ X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝑓 ) ‘ 𝑘 ) = X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝑓 ) ‘ 𝑖 )
6	5	a1i	⊢ ( 𝑓 = ℎ → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝑓 ) ‘ 𝑘 ) = X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝑓 ) ‘ 𝑖 ) )
7		coeq2	⊢ ( 𝑓 = ℎ → ( [,) ∘ 𝑓 ) = ( [,) ∘ ℎ ) )
8	7	fveq1d	⊢ ( 𝑓 = ℎ → ( ( [,) ∘ 𝑓 ) ‘ 𝑖 ) = ( ( [,) ∘ ℎ ) ‘ 𝑖 ) )
9	8	ixpeq2dv	⊢ ( 𝑓 = ℎ → X 𝑖 ∈ 𝑋 ( ( [,) ∘ 𝑓 ) ‘ 𝑖 ) = X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) )
10	6 9	eqtrd	⊢ ( 𝑓 = ℎ → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝑓 ) ‘ 𝑘 ) = X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) )
11	10	sseq1d	⊢ ( 𝑓 = ℎ → ( X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝑓 ) ‘ 𝑘 ) ⊆ 𝐺 ↔ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) ⊆ 𝐺 ) )
12	11	cbvrabv	⊢ { 𝑓 ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) ∣ X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝑓 ) ‘ 𝑘 ) ⊆ 𝐺 } = { ℎ ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) ∣ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) ⊆ 𝐺 }
13	1 2 3 12	opnvonmbllem2	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )