Definition df-salg 43857

Description: Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Assertion

Ref	Expression
df-salg	⊢ SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-salg

Step	Hyp	Ref	Expression
1		csalg 43856	. 2 class SAlg
2		c0 4257	. . . . 5 class ∅
3		vx	. . . . . 6 setvar 𝑥
4	3	cv 1538	. . . . 5 class 𝑥
5	2, 4	wcel 2107	. . . 4 wff ∅ ∈ 𝑥
6	4	cuni 4840	. . . . . . 7 class ∪ 𝑥
7		vy	. . . . . . . 8 setvar 𝑦
8	7	cv 1538	. . . . . . 7 class 𝑦
9	6, 8	cdif 3885	. . . . . 6 class (∪ 𝑥 ∖ 𝑦)
10	9, 4	wcel 2107	. . . . 5 wff (∪ 𝑥 ∖ 𝑦) ∈ 𝑥
11	10, 7, 4	wral 3065	. . . 4 wff ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥
12		com 7721	. . . . . . 7 class ω
13		cdom 8740	. . . . . . 7 class ≼
14	8, 12, 13	wbr 5075	. . . . . 6 wff 𝑦 ≼ ω
15	8	cuni 4840	. . . . . . 7 class ∪ 𝑦
16	15, 4	wcel 2107	. . . . . 6 wff ∪ 𝑦 ∈ 𝑥
17	14, 16	wi 4	. . . . 5 wff (𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥)
18	4	cpw 4534	. . . . 5 class 𝒫 𝑥
19	17, 7, 18	wral 3065	. . . 4 wff ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥)
20	5, 11, 19	w3a 1086	. . 3 wff (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))
21	20, 3	cab 2716	. 2 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))}
22	1, 21	wceq 1539	1 wff SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))}

This definition is referenced by:  issal  43862