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	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	unisalgen.s	⊢ 𝑆 = ( SalGen ‘ 𝑋 )
	unisalgen.u	⊢ 𝑈 = ∪ 𝑋
Assertion	unisalgen	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		unisalgen.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		unisalgen.s	⊢ 𝑆 = ( SalGen ‘ 𝑋 )
3		unisalgen.u	⊢ 𝑈 = ∪ 𝑋
4	1 2 3	salgenuni	⊢ ( 𝜑 → ∪ 𝑆 = 𝑈 )
5	4	eqcomd	⊢ ( 𝜑 → 𝑈 = ∪ 𝑆 )
6	2	a1i	⊢ ( 𝜑 → 𝑆 = ( SalGen ‘ 𝑋 ) )
7		salgencl	⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) ∈ SAlg )
8	1 7	syl	⊢ ( 𝜑 → ( SalGen ‘ 𝑋 ) ∈ SAlg )
9	6 8	eqeltrd	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
10		saluni	⊢ ( 𝑆 ∈ SAlg → ∪ 𝑆 ∈ 𝑆 )
11	9 10	syl	⊢ ( 𝜑 → ∪ 𝑆 ∈ 𝑆 )
12	5 11	eqeltrd	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )