Metamath Proof Explorer


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 ( ( 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) ∧ 𝐴𝑆 ) → ( sigaGen ‘ 𝐴 ) ⊆ 𝑆 )

Proof

Step Hyp Ref Expression
1 ssexg ( ( 𝐴𝑆𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) ) → 𝐴 ∈ V )
2 1 ancoms ( ( 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) ∧ 𝐴𝑆 ) → 𝐴 ∈ V )
3 sigagenval ( 𝐴 ∈ V → ( sigaGen ‘ 𝐴 ) = { 𝑠 ∈ ( sigAlgebra ‘ 𝐴 ) ∣ 𝐴𝑠 } )
4 2 3 syl ( ( 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) ∧ 𝐴𝑆 ) → ( sigaGen ‘ 𝐴 ) = { 𝑠 ∈ ( sigAlgebra ‘ 𝐴 ) ∣ 𝐴𝑠 } )
5 sseq2 ( 𝑠 = 𝑆 → ( 𝐴𝑠𝐴𝑆 ) )
6 5 intminss ( ( 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) ∧ 𝐴𝑆 ) → { 𝑠 ∈ ( sigAlgebra ‘ 𝐴 ) ∣ 𝐴𝑠 } ⊆ 𝑆 )
7 4 6 eqsstrd ( ( 𝑆 ∈ ( sigAlgebra ‘ 𝐴 ) ∧ 𝐴𝑆 ) → ( sigaGen ‘ 𝐴 ) ⊆ 𝑆 )