Definition df-carsg

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccarsg	⊢ toCaraSiga
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		va	⊢ 𝑎
4	1	cv	⊢ 𝑚
5	4	cdm	⊢ dom 𝑚
6	5	cuni	⊢ ∪ dom 𝑚
7	6	cpw	⊢ 𝒫 ∪ dom 𝑚
8		ve	⊢ 𝑒
9	8	cv	⊢ 𝑒
10	3	cv	⊢ 𝑎
11	9 10	cin	⊢ ( 𝑒 ∩ 𝑎 )
12	11 4	cfv	⊢ ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) )
13		cxad	⊢ +e
14	9 10	cdif	⊢ ( 𝑒 ∖ 𝑎 )
15	14 4	cfv	⊢ ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) )
16	12 15 13	co	⊢ ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +e ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) )
17	9 4	cfv	⊢ ( 𝑚 ‘ 𝑒 )
18	16 17	wceq	⊢ ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +e ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑚 ‘ 𝑒 )
19	18 8 7	wral	⊢ ∀ 𝑒 ∈ 𝒫 ∪ dom 𝑚 ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +e ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑚 ‘ 𝑒 )
20	19 3 7	crab	⊢ { 𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀ 𝑒 ∈ 𝒫 ∪ dom 𝑚 ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +e ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑚 ‘ 𝑒 ) }
21	1 2 20	cmpt	⊢ ( 𝑚 ∈ V ↦ { 𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀ 𝑒 ∈ 𝒫 ∪ dom 𝑚 ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +e ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑚 ‘ 𝑒 ) } )
22	0 21	wceq	⊢ toCaraSiga = ( 𝑚 ∈ V ↦ { 𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀ 𝑒 ∈ 𝒫 ∪ dom 𝑚 ( ( 𝑚 ‘ ( 𝑒 ∩ 𝑎 ) ) +e ( 𝑚 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑚 ‘ 𝑒 ) } )