Description: SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | saliincl.s | |
|
saliincl.kct | |
||
saliincl.kn0 | |
||
saliincl.e | |
||
Assertion | saliincl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | saliincl.s | |
|
2 | saliincl.kct | |
|
3 | saliincl.kn0 | |
|
4 | saliincl.e | |
|
5 | elssuni | |
|
6 | 4 5 | syl | |
7 | df-ss | |
|
8 | 6 7 | sylib | |
9 | 8 | eqcomd | |
10 | incom | |
|
11 | 10 | a1i | |
12 | dfin4 | |
|
13 | 12 | a1i | |
14 | 9 11 13 | 3eqtrd | |
15 | 14 | iineq2dv | |
16 | iindif2 | |
|
17 | 3 16 | syl | |
18 | 15 17 | eqtrd | |
19 | 1 | adantr | |
20 | saldifcl | |
|
21 | 19 4 20 | syl2anc | |
22 | 1 2 21 | saliuncl | |
23 | saldifcl | |
|
24 | 1 22 23 | syl2anc | |
25 | 18 24 | eqeltrd | |