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