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}^{} ↾}_{\{x \| \forall y \in {vol}^{}^{-1} [ℝ] {vol}^{} (y) = {vol}^{} (y \cap x) + {vol}^{*} (y ∖ x)\}}$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-vol

Detailed syntax breakdown