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 | |
|
ovolval5.m | |
||
Assertion | ovolval5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovolval5.a | |
|
2 | ovolval5.m | |
|
3 | eqeq1 | |
|
4 | 3 | anbi2d | |
5 | 4 | rexbidv | |
6 | coeq2 | |
|
7 | 6 | rneqd | |
8 | 7 | unieqd | |
9 | 8 | sseq2d | |
10 | coeq2 | |
|
11 | 10 | fveq2d | |
12 | 11 | eqeq2d | |
13 | 9 12 | anbi12d | |
14 | 13 | cbvrexvw | |
15 | 14 | a1i | |
16 | 5 15 | bitrd | |
17 | 16 | cbvrabv | |
18 | 1 17 | ovolval4 | |
19 | 11 | eqeq2d | |
20 | 9 19 | anbi12d | |
21 | 20 | cbvrexvw | |
22 | 21 | a1i | |
23 | eqeq1 | |
|
24 | 23 | anbi2d | |
25 | 24 | rexbidv | |
26 | 22 25 | bitrd | |
27 | 26 | cbvrabv | |
28 | 2 27 | ovolval5lem3 | |
29 | 28 | a1i | |
30 | 18 29 | eqtrd | |