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 32073
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 32072 . 2 class sigAlgebra
2 vo . . 3 setvar 𝑜
3 cvv 3431 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1541 . . . . . 6 class 𝑠
62cv 1541 . . . . . . 7 class 𝑜
76cpw 4539 . . . . . 6 class 𝒫 𝑜
85, 7wss 3892 . . . . 5 wff 𝑠 ⊆ 𝒫 𝑜
92, 4wel 2111 . . . . . 6 wff 𝑜𝑠
10 vx . . . . . . . . . 10 setvar 𝑥
1110cv 1541 . . . . . . . . 9 class 𝑥
126, 11cdif 3889 . . . . . . . 8 class (𝑜𝑥)
1312, 5wcel 2110 . . . . . . 7 wff (𝑜𝑥) ∈ 𝑠
1413, 10, 5wral 3066 . . . . . 6 wff 𝑥𝑠 (𝑜𝑥) ∈ 𝑠
15 com 7706 . . . . . . . . 9 class ω
16 cdom 8714 . . . . . . . . 9 class
1711, 15, 16wbr 5079 . . . . . . . 8 wff 𝑥 ≼ ω
1811cuni 4845 . . . . . . . . 9 class 𝑥
1918, 5wcel 2110 . . . . . . . 8 wff 𝑥𝑠
2017, 19wi 4 . . . . . . 7 wff (𝑥 ≼ ω → 𝑥𝑠)
215cpw 4539 . . . . . . 7 class 𝒫 𝑠
2220, 10, 21wral 3066 . . . . . 6 wff 𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)
239, 14, 22w3a 1086 . . . . 5 wff (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠))
248, 23wa 396 . . . 4 wff (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))
2524, 4cab 2717 . . 3 class {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))}
262, 3, 25cmpt 5162 . 2 class (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))})
271, 26wceq 1542 1 wff sigAlgebra = (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜𝑠 ∧ ∀𝑥𝑠 (𝑜𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → 𝑥𝑠)))})
Colors of variables: wff setvar class
This definition is referenced by:  sigaval  32075  issiga  32076  isrnsiga  32077
  Copyright terms: Public domain W3C validator