Theorem salgencld

Description: SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	salgencld.1	$$⊢\phi \to X\in V$$
	salgencld.2	$$⊢S=\mathrm{SalGen}\left(X\right)$$
Assertion	salgencld	$$⊢\phi \to S\in \mathrm{SAlg}$$

Proof

Step	Hyp	Ref	Expression
1		salgencld.1	$$⊢\phi \to X\in V$$
2		salgencld.2	$$⊢S=\mathrm{SalGen}\left(X\right)$$
3		salgencl	$$⊢X\in V\to \mathrm{SalGen}\left(X\right)\in \mathrm{SAlg}$$
4	1 3	syl	$$⊢\phi \to \mathrm{SalGen}\left(X\right)\in \mathrm{SAlg}$$
5	2 4	eqeltrid	$$⊢\phi \to S\in \mathrm{SAlg}$$