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 | |
|
opnvonmbl.s | |
||
opnvonmbl.g | |
||
Assertion | opnvonmbl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opnvonmbl.x | |
|
2 | opnvonmbl.s | |
|
3 | opnvonmbl.g | |
|
4 | fveq2 | |
|
5 | 4 | cbvixpv | |
6 | 5 | a1i | |
7 | coeq2 | |
|
8 | 7 | fveq1d | |
9 | 8 | ixpeq2dv | |
10 | 6 9 | eqtrd | |
11 | 10 | sseq1d | |
12 | 11 | cbvrabv | |
13 | 1 2 3 12 | opnvonmbllem2 | |