Definition df-sigagen 30202

Description: Define the sigma-algebra generated by a given collection of sets as the intersection of all sigma-algebra containing that set. (Contributed by Thierry Arnoux, 27-Dec-2016.)

Assertion

Ref	Expression
df-sigagen	|- sigaGen = ( x e. _V |-> |^| { s e. (sigAlgebra ` U. x ) | x C_ s } )

Distinct variable group:   x, s

Detailed syntax breakdown of Definition df-sigagen

Step	Hyp	Ref	Expression
1		csigagen 30201	. 2 class sigaGen
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . . 6 class x
5		vs	. . . . . . 7 setvar s
6	5	cv 1482	. . . . . 6 class s
7	4, 6	wss 3574	. . . . 5 wff x C_ s
8	4	cuni 4436	. . . . . 6 class U. x
9		csiga 30170	. . . . . 6 class sigAlgebra
10	8, 9	cfv 5888	. . . . 5 class (sigAlgebra ` U. x )
11	7, 5, 10	crab 2916	. . . 4 class { s e. (sigAlgebra ` U. x ) | x C_ s }
12	11	cint 4475	. . 3 class |^| { s e. (sigAlgebra ` U. x ) | x C_ s }
13	2, 3, 12	cmpt 4729	. 2 class ( x e. _V |-> |^| { s e. (sigAlgebra ` U. x ) | x C_ s } )
14	1, 13	wceq 1483	1 wff sigaGen = ( x e. _V |-> |^| { s e. (sigAlgebra ` U. x ) | x C_ s } )

This definition is referenced by:  sigagenval  30203  dmsigagen  30207  brsiga  30246