Theorem unisalgen

Description: The union of a set belongs to the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	unisalgen.x	$$⊢\phi \to X\in V$$
	unisalgen.s	$$⊢S=\mathrm{SalGen}\left(X\right)$$
	unisalgen.u	$$⊢U=\bigcup X$$
Assertion	unisalgen	$$⊢\phi \to U\in S$$

Proof

Step	Hyp	Ref	Expression
1		unisalgen.x	$$⊢\phi \to X\in V$$
2		unisalgen.s	$$⊢S=\mathrm{SalGen}\left(X\right)$$
3		unisalgen.u	$$⊢U=\bigcup X$$
4	1 2 3	salgenuni	$$⊢\phi \to \bigcup S=U$$
5	4	eqcomd	$$⊢\phi \to U=\bigcup S$$
6	2	a1i	$$⊢\phi \to S=\mathrm{SalGen}\left(X\right)$$
7		salgencl	$$⊢X\in V\to \mathrm{SalGen}\left(X\right)\in \mathrm{SAlg}$$
8	1 7	syl	$$⊢\phi \to \mathrm{SalGen}\left(X\right)\in \mathrm{SAlg}$$
9	6 8	eqeltrd	$$⊢\phi \to S\in \mathrm{SAlg}$$
10		saluni	$$⊢S\in \mathrm{SAlg}\to \bigcup S\in S$$
11	9 10	syl	$$⊢\phi \to \bigcup S\in S$$
12	5 11	eqeltrd	$$⊢\phi \to U\in S$$