Definition df-caragen 47705

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 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +e (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)})

Distinct variable group:   𝑒,𝑎,𝑜

Detailed syntax breakdown of Definition df-caragen

Step	Hyp	Ref	Expression
1		ccaragen 47704	. 2 class CaraGen
2		vo	. . 3 setvar 𝑜
3		come 47702	. . 3 class OutMeas
4		va	. . . . . . . . . 10 setvar 𝑎
5	4	cv 1569	. . . . . . . . 9 class 𝑎
6		ve	. . . . . . . . . 10 setvar 𝑒
7	6	cv 1569	. . . . . . . . 9 class 𝑒
8	5, 7	cin 4092	. . . . . . . 8 class (𝑎 ∩ 𝑒)
9	2	cv 1569	. . . . . . . 8 class 𝑜
10	8, 9	cfv 6555	. . . . . . 7 class (𝑜‘(𝑎 ∩ 𝑒))
11	5, 7	cdif 4048	. . . . . . . 8 class (𝑎 ∖ 𝑒)
12	11, 9	cfv 6555	. . . . . . 7 class (𝑜‘(𝑎 ∖ 𝑒))
13		cxad 13263	. . . . . . 7 class +e
14	10, 12, 13	co 7440	. . . . . 6 class ((𝑜‘(𝑎 ∩ 𝑒)) +e (𝑜‘(𝑎 ∖ 𝑒)))
15	5, 9	cfv 6555	. . . . . 6 class (𝑜‘𝑎)
16	14, 15	wceq 1570	. . . . 5 wff ((𝑜‘(𝑎 ∩ 𝑒)) +e (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)
17	9	cdm 5655	. . . . . . 7 class dom 𝑜
18	17	cuni 4870	. . . . . 6 class ∪ dom 𝑜
19	18	cpw 4560	. . . . 5 class 𝒫 ∪ dom 𝑜
20	16, 4, 19	wral 3080	. . . 4 wff ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +e (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)
21	20, 6, 19	crab 3416	. . 3 class {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +e (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)}
22	2, 3, 21	cmpt 5189	. 2 class (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +e (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)})
23	1, 22	wceq 1570	1 wff CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +e (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)})

This definition is used by:  caragenval  47706