Theorem unisalgen2

Description: The union of a set belongs is equal to the union of the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	unisalgen2.x	|- ( ph -> A e. V )
	unisalgen2.s	|- S = ( SalGen ` A )
Assertion	unisalgen2	|- ( ph -> U. S = U. A )

Proof

Step	Hyp	Ref	Expression
1		unisalgen2.x	|- ( ph -> A e. V )
2		unisalgen2.s	|- S = ( SalGen ` A )
3	2	eqcomi	|- ( SalGen ` A ) = S
4	3	a1i	|- ( ph -> ( SalGen ` A ) = S )
5	1	dfsalgen2	|- ( ph -> ( ( SalGen ` A ) = S <-> ( ( S e. SAlg /\ U. S = U. A /\ A C_ S ) /\ A. x e. SAlg ( ( U. x = U. A /\ A C_ x ) -> S C_ x ) ) ) )
6	4 5	mpbid	|- ( ph -> ( ( S e. SAlg /\ U. S = U. A /\ A C_ S ) /\ A. x e. SAlg ( ( U. x = U. A /\ A C_ x ) -> S C_ x ) ) )
7	6	simpld	|- ( ph -> ( S e. SAlg /\ U. S = U. A /\ A C_ S ) )
8	7	simp2d	|- ( ph -> U. S = U. A )