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		elssuni	|- ( E e. S -> E C_ U. S )
6	4 5	syl	|- ( ( ph /\ k e. K ) -> E C_ U. S )
7		df-ss	|- ( E C_ U. S <-> ( E i^i U. S ) = E )
8	6 7	sylib	|- ( ( ph /\ k e. K ) -> ( E i^i U. S ) = E )
9	8	eqcomd	|- ( ( ph /\ k e. K ) -> E = ( E i^i U. S ) )
10		incom	|- ( E i^i U. S ) = ( U. S i^i E )
11	10	a1i	|- ( ( ph /\ k e. K ) -> ( E i^i U. S ) = ( U. S i^i E ) )
12		dfin4	|- ( U. S i^i E ) = ( U. S \ ( U. S \ E ) )
13	12	a1i	|- ( ( ph /\ k e. K ) -> ( U. S i^i E ) = ( U. S \ ( U. S \ E ) ) )
14	9 11 13	3eqtrd	|- ( ( ph /\ k e. K ) -> E = ( U. S \ ( U. S \ E ) ) )
15	14	iineq2dv	|- ( ph -> |^|_ k e. K E = |^|_ k e. K ( U. S \ ( U. S \ E ) ) )
16		iindif2	|- ( K =/= (/) -> |^|_ k e. K ( U. S \ ( U. S \ E ) ) = ( U. S \ U_ k e. K ( U. S \ E ) ) )
17	3 16	syl	|- ( ph -> |^|_ k e. K ( U. S \ ( U. S \ E ) ) = ( U. S \ U_ k e. K ( U. S \ E ) ) )
18	15 17	eqtrd	|- ( ph -> |^|_ k e. K E = ( U. S \ U_ k e. K ( U. S \ E ) ) )
19	1	adantr	|- ( ( ph /\ k e. K ) -> S e. SAlg )
20		saldifcl	|- ( ( S e. SAlg /\ E e. S ) -> ( U. S \ E ) e. S )
21	19 4 20	syl2anc	|- ( ( ph /\ k e. K ) -> ( U. S \ E ) e. S )
22	1 2 21	saliuncl	|- ( ph -> U_ k e. K ( U. S \ E ) e. S )
23		saldifcl	|- ( ( S e. SAlg /\ U_ k e. K ( U. S \ E ) e. S ) -> ( U. S \ U_ k e. K ( U. S \ E ) ) e. S )
24	1 22 23	syl2anc	|- ( ph -> ( U. S \ U_ k e. K ( U. S \ E ) ) e. S )
25	18 24	eqeltrd	|- ( ph -> |^|_ k e. K E e. S )