Definition df-salg 40529

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

Assertion

Ref	Expression
df-salg	|- SAlg = { x | ( (/) e. x /\ A. y e. x ( U. x \ y ) e. x /\ A. y e. ~P x ( y ~<_ om -> U. y e. x ) ) }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-salg

Step	Hyp	Ref	Expression
1		csalg 40528	. 2 class SAlg
2		c0 3915	. . . . 5 class (/)
3		vx	. . . . . 6 setvar x
4	3	cv 1482	. . . . 5 class x
5	2, 4	wcel 1990	. . . 4 wff (/) e. x
6	4	cuni 4436	. . . . . . 7 class U. x
7		vy	. . . . . . . 8 setvar y
8	7	cv 1482	. . . . . . 7 class y
9	6, 8	cdif 3571	. . . . . 6 class ( U. x \ y )
10	9, 4	wcel 1990	. . . . 5 wff ( U. x \ y ) e. x
11	10, 7, 4	wral 2912	. . . 4 wff A. y e. x ( U. x \ y ) e. x
12		com 7065	. . . . . . 7 class om
13		cdom 7953	. . . . . . 7 class ~<_
14	8, 12, 13	wbr 4653	. . . . . 6 wff y ~<_ om
15	8	cuni 4436	. . . . . . 7 class U. y
16	15, 4	wcel 1990	. . . . . 6 wff U. y e. x
17	14, 16	wi 4	. . . . 5 wff ( y ~<_ om -> U. y e. x )
18	4	cpw 4158	. . . . 5 class ~P x
19	17, 7, 18	wral 2912	. . . 4 wff A. y e. ~P x ( y ~<_ om -> U. y e. x )
20	5, 11, 19	w3a 1037	. . 3 wff ( (/) e. x /\ A. y e. x ( U. x \ y ) e. x /\ A. y e. ~P x ( y ~<_ om -> U. y e. x ) )
21	20, 3	cab 2608	. 2 class { x | ( (/) e. x /\ A. y e. x ( U. x \ y ) e. x /\ A. y e. ~P x ( y ~<_ om -> U. y e. x ) ) }
22	1, 21	wceq 1483	1 wff SAlg = { x | ( (/) e. x /\ A. y e. x ( U. x \ y ) e. x /\ A. y e. ~P x ( y ~<_ om -> U. y e. x ) ) }

This definition is referenced by:  issal  40534