Metamath Proof Explorer


Theorem saliincl

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

Ref Expression
Hypotheses saliincl.s φSSAlg
saliincl.kct φKω
saliincl.kn0 φK
saliincl.e φkKES
Assertion saliincl φkKES

Proof

Step Hyp Ref Expression
1 saliincl.s φSSAlg
2 saliincl.kct φKω
3 saliincl.kn0 φK
4 saliincl.e φkKES
5 elssuni ESES
6 4 5 syl φkKES
7 df-ss ESES=E
8 6 7 sylib φkKES=E
9 8 eqcomd φkKE=ES
10 incom ES=SE
11 10 a1i φkKES=SE
12 dfin4 SE=SSE
13 12 a1i φkKSE=SSE
14 9 11 13 3eqtrd φkKE=SSE
15 14 iineq2dv φkKE=kKSSE
16 iindif2 KkKSSE=SkKSE
17 3 16 syl φkKSSE=SkKSE
18 15 17 eqtrd φkKE=SkKSE
19 1 adantr φkKSSAlg
20 saldifcl SSAlgESSES
21 19 4 20 syl2anc φkKSES
22 1 2 21 saliuncl φkKSES
23 saldifcl SSAlgkKSESSkKSES
24 1 22 23 syl2anc φSkKSES
25 18 24 eqeltrd φkKES