Theorem unisg

Description: The sigma-algebra generated by a collection A is a sigma-algebra on U. A . (Contributed by Thierry Arnoux, 27-Dec-2016)

	Ref	Expression
Assertion	unisg	|- ( A e. V -> U. ( sigaGen ` A ) = U. A )

Proof

Step	Hyp	Ref	Expression
1		sigagensiga	|- ( A e. V -> ( sigaGen ` A ) e. ( sigAlgebra ` U. A ) )
2		issgon	|- ( ( sigaGen ` A ) e. ( sigAlgebra ` U. A ) <-> ( ( sigaGen ` A ) e. U. ran sigAlgebra /\ U. A = U. ( sigaGen ` A ) ) )
3	1 2	sylib	|- ( A e. V -> ( ( sigaGen ` A ) e. U. ran sigAlgebra /\ U. A = U. ( sigaGen ` A ) ) )
4	3	simprd	|- ( A e. V -> U. A = U. ( sigaGen ` A ) )
5	4	eqcomd	|- ( A e. V -> U. ( sigaGen ` A ) = U. A )