Metamath Proof Explorer

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 = m ∈ V ⟼ a ∈ 𝒫 ⋃ dom ⁡ m | ∀ e ∈ 𝒫 ⋃ dom ⁡ m m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccarsg class toCaraSiga
1 vm setvar m
2 cvv class V
3 va setvar a
4 1 cv setvar m
5 4 cdm class dom ⁡ m
6 5 cuni class ⋃ dom ⁡ m
7 6 cpw class 𝒫 ⋃ dom ⁡ m
8 ve setvar e
9 8 cv setvar e
10 3 cv setvar a
11 9 10 cin class e ∩ a
12 11 4 cfv class m ⁡ e ∩ a
13 cxad class + 𝑒
14 9 10 cdif class e ∖ a
15 14 4 cfv class m ⁡ e ∖ a
16 12 15 13 co class m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a
17 9 4 cfv class m ⁡ e
18 16 17 wceq wff m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e
19 18 8 7 wral wff ∀ e ∈ 𝒫 ⋃ dom ⁡ m m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e
20 19 3 7 crab class a ∈ 𝒫 ⋃ dom ⁡ m | ∀ e ∈ 𝒫 ⋃ dom ⁡ m m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e
21 1 2 20 cmpt class m ∈ V ⟼ a ∈ 𝒫 ⋃ dom ⁡ m | ∀ e ∈ 𝒫 ⋃ dom ⁡ m m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e
22 0 21 wceq wff toCaraSiga = m ∈ V ⟼ a ∈ 𝒫 ⋃ dom ⁡ m | ∀ e ∈ 𝒫 ⋃ dom ⁡ m m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e