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	3	ralrimiva	|- ( ph -> A. k e. K E e. S )
5		dfiun3g	|- ( A. k e. K E e. S -> U_ k e. K E = U. ran ( k e. K |-> E ) )
6	4 5	syl	|- ( ph -> U_ k e. K E = U. ran ( k e. K |-> E ) )
7		eqid	|- ( k e. K |-> E ) = ( k e. K |-> E )
8	7	rnmptss	|- ( A. k e. K E e. S -> ran ( k e. K |-> E ) C_ S )
9	4 8	syl	|- ( ph -> ran ( k e. K |-> E ) C_ S )
10	1 9	ssexd	|- ( ph -> ran ( k e. K |-> E ) e. _V )
11		elpwg	|- ( ran ( k e. K |-> E ) e. _V -> ( ran ( k e. K |-> E ) e. ~P S <-> ran ( k e. K |-> E ) C_ S ) )
12	10 11	syl	|- ( ph -> ( ran ( k e. K |-> E ) e. ~P S <-> ran ( k e. K |-> E ) C_ S ) )
13	9 12	mpbird	|- ( ph -> ran ( k e. K |-> E ) e. ~P S )
14		1stcrestlem	|- ( K ~<_ _om -> ran ( k e. K |-> E ) ~<_ _om )
15	2 14	syl	|- ( ph -> ran ( k e. K |-> E ) ~<_ _om )
16	1 13 15	salunicl	|- ( ph -> U. ran ( k e. K |-> E ) e. S )
17	6 16	eqeltrd	|- ( ph -> U_ k e. K E e. S )