Theorem sigagenid

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

	Ref	Expression
Assertion	sigagenid	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( sigaGen ‘ 𝑆 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		sgon	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) )
2		ssid	⊢ 𝑆 ⊆ 𝑆
3		sigagenss	⊢ ( ( 𝑆 ∈ ( sigAlgebra ‘ ∪ 𝑆 ) ∧ 𝑆 ⊆ 𝑆 ) → ( sigaGen ‘ 𝑆 ) ⊆ 𝑆 )
4	1 2 3	sylancl	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( sigaGen ‘ 𝑆 ) ⊆ 𝑆 )
5		sssigagen	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ⊆ ( sigaGen ‘ 𝑆 ) )
6	4 5	eqssd	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( sigaGen ‘ 𝑆 ) = 𝑆 )