Metamath Proof Explorer


Definition df-caragen

Description: Define the sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion df-caragen CaraGen = o OutMeas e 𝒫 dom o | a 𝒫 dom o o a e + 𝑒 o a e = o a

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccaragen class CaraGen
1 vo setvar o
2 come class OutMeas
3 ve setvar e
4 1 cv setvar o
5 4 cdm class dom o
6 5 cuni class dom o
7 6 cpw class 𝒫 dom o
8 va setvar a
9 8 cv setvar a
10 3 cv setvar e
11 9 10 cin class a e
12 11 4 cfv class o a e
13 cxad class + 𝑒
14 9 10 cdif class a e
15 14 4 cfv class o a e
16 12 15 13 co class o a e + 𝑒 o a e
17 9 4 cfv class o a
18 16 17 wceq wff o a e + 𝑒 o a e = o a
19 18 8 7 wral wff a 𝒫 dom o o a e + 𝑒 o a e = o a
20 19 3 7 crab class e 𝒫 dom o | a 𝒫 dom o o a e + 𝑒 o a e = o a
21 1 2 20 cmpt class o OutMeas e 𝒫 dom o | a 𝒫 dom o o a e + 𝑒 o a e = o a
22 0 21 wceq wff CaraGen = o OutMeas e 𝒫 dom o | a 𝒫 dom o o a e + 𝑒 o a e = o a