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	$$⊢\phi \to A\in V$$
	vonvol.b	$$⊢\phi \to B\in \mathrm{dom}vol$$
Assertion	vonvol	$$⊢\phi \to \mathrm{voln}\left(\left\{A\right\}\right)\left(B^{\left\{A\right\}}\right)=vol\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		vonvol.a	$$⊢\phi \to A\in V$$
2		vonvol.b	$$⊢\phi \to B\in \mathrm{dom}vol$$
3		mblss	$$⊢B\in \mathrm{dom}vol\to B\subseteq ℝ$$
4	2 3	syl	$$⊢\phi \to B\subseteq ℝ$$
5	1 4	ovnovol	$$⊢\phi \to \mathrm{voln*}\left(\left\{A\right\}\right)\left(B^{\left\{A\right\}}\right)={vol}^{*}\left(B\right)$$
6		snfi	$$⊢\left\{A\right\}\in \mathrm{Fin}$$
7	6	a1i	$$⊢\phi \to \left\{A\right\}\in \mathrm{Fin}$$
8	1 4	vonvolmbl	$$⊢\phi \to \left(B^{\left\{A\right\}}\in \mathrm{dom}\mathrm{voln}\left(\left\{A\right\}\right)\leftrightarrow B\in \mathrm{dom}vol\right)$$
9	2 8	mpbird	$$⊢\phi \to B^{\left\{A\right\}}\in \mathrm{dom}\mathrm{voln}\left(\left\{A\right\}\right)$$
10	7 9	mblvon	$$⊢\phi \to \mathrm{voln}\left(\left\{A\right\}\right)\left(B^{\left\{A\right\}}\right)=\mathrm{voln*}\left(\left\{A\right\}\right)\left(B^{\left\{A\right\}}\right)$$
11		mblvol	$$⊢B\in \mathrm{dom}vol\to vol\left(B\right)={vol}^{*}\left(B\right)$$
12	2 11	syl	$$⊢\phi \to vol\left(B\right)={vol}^{*}\left(B\right)$$
13	5 10 12	3eqtr4d	$$⊢\phi \to \mathrm{voln}\left(\left\{A\right\}\right)\left(B^{\left\{A\right\}}\right)=vol\left(B\right)$$