Theorem unisg

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

	Ref	Expression
Assertion	unisg	$$⊢A\in V\to \bigcup 𝛔\left(A\right)=\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		sigagensiga	$$⊢A\in V\to 𝛔\left(A\right)\in \mathrm{sigAlgebra}\left(\bigcup A\right)$$
2		issgon	$$⊢𝛔\left(A\right)\in \mathrm{sigAlgebra}\left(\bigcup A\right)\leftrightarrow \left(𝛔\left(A\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \bigcup A=\bigcup 𝛔\left(A\right)\right)$$
3	1 2	sylib	$$⊢A\in V\to \left(𝛔\left(A\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \bigcup A=\bigcup 𝛔\left(A\right)\right)$$
4	3	simprd	$$⊢A\in V\to \bigcup A=\bigcup 𝛔\left(A\right)$$
5	4	eqcomd	$$⊢A\in V\to \bigcup 𝛔\left(A\right)=\bigcup A$$