Theorem vonvol2

Description: The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	vonvol2.f	|- F/_ f Y
	vonvol2.a	|- ( ph -> A e. V )
	vonvol2.x	|- ( ph -> X e. dom ( voln ` { A } ) )
	vonvol2.y	|- Y = U_ f e. X ran f
Assertion	vonvol2	|- ( ph -> ( ( voln ` { A } ) ` X ) = ( vol ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		vonvol2.f	|- F/_ f Y
2		vonvol2.a	|- ( ph -> A e. V )
3		vonvol2.x	|- ( ph -> X e. dom ( voln ` { A } ) )
4		vonvol2.y	|- Y = U_ f e. X ran f
5		snfi	|- { A } e. Fin
6	5	a1i	|- ( ph -> { A } e. Fin )
7	6 3	vonmblss2	|- ( ph -> X C_ ( RR ^m { A } ) )
8	1 2 7 4	ssmapsn	|- ( ph -> X = ( Y ^m { A } ) )
9	8	eqcomd	|- ( ph -> ( Y ^m { A } ) = X )
10	9 3	eqeltrd	|- ( ph -> ( Y ^m { A } ) e. dom ( voln ` { A } ) )
11	7	adantr	|- ( ( ph /\ f e. X ) -> X C_ ( RR ^m { A } ) )
12		simpr	|- ( ( ph /\ f e. X ) -> f e. X )
13	11 12	sseldd	|- ( ( ph /\ f e. X ) -> f e. ( RR ^m { A } ) )
14		elmapi	|- ( f e. ( RR ^m { A } ) -> f : { A } --> RR )
15		frn	|- ( f : { A } --> RR -> ran f C_ RR )
16	13 14 15	3syl	|- ( ( ph /\ f e. X ) -> ran f C_ RR )
17	16	ralrimiva	|- ( ph -> A. f e. X ran f C_ RR )
18		iunss	|- ( U_ f e. X ran f C_ RR <-> A. f e. X ran f C_ RR )
19	17 18	sylibr	|- ( ph -> U_ f e. X ran f C_ RR )
20	4 19	eqsstrid	|- ( ph -> Y C_ RR )
21	2 20	vonvolmbl	|- ( ph -> ( ( Y ^m { A } ) e. dom ( voln ` { A } ) <-> Y e. dom vol ) )
22	10 21	mpbid	|- ( ph -> Y e. dom vol )
23	2 22	vonvol	|- ( ph -> ( ( voln ` { A } ) ` ( Y ^m { A } ) ) = ( vol ` Y ) )
24	9	eqcomd	|- ( ph -> X = ( Y ^m { A } ) )
25	24	fveq2d	|- ( ph -> ( ( voln ` { A } ) ` X ) = ( ( voln ` { A } ) ` ( Y ^m { A } ) ) )
26		eqidd	|- ( ph -> ( vol ` Y ) = ( vol ` Y ) )
27	23 25 26	3eqtr4d	|- ( ph -> ( ( voln ` { A } ) ` X ) = ( vol ` Y ) )