df-caragen

Description: Define the sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	df-caragen	$⊢ CaraGen = (o \in OutMeas ⟼ \{e \in 𝒫 ⋃ dom o \| \forall a \in 𝒫 ⋃ dom o o (a \cap e) +_{𝑒} o (a ∖ e) = o (a)\})$

Step	Hyp	Ref	Expression
0		ccaragen	$class CaraGen$
1		vo	$setvar o$
2		come	$class OutMeas$
3		ve	$setvar e$
4	1	cv	$setvar o$
5	4	cdm	$class dom o$
6	5	cuni	$class ⋃ dom o$
7	6	cpw	$class 𝒫 ⋃ dom o$
8		va	$setvar a$
9	8	cv	$setvar a$
10	3	cv	$setvar e$
11	9 10	cin	$class (a \cap e)$
12	11 4	cfv	$class o (a \cap e)$
13		cxad	$class +_{𝑒}$
14	9 10	cdif	$class (a ∖ e)$
15	14 4	cfv	$class o (a ∖ e)$
16	12 15 13	co	$class (o (a \cap e) +_{𝑒} o (a ∖ e))$
17	9 4	cfv	$class o (a)$
18	16 17	wceq	$wff o (a \cap e) +_{𝑒} o (a ∖ e) = o (a)$
19	18 8 7	wral	$wff \forall a \in 𝒫 ⋃ dom o o (a \cap e) +_{𝑒} o (a ∖ e) = o (a)$
20	19 3 7	crab	$class \{e \in 𝒫 ⋃ dom o \| \forall a \in 𝒫 ⋃ dom o o (a \cap e) +_{𝑒} o (a ∖ e) = o (a)\}$
21	1 2 20	cmpt	$class (o \in OutMeas ⟼ \{e \in 𝒫 ⋃ dom o \| \forall a \in 𝒫 ⋃ dom o o (a \cap e) +_{𝑒} o (a ∖ e) = o (a)\})$
22	0 21	wceq	$wff CaraGen = (o \in OutMeas ⟼ \{e \in 𝒫 ⋃ dom o \| \forall a \in 𝒫 ⋃ dom o o (a \cap e) +_{𝑒} o (a ∖ e) = o (a)\})$

Metamath Proof Explorer