Definition df-carsg 30364

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

Assertion

Ref	Expression
df-carsg	|- toCaraSiga = ( m e. _V |-> { a e. ~P U. dom m | A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) } )

Distinct variable group:   m, a, e

Detailed syntax breakdown of Definition df-carsg

Step	Hyp	Ref	Expression
1		ccarsg 30363	. 2 class toCaraSiga
2		vm	. . 3 setvar m
3		cvv 3200	. . 3 class _V
4		ve	. . . . . . . . . 10 setvar e
5	4	cv 1482	. . . . . . . . 9 class e
6		va	. . . . . . . . . 10 setvar a
7	6	cv 1482	. . . . . . . . 9 class a
8	5, 7	cin 3573	. . . . . . . 8 class ( e i^i a )
9	2	cv 1482	. . . . . . . 8 class m
10	8, 9	cfv 5888	. . . . . . 7 class ( m ` ( e i^i a ) )
11	5, 7	cdif 3571	. . . . . . . 8 class ( e \ a )
12	11, 9	cfv 5888	. . . . . . 7 class ( m ` ( e \ a ) )
13		cxad 11944	. . . . . . 7 class +e
14	10, 12, 13	co 6650	. . . . . 6 class ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) )
15	5, 9	cfv 5888	. . . . . 6 class ( m ` e )
16	14, 15	wceq 1483	. . . . 5 wff ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e )
17	9	cdm 5114	. . . . . . 7 class dom m
18	17	cuni 4436	. . . . . 6 class U. dom m
19	18	cpw 4158	. . . . 5 class ~P U. dom m
20	16, 4, 19	wral 2912	. . . 4 wff A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e )
21	20, 6, 19	crab 2916	. . 3 class { a e. ~P U. dom m | A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) }
22	2, 3, 21	cmpt 4729	. 2 class ( m e. _V |-> { a e. ~P U. dom m | A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) } )
23	1, 22	wceq 1483	1 wff toCaraSiga = ( m e. _V |-> { a e. ~P U. dom m | A. e e. ~P U. dom m ( ( m ` ( e i^i a ) ) +e ( m ` ( e \ a ) ) ) = ( m ` e ) } )

This definition is referenced by:  carsgval  30365