Theorem vonvol

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	vonvol.a	|- ( ph -> A e. V )
	vonvol.b	|- ( ph -> B e. dom vol )
Assertion	vonvol	|- ( ph -> ( ( voln ` { A } ) ` ( B ^m { A } ) ) = ( vol ` B ) )

Proof

Step	Hyp	Ref	Expression
1		vonvol.a	|- ( ph -> A e. V )
2		vonvol.b	|- ( ph -> B e. dom vol )
3		mblss	|- ( B e. dom vol -> B C_ RR )
4	2 3	syl	|- ( ph -> B C_ RR )
5	1 4	ovnovol	|- ( ph -> ( ( voln* ` { A } ) ` ( B ^m { A } ) ) = ( vol* ` B ) )
6		snfi	|- { A } e. Fin
7	6	a1i	|- ( ph -> { A } e. Fin )
8	1 4	vonvolmbl	|- ( ph -> ( ( B ^m { A } ) e. dom ( voln ` { A } ) <-> B e. dom vol ) )
9	2 8	mpbird	|- ( ph -> ( B ^m { A } ) e. dom ( voln ` { A } ) )
10	7 9	mblvon	|- ( ph -> ( ( voln ` { A } ) ` ( B ^m { A } ) ) = ( ( voln* ` { A } ) ` ( B ^m { A } ) ) )
11		mblvol	|- ( B e. dom vol -> ( vol ` B ) = ( vol* ` B ) )
12	2 11	syl	|- ( ph -> ( vol ` B ) = ( vol* ` B ) )
13	5 10 12	3eqtr4d	|- ( ph -> ( ( voln ` { A } ) ` ( B ^m { A } ) ) = ( vol ` B ) )