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	|- ( ph -> X e. V )
	unisalgen.s	|- S = ( SalGen ` X )
	unisalgen.u	|- U = U. X
Assertion	unisalgen	|- ( ph -> U e. S )

Proof

Step	Hyp	Ref	Expression
1		unisalgen.x	|- ( ph -> X e. V )
2		unisalgen.s	|- S = ( SalGen ` X )
3		unisalgen.u	|- U = U. X
4	1 2 3	salgenuni	|- ( ph -> U. S = U )
5	4	eqcomd	|- ( ph -> U = U. S )
6	2	a1i	|- ( ph -> S = ( SalGen ` X ) )
7		salgencl	|- ( X e. V -> ( SalGen ` X ) e. SAlg )
8	1 7	syl	|- ( ph -> ( SalGen ` X ) e. SAlg )
9	6 8	eqeltrd	|- ( ph -> S e. SAlg )
10		saluni	|- ( S e. SAlg -> U. S e. S )
11	9 10	syl	|- ( ph -> U. S e. S )
12	5 11	eqeltrd	|- ( ph -> U e. S )