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

Detailed syntax breakdown

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