Theorem saliincl

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

	Ref	Expression
Hypotheses	saliincl.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	saliincl.kct	⊢ ( 𝜑 → 𝐾 ≼ ω )
	saliincl.kn0	⊢ ( 𝜑 → 𝐾 ≠ ∅ )
	saliincl.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
Assertion	saliincl	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		saliincl.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		saliincl.kct	⊢ ( 𝜑 → 𝐾 ≼ ω )
3		saliincl.kn0	⊢ ( 𝜑 → 𝐾 ≠ ∅ )
4		saliincl.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
5		nfv	⊢ Ⅎ 𝑘 𝜑
6		nfcv	⊢ Ⅎ 𝑘 𝑆
7		nfcv	⊢ Ⅎ 𝑘 𝐾
8	5 6 7 1 2 3 4	saliinclf	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )