Definition df-siga 31977

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 31976	. 2 class sigAlgebra
2		vo	. . 3 setvar 𝑜
3		cvv 3422	. . 3 class V
4		vs	. . . . . . 7 setvar 𝑠
5	4	cv 1538	. . . . . 6 class 𝑠
6	2	cv 1538	. . . . . . 7 class 𝑜
7	6	cpw 4530	. . . . . 6 class 𝒫 𝑜
8	5, 7	wss 3883	. . . . 5 wff 𝑠 ⊆ 𝒫 𝑜
9	2, 4	wel 2109	. . . . . 6 wff 𝑜 ∈ 𝑠
10		vx	. . . . . . . . . 10 setvar 𝑥
11	10	cv 1538	. . . . . . . . 9 class 𝑥
12	6, 11	cdif 3880	. . . . . . . 8 class (𝑜 ∖ 𝑥)
13	12, 5	wcel 2108	. . . . . . 7 wff (𝑜 ∖ 𝑥) ∈ 𝑠
14	13, 10, 5	wral 3063	. . . . . 6 wff ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠
15		com 7687	. . . . . . . . 9 class ω
16		cdom 8689	. . . . . . . . 9 class ≼
17	11, 15, 16	wbr 5070	. . . . . . . 8 wff 𝑥 ≼ ω
18	11	cuni 4836	. . . . . . . . 9 class ∪ 𝑥
19	18, 5	wcel 2108	. . . . . . . 8 wff ∪ 𝑥 ∈ 𝑠
20	17, 19	wi 4	. . . . . . 7 wff (𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)
21	5	cpw 4530	. . . . . . 7 class 𝒫 𝑠
22	20, 10, 21	wral 3063	. . . . . 6 wff ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)
23	9, 14, 22	w3a 1085	. . . . 5 wff (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
24	8, 23	wa 395	. . . 4 wff (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))
25	24, 4	cab 2715	. . 3 class {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))}
26	2, 3, 25	cmpt 5153	. 2 class (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))})
27	1, 26	wceq 1539	1 wff sigAlgebra = (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))})

This definition is referenced by:  sigaval  31979  issiga  31980  isrnsiga  31981