Definition df-carsg 35004

Description: Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval 35005 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 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +e (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})

Distinct variable group:   𝑚,𝑎,𝑒

Detailed syntax breakdown of Definition df-carsg

Step	Hyp	Ref	Expression
1		ccarsg 35003	. 2 class toCaraSiga
2		vm	. . 3 setvar 𝑚
3		cvv 3454	. . 3 class V
4		ve	. . . . . . . . . 10 setvar 𝑒
5	4	cv 1569	. . . . . . . . 9 class 𝑒
6		va	. . . . . . . . . 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 6558	. . . . . . 7 class (𝑚‘(𝑒 ∩ 𝑎))
11	5, 7	cdif 4048	. . . . . . . 8 class (𝑒 ∖ 𝑎)
12	11, 9	cfv 6558	. . . . . . 7 class (𝑚‘(𝑒 ∖ 𝑎))
13		cxad 13266	. . . . . . 7 class +e
14	10, 12, 13	co 7443	. . . . . 6 class ((𝑚‘(𝑒 ∩ 𝑎)) +e (𝑚‘(𝑒 ∖ 𝑎)))
15	5, 9	cfv 6558	. . . . . 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 (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +e (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})
23	1, 22	wceq 1570	1 wff toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +e (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})

This definition is used by:  carsgval  35005