Theorem ioovonmbl

Description: Any n-dimensional open interval is Lebesgue measurable. This is the first statement in Proposition 115G (c) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	ioovonmbl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ioovonmbl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
	ioovonmbl.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ* )
	ioovonmbl.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ* )
Assertion	ioovonmbl	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ioovonmbl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ioovonmbl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
3		ioovonmbl.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ* )
4		ioovonmbl.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ* )
5	1 3 4	ioorrnopnxr	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
6	1 2 5	opnvonmbl	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )