Definition df-sigagen

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csigagen	|- sigaGen
1		vx	|- x
2		cvv	|- _V
3		vs	|- s
4		csiga	|- sigAlgebra
5	1	cv	|- x
6	5	cuni	|- U. x
7	6 4	cfv	|- ( sigAlgebra ` U. x )
8	3	cv	|- s
9	5 8	wss	|- x C_ s
10	9 3 7	crab	|- { s e. ( sigAlgebra ` U. x ) | x C_ s }
11	10	cint	|- |^| { s e. ( sigAlgebra ` U. x ) | x C_ s }
12	1 2 11	cmpt	|- ( x e. _V |-> |^| { s e. ( sigAlgebra ` U. x ) | x C_ s } )
13	0 12	wceq	|- sigaGen = ( x e. _V |-> |^| { s e. ( sigAlgebra ` U. x ) | x C_ s } )