Theorem saliinclf

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

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

Proof

Step	Hyp	Ref	Expression
1		saliinclf.1	|- F/ k ph
2		saliinclf.2	|- F/_ k S
3		saliinclf.3	|- F/_ k K
4		saliinclf.4	|- ( ph -> S e. SAlg )
5		saliinclf.5	|- ( ph -> K ~<_ _om )
6		saliinclf.6	|- ( ph -> K =/= (/) )
7		saliinclf.7	|- ( ( ph /\ k e. K ) -> E e. S )
8		incom	|- ( E i^i U. S ) = ( U. S i^i E )
9		elssuni	|- ( E e. S -> E C_ U. S )
10	7 9	syl	|- ( ( ph /\ k e. K ) -> E C_ U. S )
11		dfss2	|- ( E C_ U. S <-> ( E i^i U. S ) = E )
12	10 11	sylib	|- ( ( ph /\ k e. K ) -> ( E i^i U. S ) = E )
13		dfin4	|- ( U. S i^i E ) = ( U. S \ ( U. S \ E ) )
14	13	a1i	|- ( ( ph /\ k e. K ) -> ( U. S i^i E ) = ( U. S \ ( U. S \ E ) ) )
15	8 12 14	3eqtr3a	|- ( ( ph /\ k e. K ) -> E = ( U. S \ ( U. S \ E ) ) )
16	1 15	iineq2d	|- ( ph -> |^|_ k e. K E = |^|_ k e. K ( U. S \ ( U. S \ E ) ) )
17	2	nfuni	|- F/_ k U. S
18	3 17	iindif2f	|- ( K =/= (/) -> |^|_ k e. K ( U. S \ ( U. S \ E ) ) = ( U. S \ U_ k e. K ( U. S \ E ) ) )
19	6 18	syl	|- ( ph -> |^|_ k e. K ( U. S \ ( U. S \ E ) ) = ( U. S \ U_ k e. K ( U. S \ E ) ) )
20	16 19	eqtrd	|- ( ph -> |^|_ k e. K E = ( U. S \ U_ k e. K ( U. S \ E ) ) )
21		saldifcl	|- ( ( S e. SAlg /\ E e. S ) -> ( U. S \ E ) e. S )
22	4 7 21	syl2an2r	|- ( ( ph /\ k e. K ) -> ( U. S \ E ) e. S )
23	1 2 3 4 5 22	saliunclf	|- ( ph -> U_ k e. K ( U. S \ E ) e. S )
24		saldifcl	|- ( ( S e. SAlg /\ U_ k e. K ( U. S \ E ) e. S ) -> ( U. S \ U_ k e. K ( U. S \ E ) ) e. S )
25	4 23 24	syl2anc	|- ( ph -> ( U. S \ U_ k e. K ( U. S \ E ) ) e. S )
26	20 25	eqeltrd	|- ( ph -> |^|_ k e. K E e. S )