Metamath Proof Explorer


Theorem vonvolmbl2

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 _fY
vonvolmbl2.a φAV
vonvolmbl2.x φXA
vonvolmbl2.y Y=fXranf
Assertion vonvolmbl2 φXdomvolnAYdomvol

Proof

Step Hyp Ref Expression
1 vonvolmbl2.f _fY
2 vonvolmbl2.a φAV
3 vonvolmbl2.x φXA
4 vonvolmbl2.y Y=fXranf
5 1 2 3 4 ssmapsn φX=YA
6 5 eleq1d φXdomvolnAYAdomvolnA
7 3 adantr φfXXA
8 simpr φfXfX
9 7 8 sseldd φfXfA
10 elmapi fAf:A
11 frn f:Aranf
12 9 10 11 3syl φfXranf
13 12 ralrimiva φfXranf
14 iunss fXranffXranf
15 13 14 sylibr φfXranf
16 4 15 eqsstrid φY
17 2 16 vonvolmbl φYAdomvolnAYdomvol
18 6 17 bitrd φXdomvolnAYdomvol