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 \leftrightarrow \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)\leftrightarrow \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)$$