Definition df-carsg 34304

Description: Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval 34305 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 34303	. 2 class toCaraSiga
2		vm	. . 3 setvar 𝑚
3		cvv 3480	. . 3 class V
4		ve	. . . . . . . . . 10 setvar 𝑒
5	4	cv 1539	. . . . . . . . 9 class 𝑒
6		va	. . . . . . . . . 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 (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})
23	1, 22	wceq 1540	1 wff toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})

This definition is referenced by:  carsgval  34305