Theorem sigagenid

Description: The sigma-algebra generated by a sigma-algebra is itself. (Contributed by Thierry Arnoux, 4-Jun-2017)

	Ref	Expression
Assertion	sigagenid	|- ( S e. U. ran sigAlgebra -> ( sigaGen ` S ) = S )

Proof

Step	Hyp	Ref	Expression
1		sgon	|- ( S e. U. ran sigAlgebra -> S e. ( sigAlgebra ` U. S ) )
2		ssid	|- S C_ S
3		sigagenss	|- ( ( S e. ( sigAlgebra ` U. S ) /\ S C_ S ) -> ( sigaGen ` S ) C_ S )
4	1 2 3	sylancl	|- ( S e. U. ran sigAlgebra -> ( sigaGen ` S ) C_ S )
5		sssigagen	|- ( S e. U. ran sigAlgebra -> S C_ ( sigaGen ` S ) )
6	4 5	eqssd	|- ( S e. U. ran sigAlgebra -> ( sigaGen ` S ) = S )