Metamath Proof Explorer


Theorem sigaclfu

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

Ref Expression
Assertion sigaclfu S ran sigAlgebra A 𝒫 S A Fin A S

Proof

Step Hyp Ref Expression
1 fict A Fin A ω
2 sigaclcu S ran sigAlgebra A 𝒫 S A ω A S
3 1 2 syl3an3 S ran sigAlgebra A 𝒫 S A Fin A S