Users' Mathboxes 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 45194
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 45193 . 2 class CaraGen
2 vo . . 3 setvar 𝑜
3 come 45191 . . 3 class OutMeas
4 va . . . . . . . . . 10 setvar 𝑎
54cv 1540 . . . . . . . . 9 class 𝑎
6 ve . . . . . . . . . 10 setvar 𝑒
76cv 1540 . . . . . . . . 9 class 𝑒
85, 7cin 3946 . . . . . . . 8 class (𝑎𝑒)
92cv 1540 . . . . . . . 8 class 𝑜
108, 9cfv 6540 . . . . . . 7 class (𝑜‘(𝑎𝑒))
115, 7cdif 3944 . . . . . . . 8 class (𝑎𝑒)
1211, 9cfv 6540 . . . . . . 7 class (𝑜‘(𝑎𝑒))
13 cxad 13086 . . . . . . 7 class +𝑒
1410, 12, 13co 7405 . . . . . 6 class ((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒)))
155, 9cfv 6540 . . . . . 6 class (𝑜𝑎)
1614, 15wceq 1541 . . . . 5 wff ((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)
179cdm 5675 . . . . . . 7 class dom 𝑜
1817cuni 4907 . . . . . 6 class dom 𝑜
1918cpw 4601 . . . . 5 class 𝒫 dom 𝑜
2016, 4, 19wral 3061 . . . 4 wff 𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)
2120, 6, 19crab 3432 . . 3 class {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)}
222, 3, 21cmpt 5230 . 2 class (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)})
231, 22wceq 1541 1 wff CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)})
Colors of variables: wff setvar class
This definition is referenced by:  caragenval  45195
  Copyright terms: Public domain W3C validator