# Metamath Proof Explorer

## Theorem sigagensiga

Description: A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion sigagensiga ${⊢}{A}\in {V}\to 𝛔\left({A}\right)\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)$

### Proof

Step Hyp Ref Expression
1 sigagenval ${⊢}{A}\in {V}\to 𝛔\left({A}\right)=\bigcap \left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}$
2 fvex ${⊢}𝛔\left({A}\right)\in \mathrm{V}$
3 1 2 eqeltrrdi ${⊢}{A}\in {V}\to \bigcap \left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\in \mathrm{V}$
4 intex ${⊢}\left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\ne \varnothing ↔\bigcap \left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\in \mathrm{V}$
5 3 4 sylibr ${⊢}{A}\in {V}\to \left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\ne \varnothing$
6 ssrab2 ${⊢}\left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\subseteq \mathrm{sigAlgebra}\left(\bigcup {A}\right)$
7 6 a1i ${⊢}{A}\in {V}\to \left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\subseteq \mathrm{sigAlgebra}\left(\bigcup {A}\right)$
8 fvex ${⊢}\mathrm{sigAlgebra}\left(\bigcup {A}\right)\in \mathrm{V}$
9 8 elpw2 ${⊢}\left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\in 𝒫\mathrm{sigAlgebra}\left(\bigcup {A}\right)↔\left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\subseteq \mathrm{sigAlgebra}\left(\bigcup {A}\right)$
10 7 9 sylibr ${⊢}{A}\in {V}\to \left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\in 𝒫\mathrm{sigAlgebra}\left(\bigcup {A}\right)$
11 insiga ${⊢}\left(\left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\ne \varnothing \wedge \left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\in 𝒫\mathrm{sigAlgebra}\left(\bigcup {A}\right)\right)\to \bigcap \left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)$
12 5 10 11 syl2anc ${⊢}{A}\in {V}\to \bigcap \left\{{s}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)|{A}\subseteq {s}\right\}\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)$
13 1 12 eqeltrd ${⊢}{A}\in {V}\to 𝛔\left({A}\right)\in \mathrm{sigAlgebra}\left(\bigcup {A}\right)$