Users' Mathboxes 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 29949
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 29948 . 2 class sigAlgebra
2 vo . . 3 setvar 𝑜
3 cvv 3186 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1479 . . . . . 6 class 𝑠
62cv 1479 . . . . . . 7 class 𝑜
76cpw 4130 . . . . . 6 class 𝒫 𝑜
85, 7wss 3555 . . . . 5 wff 𝑠 ⊆ 𝒫 𝑜
92, 4wel 1988 . . . . . 6 wff 𝑜𝑠
10 vx . . . . . . . . . 10 setvar 𝑥
1110cv 1479 . . . . . . . . 9 class 𝑥
126, 11cdif 3552 . . . . . . . 8 class (𝑜𝑥)
1312, 5wcel 1987 . . . . . . 7 wff (𝑜𝑥) ∈ 𝑠
1413, 10, 5wral 2907 . . . . . 6 wff 𝑥𝑠 (𝑜𝑥) ∈ 𝑠
15 com 7012 . . . . . . . . 9 class ω
16 cdom 7897 . . . . . . . . 9 class
1711, 15, 16wbr 4613 . . . . . . . 8 wff 𝑥 ≼ ω
1811cuni 4402 . . . . . . . . 9 class 𝑥
1918, 5wcel 1987 . . . . . . . 8 wff 𝑥𝑠
2017, 19wi 4 . . . . . . 7 wff (𝑥 ≼ ω → 𝑥𝑠)
215cpw 4130 . . . . . . 7 class 𝒫 𝑠
2220, 10, 21wral 2907 . . . . . 6 wff 𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)
239, 14, 22w3a 1036 . . . . 5 wff (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠))
248, 23wa 384 . . . 4 wff (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))
2524, 4cab 2607 . . 3 class {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))}
262, 3, 25cmpt 4673 . 2 class (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))})
271, 26wceq 1480 1 wff sigAlgebra = (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))})
Colors of variables: wff setvar class
This definition is referenced by:  sigaval  29951  issiga  29952  isrnsigaOLD  29953  isrnsiga  29954
  Copyright terms: Public domain W3C validator