Definition df-caragen 43131

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 43130	. 2 class CaraGen
2		vo	. . 3 setvar 𝑜
3		come 43128	. . 3 class OutMeas
4		va	. . . . . . . . . 10 setvar 𝑎
5	4	cv 1537	. . . . . . . . 9 class 𝑎
6		ve	. . . . . . . . . 10 setvar 𝑒
7	6	cv 1537	. . . . . . . . 9 class 𝑒
8	5, 7	cin 3880	. . . . . . . 8 class (𝑎 ∩ 𝑒)
9	2	cv 1537	. . . . . . . 8 class 𝑜
10	8, 9	cfv 6324	. . . . . . 7 class (𝑜‘(𝑎 ∩ 𝑒))
11	5, 7	cdif 3878	. . . . . . . 8 class (𝑎 ∖ 𝑒)
12	11, 9	cfv 6324	. . . . . . 7 class (𝑜‘(𝑎 ∖ 𝑒))
13		cxad 12493	. . . . . . 7 class +𝑒
14	10, 12, 13	co 7135	. . . . . 6 class ((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒)))
15	5, 9	cfv 6324	. . . . . 6 class (𝑜‘𝑎)
16	14, 15	wceq 1538	. . . . 5 wff ((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)
17	9	cdm 5519	. . . . . . 7 class dom 𝑜
18	17	cuni 4800	. . . . . 6 class ∪ dom 𝑜
19	18	cpw 4497	. . . . 5 class 𝒫 ∪ dom 𝑜
20	16, 4, 19	wral 3106	. . . 4 wff ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)
21	20, 6, 19	crab 3110	. . 3 class {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)}
22	2, 3, 21	cmpt 5110	. 2 class (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)})
23	1, 22	wceq 1538	1 wff CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)})

This definition is referenced by:  caragenval  43132