Theorem sgsiga

Description: A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 30-Jan-2017)

	Ref	Expression
Hypothesis	sgsiga.1	$$⊢\phi \to A\in V$$
Assertion	sgsiga	$$⊢\phi \to 𝛔\left(A\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$

Proof

Step	Hyp	Ref	Expression
1		sgsiga.1	$$⊢\phi \to A\in V$$
2		sigagensiga	$$⊢A\in V\to 𝛔\left(A\right)\in \mathrm{sigAlgebra}\left(\bigcup A\right)$$
3		elrnsiga	$$⊢𝛔\left(A\right)\in \mathrm{sigAlgebra}\left(\bigcup A\right)\to 𝛔\left(A\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
4	1 2 3	3syl	$$⊢\phi \to 𝛔\left(A\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$