Theorem salgencld

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

	Ref	Expression
Hypotheses	salgencld.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	salgencld.2	⊢ 𝑆 = ( SalGen ‘ 𝑋 )
Assertion	salgencld	⊢ ( 𝜑 → 𝑆 ∈ SAlg )

Proof

Step	Hyp	Ref	Expression
1		salgencld.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		salgencld.2	⊢ 𝑆 = ( SalGen ‘ 𝑋 )
3		salgencl	⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) ∈ SAlg )
4	1 3	syl	⊢ ( 𝜑 → ( SalGen ‘ 𝑋 ) ∈ SAlg )
5	2 4	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ SAlg )