Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-siga Structured version   Visualization version   GIF version

Definition df-siga 29498
 Description: Define a sigma-algebra, i.e. a set closed under complement and countable union. Literature usually uses capital greek sigma and omega letters for the algebra set, and the base set respectively. We are using 𝑆 and 𝑂 as a parallel. (Contributed by Thierry Arnoux, 3-Sep-2016.)
Assertion
Ref Expression
df-siga sigAlgebra = (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))})
Distinct variable group:   𝑜,𝑠,𝑥

Detailed syntax breakdown of Definition df-siga
StepHypRef Expression
1 csiga 29497 . 2 class sigAlgebra
2 vo . . 3 setvar 𝑜
3 cvv 3173 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1474 . . . . . 6 class 𝑠
62cv 1474 . . . . . . 7 class 𝑜
76cpw 4108 . . . . . 6 class 𝒫 𝑜
85, 7wss 3540 . . . . 5 wff 𝑠 ⊆ 𝒫 𝑜
92, 4wel 1978 . . . . . 6 wff 𝑜𝑠
10 vx . . . . . . . . . 10 setvar 𝑥
1110cv 1474 . . . . . . . . 9 class 𝑥
126, 11cdif 3537 . . . . . . . 8 class (𝑜𝑥)
1312, 5wcel 1977 . . . . . . 7 wff (𝑜𝑥) ∈ 𝑠
1413, 10, 5wral 2896 . . . . . 6 wff 𝑥𝑠 (𝑜𝑥) ∈ 𝑠
15 com 6957 . . . . . . . . 9 class ω
16 cdom 7839 . . . . . . . . 9 class
1711, 15, 16wbr 4583 . . . . . . . 8 wff 𝑥 ≼ ω
1811cuni 4372 . . . . . . . . 9 class 𝑥
1918, 5wcel 1977 . . . . . . . 8 wff 𝑥𝑠
2017, 19wi 4 . . . . . . 7 wff (𝑥 ≼ ω → 𝑥𝑠)
215cpw 4108 . . . . . . 7 class 𝒫 𝑠
2220, 10, 21wral 2896 . . . . . 6 wff 𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)
239, 14, 22w3a 1031 . . . . 5 wff (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠))
248, 23wa 383 . . . 4 wff (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))
2524, 4cab 2596 . . 3 class {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))}
262, 3, 25cmpt 4643 . 2 class (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))})
271, 26wceq 1475 1 wff sigAlgebra = (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))})
 Colors of variables: wff setvar class This definition is referenced by:  sigaval  29500  issiga  29501  isrnsigaOLD  29502  isrnsiga  29503
 Copyright terms: Public domain W3C validator