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 \in ⋃ ran sigAlgebra \land A \in 𝒫 S \land A \in Fin) \to ⋃ A \in S$

Step	Hyp	Ref	Expression
1		fict	$⊢ A \in Fin \to A ≼ ω$
2		sigaclcu	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S \land A ≼ ω) \to ⋃ A \in S$
3	1 2	syl3an3	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S \land A \in Fin) \to ⋃ A \in S$