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	$$⊢\mathrm{SalGen}=\left(x\in \mathrm{V}⟼\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csalgen	$$class\mathrm{SalGen}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		csalg	$$class\mathrm{SAlg}$$
5	3	cv	$$setvars$$
6	5	cuni	$$class\bigcup s$$
7	1	cv	$$setvarx$$
8	7	cuni	$$class\bigcup x$$
9	6 8	wceq	$$wff\bigcup s=\bigcup x$$
10	7 5	wss	$$wffx\subseteq s$$
11	9 10	wa	$$wff\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)$$
12	11 3 4	crab	$$class\left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\right\}$$
13	12	cint	$$class\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\right\}$$
14	1 2 13	cmpt	$$class\left(x\in \mathrm{V}⟼\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\right\}\right)$$
15	0 14	wceq	$$wff\mathrm{SalGen}=\left(x\in \mathrm{V}⟼\bigcap \left\{s\in \mathrm{SAlg}|\left(\bigcup s=\bigcup x\wedge x\subseteq s\right)\right\}\right)$$