Definition df-salg

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

	Ref	Expression
Assertion	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 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csalg	|- SAlg
1		vx	|- x
2		c0	|- (/)
3	1	cv	|- x
4	2 3	wcel	|- (/) e. x
5		vy	|- y
6	3	cuni	|- U. x
7	5	cv	|- y
8	6 7	cdif	|- ( U. x \ y )
9	8 3	wcel	|- ( U. x \ y ) e. x
10	9 5 3	wral	|- A. y e. x ( U. x \ y ) e. x
11	3	cpw	|- ~P x
12		cdom	|- ~<_
13		com	|- _om
14	7 13 12	wbr	|- y ~<_ _om
15	7	cuni	|- U. y
16	15 3	wcel	|- U. y e. x
17	14 16	wi	|- ( y ~<_ _om -> U. y e. x )
18	17 5 11	wral	|- A. y e. ~P x ( y ~<_ _om -> U. y e. x )
19	4 10 18	w3a	|- ( (/) e. x /\ A. y e. x ( U. x \ y ) e. x /\ A. y e. ~P x ( y ~<_ _om -> U. y e. x ) )
20	19 1	cab	|- { x | ( (/) e. x /\ A. y e. x ( U. x \ y ) e. x /\ A. y e. ~P x ( y ~<_ _om -> U. y e. x ) ) }
21	0 20	wceq	|- SAlg = { x | ( (/) e. x /\ A. y e. x ( U. x \ y ) e. x /\ A. y e. ~P x ( y ~<_ _om -> U. y e. x ) ) }