Definition df-salgen 40533

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 40559. 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 40561. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.)

Assertion

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

Distinct variable group:   x, s

Detailed syntax breakdown of Definition df-salgen

Step	Hyp	Ref	Expression
1		csalgen 40532	. 2 class SalGen
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vs	. . . . . . . . 9 setvar s
5	4	cv 1482	. . . . . . . 8 class s
6	5	cuni 4436	. . . . . . 7 class U. s
7	2	cv 1482	. . . . . . . 8 class x
8	7	cuni 4436	. . . . . . 7 class U. x
9	6, 8	wceq 1483	. . . . . 6 wff U. s = U. x
10	7, 5	wss 3574	. . . . . 6 wff x C_ s
11	9, 10	wa 384	. . . . 5 wff ( U. s = U. x /\ x C_ s )
12		csalg 40528	. . . . 5 class SAlg
13	11, 4, 12	crab 2916	. . . 4 class { s e. SAlg | ( U. s = U. x /\ x C_ s ) }
14	13	cint 4475	. . 3 class |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) }
15	2, 3, 14	cmpt 4729	. 2 class ( x e. _V |-> |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) } )
16	1, 15	wceq 1483	1 wff SalGen = ( x e. _V |-> |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) } )

This definition is referenced by:  salgenval  40541