Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-carsg Structured version   Visualization version   GIF version

Definition df-carsg 30492
 Description: Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval 30493 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
StepHypRef Expression
1 ccarsg 30491 . 2 class toCaraSiga
2 vm . . 3 setvar 𝑚
3 cvv 3231 . . 3 class V
4 ve . . . . . . . . . 10 setvar 𝑒
54cv 1522 . . . . . . . . 9 class 𝑒
6 va . . . . . . . . . 10 setvar 𝑎
76cv 1522 . . . . . . . . 9 class 𝑎
85, 7cin 3606 . . . . . . . 8 class (𝑒𝑎)
92cv 1522 . . . . . . . 8 class 𝑚
108, 9cfv 5926 . . . . . . 7 class (𝑚‘(𝑒𝑎))
115, 7cdif 3604 . . . . . . . 8 class (𝑒𝑎)
1211, 9cfv 5926 . . . . . . 7 class (𝑚‘(𝑒𝑎))
13 cxad 11982 . . . . . . 7 class +𝑒
1410, 12, 13co 6690 . . . . . 6 class ((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎)))
155, 9cfv 5926 . . . . . 6 class (𝑚𝑒)
1614, 15wceq 1523 . . . . 5 wff ((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)
179cdm 5143 . . . . . . 7 class dom 𝑚
1817cuni 4468 . . . . . 6 class dom 𝑚
1918cpw 4191 . . . . 5 class 𝒫 dom 𝑚
2016, 4, 19wral 2941 . . . 4 wff 𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)
2120, 6, 19crab 2945 . . 3 class {𝑎 ∈ 𝒫 dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)}
222, 3, 21cmpt 4762 . 2 class (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)})
231, 22wceq 1523 1 wff toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 dom 𝑚((𝑚‘(𝑒𝑎)) +𝑒 (𝑚‘(𝑒𝑎))) = (𝑚𝑒)})
 Colors of variables: wff setvar class This definition is referenced by:  carsgval  30493
 Copyright terms: Public domain W3C validator