Theorem sgsiga

Description: A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 30-Jan-2017)

	Ref	Expression
Hypothesis	sgsiga.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	sgsiga	⊢ ( 𝜑 → ( sigaGen ‘ 𝐴 ) ∈ ∪ ran sigAlgebra )

Proof

Step	Hyp	Ref	Expression
1		sgsiga.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		sigagensiga	⊢ ( 𝐴 ∈ 𝑉 → ( sigaGen ‘ 𝐴 ) ∈ ( sigAlgebra ‘ ∪ 𝐴 ) )
3		elrnsiga	⊢ ( ( sigaGen ‘ 𝐴 ) ∈ ( sigAlgebra ‘ ∪ 𝐴 ) → ( sigaGen ‘ 𝐴 ) ∈ ∪ ran sigAlgebra )
4	1 2 3	3syl	⊢ ( 𝜑 → ( sigaGen ‘ 𝐴 ) ∈ ∪ ran sigAlgebra )