Definition df-salg

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csalg	⊢ SAlg
1		vx	⊢ 𝑥
2		c0	⊢ ∅
3	1	cv	⊢ 𝑥
4	2 3	wcel	⊢ ∅ ∈ 𝑥
5		vy	⊢ 𝑦
6	3	cuni	⊢ ∪ 𝑥
7	5	cv	⊢ 𝑦
8	6 7	cdif	⊢ ( ∪ 𝑥 ∖ 𝑦 )
9	8 3	wcel	⊢ ( ∪ 𝑥 ∖ 𝑦 ) ∈ 𝑥
10	9 5 3	wral	⊢ ∀ 𝑦 ∈ 𝑥 ( ∪ 𝑥 ∖ 𝑦 ) ∈ 𝑥
11	3	cpw	⊢ 𝒫 𝑥
12		cdom	⊢ ≼
13		com	⊢ ω
14	7 13 12	wbr	⊢ 𝑦 ≼ ω
15	7	cuni	⊢ ∪ 𝑦
16	15 3	wcel	⊢ ∪ 𝑦 ∈ 𝑥
17	14 16	wi	⊢ ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥 )
18	17 5 11	wral	⊢ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥 )
19	4 10 18	w3a	⊢ ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ∪ 𝑥 ∖ 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥 ) )
20	19 1	cab	⊢ { 𝑥 ∣ ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ∪ 𝑥 ∖ 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥 ) ) }
21	0 20	wceq	⊢ SAlg = { 𝑥 ∣ ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ∪ 𝑥 ∖ 𝑦 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥 ) ) }