Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-caragen Structured version   Visualization version   GIF version

Definition df-caragen 39382
 Description: Define the sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Assertion
Ref Expression
df-caragen CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)})
Distinct variable group:   𝑒,𝑎,𝑜

Detailed syntax breakdown of Definition df-caragen
StepHypRef Expression
1 ccaragen 39381 . 2 class CaraGen
2 vo . . 3 setvar 𝑜
3 come 39379 . . 3 class OutMeas
4 va . . . . . . . . . 10 setvar 𝑎
54cv 1474 . . . . . . . . 9 class 𝑎
6 ve . . . . . . . . . 10 setvar 𝑒
76cv 1474 . . . . . . . . 9 class 𝑒
85, 7cin 3539 . . . . . . . 8 class (𝑎𝑒)
92cv 1474 . . . . . . . 8 class 𝑜
108, 9cfv 5804 . . . . . . 7 class (𝑜‘(𝑎𝑒))
115, 7cdif 3537 . . . . . . . 8 class (𝑎𝑒)
1211, 9cfv 5804 . . . . . . 7 class (𝑜‘(𝑎𝑒))
13 cxad 11820 . . . . . . 7 class +𝑒
1410, 12, 13co 6549 . . . . . 6 class ((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒)))
155, 9cfv 5804 . . . . . 6 class (𝑜𝑎)
1614, 15wceq 1475 . . . . 5 wff ((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)
179cdm 5038 . . . . . . 7 class dom 𝑜
1817cuni 4372 . . . . . 6 class dom 𝑜
1918cpw 4108 . . . . 5 class 𝒫 dom 𝑜
2016, 4, 19wral 2896 . . . 4 wff 𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)
2120, 6, 19crab 2900 . . 3 class {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)}
222, 3, 21cmpt 4643 . 2 class (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)})
231, 22wceq 1475 1 wff CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)})
 Colors of variables: wff setvar class This definition is referenced by:  caragenval  39383
 Copyright terms: Public domain W3C validator