Metamath Proof Explorer


Theorem issal

Description: Express the predicate " S is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion issal SVSSAlgSySSySy𝒫SyωyS

Proof

Step Hyp Ref Expression
1 eleq2 x=SxS
2 id x=Sx=S
3 unieq x=Sx=S
4 3 difeq1d x=Sxy=Sy
5 4 2 eleq12d x=SxyxSyS
6 2 5 raleqbidv x=SyxxyxySSyS
7 pweq x=S𝒫x=𝒫S
8 eleq2 x=SyxyS
9 8 imbi2d x=SyωyxyωyS
10 7 9 raleqbidv x=Sy𝒫xyωyxy𝒫SyωyS
11 1 6 10 3anbi123d x=Sxyxxyxy𝒫xyωyxSySSySy𝒫SyωyS
12 df-salg SAlg=x|xyxxyxy𝒫xyωyx
13 11 12 elab2g SVSSAlgSySSySy𝒫SyωyS