Description: SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | saliuncl.s | |
|
saliuncl.kct | |
||
saliuncl.b | |
||
Assertion | saliuncl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | saliuncl.s | |
|
2 | saliuncl.kct | |
|
3 | saliuncl.b | |
|
4 | 3 | ralrimiva | |
5 | dfiun3g | |
|
6 | 4 5 | syl | |
7 | eqid | |
|
8 | 7 | rnmptss | |
9 | 4 8 | syl | |
10 | 1 9 | ssexd | |
11 | elpwg | |
|
12 | 10 11 | syl | |
13 | 9 12 | mpbird | |
14 | 1stcrestlem | |
|
15 | 2 14 | syl | |
16 | 1 13 15 | salunicl | |
17 | 6 16 | eqeltrd | |