Definition df-caragen 46507

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

Assertion

Ref	Expression
df-caragen	⊢ CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)})

Distinct variable group:   𝑒,𝑎,𝑜

Detailed syntax breakdown of Definition df-caragen

Step	Hyp	Ref	Expression
1		ccaragen 46506	. 2 class CaraGen
2		vo	. . 3 setvar 𝑜
3		come 46504	. . 3 class OutMeas
4		va	. . . . . . . . . 10 setvar 𝑎
5	4	cv 1539	. . . . . . . . 9 class 𝑎
6		ve	. . . . . . . . . 10 setvar 𝑒
7	6	cv 1539	. . . . . . . . 9 class 𝑒
8	5, 7	cin 3950	. . . . . . . 8 class (𝑎 ∩ 𝑒)
9	2	cv 1539	. . . . . . . 8 class 𝑜
10	8, 9	cfv 6561	. . . . . . 7 class (𝑜‘(𝑎 ∩ 𝑒))
11	5, 7	cdif 3948	. . . . . . . 8 class (𝑎 ∖ 𝑒)
12	11, 9	cfv 6561	. . . . . . 7 class (𝑜‘(𝑎 ∖ 𝑒))
13		cxad 13152	. . . . . . 7 class +𝑒
14	10, 12, 13	co 7431	. . . . . 6 class ((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒)))
15	5, 9	cfv 6561	. . . . . 6 class (𝑜‘𝑎)
16	14, 15	wceq 1540	. . . . 5 wff ((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)
17	9	cdm 5685	. . . . . . 7 class dom 𝑜
18	17	cuni 4907	. . . . . 6 class ∪ dom 𝑜
19	18	cpw 4600	. . . . 5 class 𝒫 ∪ dom 𝑜
20	16, 4, 19	wral 3061	. . . 4 wff ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)
21	20, 6, 19	crab 3436	. . 3 class {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)}
22	2, 3, 21	cmpt 5225	. 2 class (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)})
23	1, 22	wceq 1540	1 wff CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)})

This definition is referenced by:  caragenval  46508