Metamath Proof Explorer


Theorem ovolval5

Description: The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval5.a φA
ovolval5.m M=y*|f2Aran.fy=sum^vol.f
Assertion ovolval5 φvol*A=supM*<

Proof

Step Hyp Ref Expression
1 ovolval5.a φA
2 ovolval5.m M=y*|f2Aran.fy=sum^vol.f
3 eqeq1 x=yx=sum^vol.gy=sum^vol.g
4 3 anbi2d x=yAran.gx=sum^vol.gAran.gy=sum^vol.g
5 4 rexbidv x=yg2Aran.gx=sum^vol.gg2Aran.gy=sum^vol.g
6 coeq2 g=f.g=.f
7 6 rneqd g=fran.g=ran.f
8 7 unieqd g=fran.g=ran.f
9 8 sseq2d g=fAran.gAran.f
10 coeq2 g=fvol.g=vol.f
11 10 fveq2d g=fsum^vol.g=sum^vol.f
12 11 eqeq2d g=fy=sum^vol.gy=sum^vol.f
13 9 12 anbi12d g=fAran.gy=sum^vol.gAran.fy=sum^vol.f
14 13 cbvrexvw g2Aran.gy=sum^vol.gf2Aran.fy=sum^vol.f
15 14 a1i x=yg2Aran.gy=sum^vol.gf2Aran.fy=sum^vol.f
16 5 15 bitrd x=yg2Aran.gx=sum^vol.gf2Aran.fy=sum^vol.f
17 16 cbvrabv x*|g2Aran.gx=sum^vol.g=y*|f2Aran.fy=sum^vol.f
18 1 17 ovolval4 φvol*A=supx*|g2Aran.gx=sum^vol.g*<
19 11 eqeq2d g=fx=sum^vol.gx=sum^vol.f
20 9 19 anbi12d g=fAran.gx=sum^vol.gAran.fx=sum^vol.f
21 20 cbvrexvw g2Aran.gx=sum^vol.gf2Aran.fx=sum^vol.f
22 21 a1i x=zg2Aran.gx=sum^vol.gf2Aran.fx=sum^vol.f
23 eqeq1 x=zx=sum^vol.fz=sum^vol.f
24 23 anbi2d x=zAran.fx=sum^vol.fAran.fz=sum^vol.f
25 24 rexbidv x=zf2Aran.fx=sum^vol.ff2Aran.fz=sum^vol.f
26 22 25 bitrd x=zg2Aran.gx=sum^vol.gf2Aran.fz=sum^vol.f
27 26 cbvrabv x*|g2Aran.gx=sum^vol.g=z*|f2Aran.fz=sum^vol.f
28 2 27 ovolval5lem3 supx*|g2Aran.gx=sum^vol.g*<=supM*<
29 28 a1i φsupx*|g2Aran.gx=sum^vol.g*<=supM*<
30 18 29 eqtrd φvol*A=supM*<