Definition df-carsg 31560

Description: Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval 31561 for its value. Definition 1.11.2 of [Bogachev] p. 41. (Contributed by Thierry Arnoux, 17-May-2020.)

Assertion

Ref	Expression
df-carsg	⊢ toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})

Distinct variable group:   𝑚,𝑎,𝑒

Detailed syntax breakdown of Definition df-carsg

Step	Hyp	Ref	Expression
1		ccarsg 31559	. 2 class toCaraSiga
2		vm	. . 3 setvar 𝑚
3		cvv 3494	. . 3 class V
4		ve	. . . . . . . . . 10 setvar 𝑒
5	4	cv 1536	. . . . . . . . 9 class 𝑒
6		va	. . . . . . . . . 10 setvar 𝑎
7	6	cv 1536	. . . . . . . . 9 class 𝑎
8	5, 7	cin 3935	. . . . . . . 8 class (𝑒 ∩ 𝑎)
9	2	cv 1536	. . . . . . . 8 class 𝑚
10	8, 9	cfv 6355	. . . . . . 7 class (𝑚‘(𝑒 ∩ 𝑎))
11	5, 7	cdif 3933	. . . . . . . 8 class (𝑒 ∖ 𝑎)
12	11, 9	cfv 6355	. . . . . . 7 class (𝑚‘(𝑒 ∖ 𝑎))
13		cxad 12506	. . . . . . 7 class +𝑒
14	10, 12, 13	co 7156	. . . . . 6 class ((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎)))
15	5, 9	cfv 6355	. . . . . 6 class (𝑚‘𝑒)
16	14, 15	wceq 1537	. . . . 5 wff ((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)
17	9	cdm 5555	. . . . . . 7 class dom 𝑚
18	17	cuni 4838	. . . . . 6 class ∪ dom 𝑚
19	18	cpw 4539	. . . . 5 class 𝒫 ∪ dom 𝑚
20	16, 4, 19	wral 3138	. . . 4 wff ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)
21	20, 6, 19	crab 3142	. . 3 class {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)}
22	2, 3, 21	cmpt 5146	. 2 class (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})
23	1, 22	wceq 1537	1 wff toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})

This definition is referenced by:  carsgval  31561