Theorem sigagenss

Description: The generated sigma-algebra is a subset of all sigma-algebras containing the generating set, i.e. the generated sigma-algebra is the smallest sigma-algebra containing the generating set, here A . (Contributed by Thierry Arnoux, 4-Jun-2017)

	Ref	Expression
Assertion	sigagenss	|- ( ( S e. ( sigAlgebra ` U. A ) /\ A C_ S ) -> ( sigaGen ` A ) C_ S )

Proof

Step	Hyp	Ref	Expression
1		ssexg	|- ( ( A C_ S /\ S e. ( sigAlgebra ` U. A ) ) -> A e. _V )
2	1	ancoms	|- ( ( S e. ( sigAlgebra ` U. A ) /\ A C_ S ) -> A e. _V )
3		sigagenval	|- ( A e. _V -> ( sigaGen ` A ) = |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } )
4	2 3	syl	|- ( ( S e. ( sigAlgebra ` U. A ) /\ A C_ S ) -> ( sigaGen ` A ) = |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } )
5		sseq2	|- ( s = S -> ( A C_ s <-> A C_ S ) )
6	5	intminss	|- ( ( S e. ( sigAlgebra ` U. A ) /\ A C_ S ) -> |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } C_ S )
7	4 6	eqsstrd	|- ( ( S e. ( sigAlgebra ` U. A ) /\ A C_ S ) -> ( sigaGen ` A ) C_ S )