Metamath Proof Explorer

Theorem sssigagen

Description: A set is a subset of the sigma-algebra it generates. (Contributed by Thierry Arnoux, 24-Jan-2017)

Ref Expression
Assertion sssigagen 
|- ( A e. V -> A C_ ( sigaGen ` A ) )

Proof

Step Hyp Ref Expression
1 ssintub 
 |-  A C_ |^| { s e. ( sigAlgebra ` U. A ) | A C_ s }
2 sigagenval 
 |-  ( A e. V -> ( sigaGen ` A ) = |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } )
3 1 2 sseqtrrid 
 |-  ( A e. V -> A C_ ( sigaGen ` A ) )