Definition df-siga 27859

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 27858	. 2 class sigAlgebra
2		vo	. . 3 setvar o
3		cvv 3113	. . 3 class _V
4		vs	. . . . . . 7 setvar s
5	4	cv 1378	. . . . . 6 class s
6	2	cv 1378	. . . . . . 7 class o
7	6	cpw 4010	. . . . . 6 class ~P o
8	5, 7	wss 3476	. . . . 5 wff s C_ ~P o
9	2, 4	wel 1768	. . . . . 6 wff o e. s
10		vx	. . . . . . . . . 10 setvar x
11	10	cv 1378	. . . . . . . . 9 class x
12	6, 11	cdif 3473	. . . . . . . 8 class ( o \ x )
13	12, 5	wcel 1767	. . . . . . 7 wff ( o \ x ) e. s
14	13, 10, 5	wral 2814	. . . . . 6 wff A. x e. s ( o \ x ) e. s
15		com 6685	. . . . . . . . 9 class om
16		cdom 7515	. . . . . . . . 9 class ~<_
17	11, 15, 16	wbr 4447	. . . . . . . 8 wff x ~<_ om
18	11	cuni 4245	. . . . . . . . 9 class U. x
19	18, 5	wcel 1767	. . . . . . . 8 wff U. x e. s
20	17, 19	wi 4	. . . . . . 7 wff ( x ~<_ om -> U. x e. s )
21	5	cpw 4010	. . . . . . 7 class ~P s
22	20, 10, 21	wral 2814	. . . . . 6 wff A. x e. ~P s ( x ~<_ om -> U. x e. s )
23	9, 14, 22	w3a 973	. . . . 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 369	. . . 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 2452	. . 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 4505	. 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 1379	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  27861  issiga  27862  isrnsigaOLD  27863  isrnsiga  27864