Definition df-salgen

Description: Define the sigma-algebra generated by a given set. Definition 111G (b) of Fremlin1 p. 13. The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set, see dfsalgen2 . The base set of the sigma-algebras used for the intersection needs to be the same, otherwise the resulting set is not guaranteed to be a sigma-algebra, as shown in the counterexample salgencntex . (Contributed by Glauco Siliprandi, 17-Aug-2020) (Revised by Glauco Siliprandi, 1-Jan-2021)

	Ref	Expression
Assertion	df-salgen	|- SalGen = ( x e. _V |-> |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csalgen	|- SalGen
1		vx	|- x
2		cvv	|- _V
3		vs	|- s
4		csalg	|- SAlg
5	3	cv	|- s
6	5	cuni	|- U. s
7	1	cv	|- x
8	7	cuni	|- U. x
9	6 8	wceq	|- U. s = U. x
10	7 5	wss	|- x C_ s
11	9 10	wa	|- ( U. s = U. x /\ x C_ s )
12	11 3 4	crab	|- { s e. SAlg | ( U. s = U. x /\ x C_ s ) }
13	12	cint	|- |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) }
14	1 2 13	cmpt	|- ( x e. _V |-> |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) } )
15	0 14	wceq	|- SalGen = ( x e. _V |-> |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) } )