# Metamath Proof Explorer

## 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 ${setvar}{x}$
2 cvv ${class}\mathrm{V}$
3 vs ${setvar}{s}$
4 csiga ${class}\mathrm{sigAlgebra}$
5 1 cv ${setvar}{x}$
6 5 cuni ${class}\bigcup {x}$
7 6 4 cfv ${class}\mathrm{sigAlgebra}\left(\bigcup {x}\right)$
8 3 cv ${setvar}{s}$
9 5 8 wss ${wff}{x}\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)$