Metamath Proof Explorer


Theorem 0elsiga

Description: A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016)

Ref Expression
Assertion 0elsiga SransigAlgebraS

Proof

Step Hyp Ref Expression
1 isrnsiga SransigAlgebraSVoS𝒫ooSxSoxSx𝒫SxωxS
2 1 simprbi SransigAlgebraoS𝒫ooSxSoxSx𝒫SxωxS
3 3simpa oSxSoxSx𝒫SxωxSoSxSoxS
4 3 adantl S𝒫ooSxSoxSx𝒫SxωxSoSxSoxS
5 4 eximi oS𝒫ooSxSoxSx𝒫SxωxSooSxSoxS
6 difeq2 x=oox=oo
7 difid oo=
8 6 7 eqtrdi x=oox=
9 8 eleq1d x=ooxSS
10 9 rspcva oSxSoxSS
11 10 exlimiv ooSxSoxSS
12 2 5 11 3syl SransigAlgebraS