Theorem saliincl

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

	Ref	Expression
Hypotheses	saliincl.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	saliincl.kct	$$⊢\phi \to K\preccurlyeq \mathrm{\omega }$$
	saliincl.kn0	$$⊢\phi \to K\ne \varnothing$$
	saliincl.e	$$⊢\left(\phi \wedge k\in K\right)\to E\in S$$
Assertion	saliincl	$$⊢\phi \to \bigcap _{k\in K}E\in S$$

Proof

Step	Hyp	Ref	Expression
1		saliincl.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
2		saliincl.kct	$$⊢\phi \to K\preccurlyeq \mathrm{\omega }$$
3		saliincl.kn0	$$⊢\phi \to K\ne \varnothing$$
4		saliincl.e	$$⊢\left(\phi \wedge k\in K\right)\to E\in S$$
5		nfv	$$⊢Ⅎk\phi$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}kS$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}kK$$
8	5 6 7 1 2 3 4	saliinclf	$$⊢\phi \to \bigcap _{k\in K}E\in S$$