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 44012
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 44011 . 2 class CaraGen
2 vo . . 3 setvar 𝑜
3 come 44009 . . 3 class OutMeas
4 va . . . . . . . . . 10 setvar 𝑎
54cv 1541 . . . . . . . . 9 class 𝑎
6 ve . . . . . . . . . 10 setvar 𝑒
76cv 1541 . . . . . . . . 9 class 𝑒
85, 7cin 3891 . . . . . . . 8 class (𝑎𝑒)
92cv 1541 . . . . . . . 8 class 𝑜
108, 9cfv 6432 . . . . . . 7 class (𝑜‘(𝑎𝑒))
115, 7cdif 3889 . . . . . . . 8 class (𝑎𝑒)
1211, 9cfv 6432 . . . . . . 7 class (𝑜‘(𝑎𝑒))
13 cxad 12857 . . . . . . 7 class +𝑒
1410, 12, 13co 7272 . . . . . 6 class ((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒)))
155, 9cfv 6432 . . . . . 6 class (𝑜𝑎)
1614, 15wceq 1542 . . . . 5 wff ((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)
179cdm 5590 . . . . . . 7 class dom 𝑜
1817cuni 4845 . . . . . 6 class dom 𝑜
1918cpw 4539 . . . . 5 class 𝒫 dom 𝑜
2016, 4, 19wral 3066 . . . 4 wff 𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)
2120, 6, 19crab 3070 . . 3 class {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)}
222, 3, 21cmpt 5162 . 2 class (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)})
231, 22wceq 1542 1 wff CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)})
Colors of variables: wff setvar class
This definition is referenced by:  caragenval  44013
  Copyright terms: Public domain W3C validator