Theorem salgencld

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

	Ref	Expression
Hypotheses	salgencld.1	|- ( ph -> X e. V )
	salgencld.2	|- S = ( SalGen ` X )
Assertion	salgencld	|- ( ph -> S e. SAlg )

Proof

Step	Hyp	Ref	Expression
1		salgencld.1	|- ( ph -> X e. V )
2		salgencld.2	|- S = ( SalGen ` X )
3		salgencl	|- ( X e. V -> ( SalGen ` X ) e. SAlg )
4	1 3	syl	|- ( ph -> ( SalGen ` X ) e. SAlg )
5	2 4	eqeltrid	|- ( ph -> S e. SAlg )