Definition df-vol

Description: Define the Lebesgue measure, which is just the outer measure with a peculiar domain of definition. The property of being Lebesgue-measurable can be expressed as A e. dom vol . (Contributed by Mario Carneiro, 17-Mar-2014)

	Ref	Expression
Assertion	df-vol	$$⊢vol={{vol}^{*}\upharpoonright }_{\left\{x|\forall y\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)\right\}}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvol	$$classvol$$
1		covol	$$class{vol}^{*}$$
2		vx	$$setvarx$$
3		vy	$$setvary$$
4	1	ccnv	$$class{{vol}^{*}}^{-1}$$
5		cr	$$classℝ$$
6	4 5	cima	$$class{{vol}^{*}}^{-1}\left[ℝ\right]$$
7	3	cv	$$setvary$$
8	7 1	cfv	$$class{vol}^{*}\left(y\right)$$
9	2	cv	$$setvarx$$
10	7 9	cin	$$class\left(y\cap x\right)$$
11	10 1	cfv	$$class{vol}^{*}\left(y\cap x\right)$$
12		caddc	$$class+$$
13	7 9	cdif	$$class\left(y\setminus x\right)$$
14	13 1	cfv	$$class{vol}^{*}\left(y\setminus x\right)$$
15	11 14 12	co	$$class\left({vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)\right)$$
16	8 15	wceq	$$wff{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)$$
17	16 3 6	wral	$$wff\forall y\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)$$
18	17 2	cab	$$class\left\{x|\forall y\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)\right\}$$
19	1 18	cres	$$class\left({{vol}^{*}\upharpoonright }_{\left\{x|\forall y\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)\right\}}\right)$$
20	0 19	wceq	$$wffvol={{vol}^{*}\upharpoonright }_{\left\{x|\forall y\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)\right\}}$$