Theorem sgon

Description: A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017)

	Ref	Expression
Assertion	sgon	|- ( S e. U. ran sigAlgebra -> S e. ( sigAlgebra ` U. S ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- U. S = U. S
2		issgon	|- ( S e. ( sigAlgebra ` U. S ) <-> ( S e. U. ran sigAlgebra /\ U. S = U. S ) )
3	2	biimpri	|- ( ( S e. U. ran sigAlgebra /\ U. S = U. S ) -> S e. ( sigAlgebra ` U. S ) )
4	1 3	mpan2	|- ( S e. U. ran sigAlgebra -> S e. ( sigAlgebra ` U. S ) )