Theorem saliincl

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

	Ref	Expression
Hypotheses	saliincl.s	|- ( ph -> S e. SAlg )
	saliincl.kct	|- ( ph -> K ~<_ _om )
	saliincl.kn0	|- ( ph -> K =/= (/) )
	saliincl.e	|- ( ( ph /\ k e. K ) -> E e. S )
Assertion	saliincl	|- ( ph -> |^|_ k e. K E e. S )

Proof

Step	Hyp	Ref	Expression
1		saliincl.s	|- ( ph -> S e. SAlg )
2		saliincl.kct	|- ( ph -> K ~<_ _om )
3		saliincl.kn0	|- ( ph -> K =/= (/) )
4		saliincl.e	|- ( ( ph /\ k e. K ) -> E e. S )
5		nfv	|- F/ k ph
6		nfcv	|- F/_ k S
7		nfcv	|- F/_ k K
8	5 6 7 1 2 3 4	saliinclf	|- ( ph -> |^|_ k e. K E e. S )