Theorem saliuncl

Description: SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	saliuncl.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	saliuncl.kct	⊢ ( 𝜑 → 𝐾 ≼ ω )
	saliuncl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
Assertion	saliuncl	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		saliuncl.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		saliuncl.kct	⊢ ( 𝜑 → 𝐾 ≼ ω )
3		saliuncl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
4		nfv	⊢ Ⅎ 𝑘 𝜑
5		nfcv	⊢ Ⅎ 𝑘 𝑆
6		nfcv	⊢ Ⅎ 𝑘 𝐾
7	4 5 6 1 2 3	saliunclf	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )