Definition df-carsg 31670

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

This definition is referenced by:  carsgval  31671