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 e. U. ran sigAlgebra /\ A e. ~P S /\ A e. Fin ) -> U. A e. S )

Proof

Step Hyp Ref Expression
1 fict 
 |-  ( A e. Fin -> A ~<_ _om )
2 sigaclcu 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S /\ A ~<_ _om ) -> U. A e. S )
3 1 2 syl3an3 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S /\ A e. Fin ) -> U. A e. S )