Definition df-siga 28338

Description: Define a sigma-algebra, i.e. a set closed under complement and countable union. Litterature 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 28337	. 2 class sigAlgebra
2		vo	. . 3 setvar o
3		cvv 3106	. . 3 class _V
4		vs	. . . . . . 7 setvar s
5	4	cv 1397	. . . . . 6 class s
6	2	cv 1397	. . . . . . 7 class o
7	6	cpw 3999	. . . . . 6 class ~P o
8	5, 7	wss 3461	. . . . 5 wff s C_ ~P o
9	2, 4	wel 1824	. . . . . 6 wff o e. s
10		vx	. . . . . . . . . 10 setvar x
11	10	cv 1397	. . . . . . . . 9 class x
12	6, 11	cdif 3458	. . . . . . . 8 class ( o \ x )
13	12, 5	wcel 1823	. . . . . . 7 wff ( o \ x ) e. s
14	13, 10, 5	wral 2804	. . . . . 6 wff A. x e. s ( o \ x ) e. s
15		com 6673	. . . . . . . . 9 class om
16		cdom 7507	. . . . . . . . 9 class ~<_
17	11, 15, 16	wbr 4439	. . . . . . . 8 wff x ~<_ om
18	11	cuni 4235	. . . . . . . . 9 class U. x
19	18, 5	wcel 1823	. . . . . . . 8 wff U. x e. s
20	17, 19	wi 4	. . . . . . 7 wff ( x ~<_ om -> U. x e. s )
21	5	cpw 3999	. . . . . . 7 class ~P s
22	20, 10, 21	wral 2804	. . . . . 6 wff A. x e. ~P s ( x ~<_ om -> U. x e. s )
23	9, 14, 22	w3a 971	. . . . 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 367	. . . 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 2439	. . 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 4497	. 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 1398	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  28340  issiga  28341  isrnsigaOLD  28342  isrnsiga  28343