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 φXFin
ioovonmbl.s S=domvolnX
ioovonmbl.a φA:X*
ioovonmbl.b φB:X*
Assertion ioovonmbl φiXAiBiS

Proof

Step Hyp Ref Expression
1 ioovonmbl.x φXFin
2 ioovonmbl.s S=domvolnX
3 ioovonmbl.a φA:X*
4 ioovonmbl.b φB:X*
5 1 3 4 ioorrnopnxr φiXAiBiTopOpenmsup
6 1 2 5 opnvonmbl φiXAiBiS