Definition df-siga

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 S and O as a parallel. (Contributed by Thierry Arnoux, 3-Sep-2016)

	Ref	Expression
Assertion	df-siga	|- sigAlgebra = ( o e. _V |-> { s | ( s C_ ~P o /\ ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csiga	|- sigAlgebra
1		vo	|- o
2		cvv	|- _V
3		vs	|- s
4	3	cv	|- s
5	1	cv	|- o
6	5	cpw	|- ~P o
7	4 6	wss	|- s C_ ~P o
8	5 4	wcel	|- o e. s
9		vx	|- x
10	9	cv	|- x
11	5 10	cdif	|- ( o \ x )
12	11 4	wcel	|- ( o \ x ) e. s
13	12 9 4	wral	|- A. x e. s ( o \ x ) e. s
14	4	cpw	|- ~P s
15		cdom	|- ~<_
16		com	|- _om
17	10 16 15	wbr	|- x ~<_ _om
18	10	cuni	|- U. x
19	18 4	wcel	|- U. x e. s
20	17 19	wi	|- ( x ~<_ _om -> U. x e. s )
21	20 9 14	wral	|- A. x e. ~P s ( x ~<_ _om -> U. x e. s )
22	8 13 21	w3a	|- ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) )
23	7 22	wa	|- ( s C_ ~P o /\ ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) )
24	23 3	cab	|- { s | ( s C_ ~P o /\ ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) }
25	1 2 24	cmpt	|- ( o e. _V |-> { s | ( s C_ ~P o /\ ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } )
26	0 25	wceq	|- sigAlgebra = ( o e. _V |-> { s | ( s C_ ~P o /\ ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } )