Metamath Proof Explorer


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 φXFin
opnvonmbl.s S=domvolnX
opnvonmbl.g φGTopOpenmsup
Assertion opnvonmbl φGS

Proof

Step Hyp Ref Expression
1 opnvonmbl.x φXFin
2 opnvonmbl.s S=domvolnX
3 opnvonmbl.g φGTopOpenmsup
4 fveq2 k=i.fk=.fi
5 4 cbvixpv kX.fk=iX.fi
6 5 a1i f=hkX.fk=iX.fi
7 coeq2 f=h.f=.h
8 7 fveq1d f=h.fi=.hi
9 8 ixpeq2dv f=hiX.fi=iX.hi
10 6 9 eqtrd f=hkX.fk=iX.hi
11 10 sseq1d f=hkX.fkGiX.hiG
12 11 cbvrabv f×X|kX.fkG=h×X|iX.hiG
13 1 2 3 12 opnvonmbllem2 φGS