Theorem sigaclfu

Description: A sigma-algebra is closed under finite union. (Contributed by Thierry Arnoux, 28-Dec-2016)

	Ref	Expression
Assertion	sigaclfu	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ∈ Fin ) → ∪ 𝐴 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		fict	⊢ ( 𝐴 ∈ Fin → 𝐴 ≼ ω )
2		sigaclcu	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω ) → ∪ 𝐴 ∈ 𝑆 )
3	1 2	syl3an3	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ∈ Fin ) → ∪ 𝐴 ∈ 𝑆 )