Definition df-voln

Description: Define the Lebesgue measure for the space of multidimensional real numbers. The cardinality of x is the dimension of the space modeled. Definition 115C of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvoln	$$class\mathrm{voln}$$
1		vx	$$setvarx$$
2		cfn	$$class\mathrm{Fin}$$
3		covoln	$$class\mathrm{voln*}$$
4	1	cv	$$setvarx$$
5	4 3	cfv	$$class\mathrm{voln*}\left(x\right)$$
6		ccaragen	$$class\mathrm{CaraGen}$$
7	5 6	cfv	$$class\mathrm{CaraGen}\left(\mathrm{voln*}\left(x\right)\right)$$
8	5 7	cres	$$class\left({\mathrm{voln*}\left(x\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(x\right)\right)}\right)$$
9	1 2 8	cmpt	$$class\left(x\in \mathrm{Fin}⟼{\mathrm{voln*}\left(x\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(x\right)\right)}\right)$$
10	0 9	wceq	$$wff\mathrm{voln}=\left(x\in \mathrm{Fin}⟼{\mathrm{voln*}\left(x\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(x\right)\right)}\right)$$