Theorem saliunclf

Description: SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	saliunclf.1	|- F/ k ph
	saliunclf.2	|- F/_ k S
	saliunclf.3	|- F/_ k K
	saliunclf.4	|- ( ph -> S e. SAlg )
	saliunclf.5	|- ( ph -> K ~<_ _om )
	saliunclf.6	|- ( ( ph /\ k e. K ) -> E e. S )
Assertion	saliunclf	|- ( ph -> U_ k e. K E e. S )

Proof

Step	Hyp	Ref	Expression
1		saliunclf.1	|- F/ k ph
2		saliunclf.2	|- F/_ k S
3		saliunclf.3	|- F/_ k K
4		saliunclf.4	|- ( ph -> S e. SAlg )
5		saliunclf.5	|- ( ph -> K ~<_ _om )
6		saliunclf.6	|- ( ( ph /\ k e. K ) -> E e. S )
7	1 6	ralrimia	|- ( ph -> A. k e. K E e. S )
8		dfiun3g	|- ( A. k e. K E e. S -> U_ k e. K E = U. ran ( k e. K |-> E ) )
9	7 8	syl	|- ( ph -> U_ k e. K E = U. ran ( k e. K |-> E ) )
10		eqid	|- ( k e. K |-> E ) = ( k e. K |-> E )
11	1 3 2 10 6	rnmptssdff	|- ( ph -> ran ( k e. K |-> E ) C_ S )
12	4 11	sselpwd	|- ( ph -> ran ( k e. K |-> E ) e. ~P S )
13	3	rn1st	|- ( K ~<_ _om -> ran ( k e. K |-> E ) ~<_ _om )
14	5 13	syl	|- ( ph -> ran ( k e. K |-> E ) ~<_ _om )
15	4 12 14	salunicl	|- ( ph -> U. ran ( k e. K |-> E ) e. S )
16	9 15	eqeltrd	|- ( ph -> U_ k e. K E e. S )