Theorem vonval

Description: Value of the Lebesgue measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypothesis	vonval.1	$$⊢\phi \to X\in \mathrm{Fin}$$
Assertion	vonval	$$⊢\phi \to \mathrm{voln}\left(X\right)={\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}$$

Proof

Step	Hyp	Ref	Expression
1		vonval.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2		df-voln	$$⊢\mathrm{voln}=\left(x\in \mathrm{Fin}⟼{\mathrm{voln*}\left(x\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(x\right)\right)}\right)$$
3		fveq2	$$⊢x=X\to \mathrm{voln*}\left(x\right)=\mathrm{voln*}\left(X\right)$$
4		2fveq3	$$⊢x=X\to \mathrm{CaraGen}\left(\mathrm{voln*}\left(x\right)\right)=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
5	3 4	reseq12d	$$⊢x=X\to {\mathrm{voln*}\left(x\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(x\right)\right)}={\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}$$
6		fvex	$$⊢\mathrm{voln*}\left(X\right)\in \mathrm{V}$$
7	6	resex	$$⊢{\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}\in \mathrm{V}$$
8	7	a1i	$$⊢\phi \to {\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}\in \mathrm{V}$$
9	2 5 1 8	fvmptd3	$$⊢\phi \to \mathrm{voln}\left(X\right)={\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}$$