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	|- F/_ f Y
	vonvolmbl2.a	|- ( ph -> A e. V )
	vonvolmbl2.x	|- ( ph -> X C_ ( RR ^m { A } ) )
	vonvolmbl2.y	|- Y = U_ f e. X ran f
Assertion	vonvolmbl2	|- ( ph -> ( X e. dom ( voln ` { A } ) <-> Y e. dom vol ) )

Proof

Step	Hyp	Ref	Expression
1		vonvolmbl2.f	|- F/_ f Y
2		vonvolmbl2.a	|- ( ph -> A e. V )
3		vonvolmbl2.x	|- ( ph -> X C_ ( RR ^m { A } ) )
4		vonvolmbl2.y	|- Y = U_ f e. X ran f
5	1 2 3 4	ssmapsn	|- ( ph -> X = ( Y ^m { A } ) )
6	5	eleq1d	|- ( ph -> ( X e. dom ( voln ` { A } ) <-> ( Y ^m { A } ) e. dom ( voln ` { A } ) ) )
7	3	adantr	|- ( ( ph /\ f e. X ) -> X C_ ( RR ^m { A } ) )
8		simpr	|- ( ( ph /\ f e. X ) -> f e. X )
9	7 8	sseldd	|- ( ( ph /\ f e. X ) -> f e. ( RR ^m { A } ) )
10		elmapi	|- ( f e. ( RR ^m { A } ) -> f : { A } --> RR )
11		frn	|- ( f : { A } --> RR -> ran f C_ RR )
12	9 10 11	3syl	|- ( ( ph /\ f e. X ) -> ran f C_ RR )
13	12	ralrimiva	|- ( ph -> A. f e. X ran f C_ RR )
14		iunss	|- ( U_ f e. X ran f C_ RR <-> A. f e. X ran f C_ RR )
15	13 14	sylibr	|- ( ph -> U_ f e. X ran f C_ RR )
16	4 15	eqsstrid	|- ( ph -> Y C_ RR )
17	2 16	vonvolmbl	|- ( ph -> ( ( Y ^m { A } ) e. dom ( voln ` { A } ) <-> Y e. dom vol ) )
18	6 17	bitrd	|- ( ph -> ( X e. dom ( voln ` { A } ) <-> Y e. dom vol ) )