Definition df-siga 30171

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.)

Assertion

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

Distinct variable group:   o, s, x

Detailed syntax breakdown of Definition df-siga

Step	Hyp	Ref	Expression
1		csiga 30170	. 2 class sigAlgebra
2		vo	. . 3 setvar o
3		cvv 3200	. . 3 class _V
4		vs	. . . . . . 7 setvar s
5	4	cv 1482	. . . . . 6 class s
6	2	cv 1482	. . . . . . 7 class o
7	6	cpw 4158	. . . . . 6 class ~P o
8	5, 7	wss 3574	. . . . 5 wff s C_ ~P o
9	2, 4	wel 1991	. . . . . 6 wff o e. s
10		vx	. . . . . . . . . 10 setvar x
11	10	cv 1482	. . . . . . . . 9 class x
12	6, 11	cdif 3571	. . . . . . . 8 class ( o \ x )
13	12, 5	wcel 1990	. . . . . . 7 wff ( o \ x ) e. s
14	13, 10, 5	wral 2912	. . . . . 6 wff A. x e. s ( o \ x ) e. s
15		com 7065	. . . . . . . . 9 class om
16		cdom 7953	. . . . . . . . 9 class ~<_
17	11, 15, 16	wbr 4653	. . . . . . . 8 wff x ~<_ om
18	11	cuni 4436	. . . . . . . . 9 class U. x
19	18, 5	wcel 1990	. . . . . . . 8 wff U. x e. s
20	17, 19	wi 4	. . . . . . 7 wff ( x ~<_ om -> U. x e. s )
21	5	cpw 4158	. . . . . . 7 class ~P s
22	20, 10, 21	wral 2912	. . . . . 6 wff A. x e. ~P s ( x ~<_ om -> U. x e. s )
23	9, 14, 22	w3a 1037	. . . . 5 wff ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ om -> U. x e. s ) )
24	8, 23	wa 384	. . . 4 wff ( 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	24, 4	cab 2608	. . 3 class { 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	2, 3, 25	cmpt 4729	. 2 class ( 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 ) ) ) } )
27	1, 26	wceq 1483	1 wff 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 ) ) ) } )

This definition is referenced by:  sigaval  30173  issiga  30174  isrnsigaOLD  30175  isrnsiga  30176