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

Step	Hyp	Ref	Expression
1		csiga 29497	. 2 class sigAlgebra
2		vo	. . 3 setvar 𝑜
3		cvv 3173	. . 3 class V
4		vs	. . . . . . 7 setvar 𝑠
5	4	cv 1474	. . . . . 6 class 𝑠
6	2	cv 1474	. . . . . . 7 class 𝑜
7	6	cpw 4108	. . . . . 6 class 𝒫 𝑜
8	5, 7	wss 3540	. . . . 5 wff 𝑠 ⊆ 𝒫 𝑜
9	2, 4	wel 1978	. . . . . 6 wff 𝑜 ∈ 𝑠
10		vx	. . . . . . . . . 10 setvar 𝑥
11	10	cv 1474	. . . . . . . . 9 class 𝑥
12	6, 11	cdif 3537	. . . . . . . 8 class (𝑜 ∖ 𝑥)
13	12, 5	wcel 1977	. . . . . . 7 wff (𝑜 ∖ 𝑥) ∈ 𝑠
14	13, 10, 5	wral 2896	. . . . . 6 wff ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠
15		com 6957	. . . . . . . . 9 class ω
16		cdom 7839	. . . . . . . . 9 class ≼
17	11, 15, 16	wbr 4583	. . . . . . . 8 wff 𝑥 ≼ ω
18	11	cuni 4372	. . . . . . . . 9 class ∪ 𝑥
19	18, 5	wcel 1977	. . . . . . . 8 wff ∪ 𝑥 ∈ 𝑠
20	17, 19	wi 4	. . . . . . 7 wff (𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)
21	5	cpw 4108	. . . . . . 7 class 𝒫 𝑠
22	20, 10, 21	wral 2896	. . . . . 6 wff ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)
23	9, 14, 22	w3a 1031	. . . . 5 wff (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
24	8, 23	wa 383	. . . 4 wff (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))
25	24, 4	cab 2596	. . 3 class {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))}
26	2, 3, 25	cmpt 4643	. 2 class (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))})
27	1, 26	wceq 1475	1 wff sigAlgebra = (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))})

This definition is referenced by:  sigaval  29500  issiga  29501  isrnsigaOLD  29502  isrnsiga  29503