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 ‘ 𝐴 ) ⊆ 𝑆 )