Definition df-siga 28944

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 28943	. 2 class sigAlgebra
2		vo	. . 3 setvar o
3		cvv 3085	. . 3 class _V
4		vs	. . . . . . 7 setvar s
5	4	cv 1437	. . . . . 6 class s
6	2	cv 1437	. . . . . . 7 class o
7	6	cpw 3987	. . . . . 6 class ~P o
8	5, 7	wss 3442	. . . . 5 wff s C_ ~P o
9	2, 4	wel 1874	. . . . . 6 wff o e. s
10		vx	. . . . . . . . . 10 setvar x
11	10	cv 1437	. . . . . . . . 9 class x
12	6, 11	cdif 3439	. . . . . . . 8 class ( o \ x )
13	12, 5	wcel 1873	. . . . . . 7 wff ( o \ x ) e. s
14	13, 10, 5	wral 2776	. . . . . 6 wff A. x e. s ( o \ x ) e. s
15		com 6712	. . . . . . . . 9 class om
16		cdom 7584	. . . . . . . . 9 class ~<_
17	11, 15, 16	wbr 4429	. . . . . . . 8 wff x ~<_ om
18	11	cuni 4225	. . . . . . . . 9 class U. x
19	18, 5	wcel 1873	. . . . . . . 8 wff U. x e. s
20	17, 19	wi 4	. . . . . . 7 wff ( x ~<_ om -> U. x e. s )
21	5	cpw 3987	. . . . . . 7 class ~P s
22	20, 10, 21	wral 2776	. . . . . 6 wff A. x e. ~P s ( x ~<_ om -> U. x e. s )
23	9, 14, 22	w3a 983	. . . . 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 371	. . . 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 2408	. . 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 4488	. 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 1438	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  28946  issiga  28947  isrnsigaOLD  28948  isrnsiga  28949