Description: A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | sigaclcu | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 | |
|
2 | isrnsiga | |
|
3 | 2 | simprbi | |
4 | simpr3 | |
|
5 | 4 | exlimiv | |
6 | 3 5 | syl | |
7 | 6 | 3ad2ant1 | |
8 | simp3 | |
|
9 | breq1 | |
|
10 | unieq | |
|
11 | 10 | eleq1d | |
12 | 9 11 | imbi12d | |
13 | 12 | rspcv | |
14 | 1 7 8 13 | syl3c | |