Metamath Proof Explorer


Theorem sigaclcu

Description: A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016)

Ref Expression
Assertion sigaclcu SransigAlgebraA𝒫SAωAS

Proof

Step Hyp Ref Expression
1 simp2 SransigAlgebraA𝒫SAωA𝒫S
2 isrnsiga SransigAlgebraSVoS𝒫ooSxSoxSx𝒫SxωxS
3 2 simprbi SransigAlgebraoS𝒫ooSxSoxSx𝒫SxωxS
4 simpr3 S𝒫ooSxSoxSx𝒫SxωxSx𝒫SxωxS
5 4 exlimiv oS𝒫ooSxSoxSx𝒫SxωxSx𝒫SxωxS
6 3 5 syl SransigAlgebrax𝒫SxωxS
7 6 3ad2ant1 SransigAlgebraA𝒫SAωx𝒫SxωxS
8 simp3 SransigAlgebraA𝒫SAωAω
9 breq1 x=AxωAω
10 unieq x=Ax=A
11 10 eleq1d x=AxSAS
12 9 11 imbi12d x=AxωxSAωAS
13 12 rspcv A𝒫Sx𝒫SxωxSAωAS
14 1 7 8 13 syl3c SransigAlgebraA𝒫SAωAS