Theorem saliuncl

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

	Ref	Expression
Hypotheses	saliuncl.s	|- ( ph -> S e. SAlg )
	saliuncl.kct	|- ( ph -> K ~<_ _om )
	saliuncl.b	|- ( ( ph /\ k e. K ) -> E e. S )
Assertion	saliuncl	|- ( ph -> U_ k e. K E e. S )

Proof

Step	Hyp	Ref	Expression
1		saliuncl.s	|- ( ph -> S e. SAlg )
2		saliuncl.kct	|- ( ph -> K ~<_ _om )
3		saliuncl.b	|- ( ( ph /\ k e. K ) -> E e. S )
4		nfv	|- F/ k ph
5		nfcv	|- F/_ k S
6		nfcv	|- F/_ k K
7	4 5 6 1 2 3	saliunclf	|- ( ph -> U_ k e. K E e. S )