Description: A subset X of the space of 1-dimensional Real numbers is Lebesgue measurable if and only if its projection Y on the Real numbers is Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | vonvolmbl2.f | |
|
vonvolmbl2.a | |
||
vonvolmbl2.x | |
||
vonvolmbl2.y | |
||
Assertion | vonvolmbl2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vonvolmbl2.f | |
|
2 | vonvolmbl2.a | |
|
3 | vonvolmbl2.x | |
|
4 | vonvolmbl2.y | |
|
5 | 1 2 3 4 | ssmapsn | |
6 | 5 | eleq1d | |
7 | 3 | adantr | |
8 | simpr | |
|
9 | 7 8 | sseldd | |
10 | elmapi | |
|
11 | frn | |
|
12 | 9 10 11 | 3syl | |
13 | 12 | ralrimiva | |
14 | iunss | |
|
15 | 13 14 | sylibr | |
16 | 4 15 | eqsstrid | |
17 | 2 16 | vonvolmbl | |
18 | 6 17 | bitrd | |