Metamath Proof Explorer


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 𝑖𝑋 ( ( 𝐴𝑖 ) (,) ( 𝐵𝑖 ) ) ∈ 𝑆 )