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 40000
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 39999 . 2 class CaraGen
2 vo . . 3 setvar 𝑜
3 come 39997 . . 3 class OutMeas
4 va . . . . . . . . . 10 setvar 𝑎
54cv 1479 . . . . . . . . 9 class 𝑎
6 ve . . . . . . . . . 10 setvar 𝑒
76cv 1479 . . . . . . . . 9 class 𝑒
85, 7cin 3559 . . . . . . . 8 class (𝑎𝑒)
92cv 1479 . . . . . . . 8 class 𝑜
108, 9cfv 5850 . . . . . . 7 class (𝑜‘(𝑎𝑒))
115, 7cdif 3557 . . . . . . . 8 class (𝑎𝑒)
1211, 9cfv 5850 . . . . . . 7 class (𝑜‘(𝑎𝑒))
13 cxad 11888 . . . . . . 7 class +𝑒
1410, 12, 13co 6605 . . . . . 6 class ((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒)))
155, 9cfv 5850 . . . . . 6 class (𝑜𝑎)
1614, 15wceq 1480 . . . . 5 wff ((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)
179cdm 5079 . . . . . . 7 class dom 𝑜
1817cuni 4407 . . . . . 6 class dom 𝑜
1918cpw 4135 . . . . 5 class 𝒫 dom 𝑜
2016, 4, 19wral 2912 . . . 4 wff 𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)
2120, 6, 19crab 2916 . . 3 class {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)}
222, 3, 21cmpt 4678 . 2 class (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)})
231, 22wceq 1480 1 wff CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 dom 𝑜((𝑜‘(𝑎𝑒)) +𝑒 (𝑜‘(𝑎𝑒))) = (𝑜𝑎)})
Colors of variables: wff setvar class
This definition is referenced by:  caragenval  40001
  Copyright terms: Public domain W3C validator