Metamath Proof Explorer


Theorem sigaex

Description: Lemma for issiga and isrnsiga . The class of sigma-algebras with base set o is a set. Note: a more generic version with ( O e. _V -> ... ) could be useful for sigaval . (Contributed by Thierry Arnoux, 24-Oct-2016)

Ref Expression
Assertion sigaex s|s𝒫oosxsoxsx𝒫sxωxsV

Proof

Step Hyp Ref Expression
1 df-rab s𝒫𝒫o|osxsoxsx𝒫sxωxs=s|s𝒫𝒫oosxsoxsx𝒫sxωxs
2 velpw s𝒫𝒫os𝒫o
3 2 anbi1i s𝒫𝒫oosxsoxsx𝒫sxωxss𝒫oosxsoxsx𝒫sxωxs
4 3 abbii s|s𝒫𝒫oosxsoxsx𝒫sxωxs=s|s𝒫oosxsoxsx𝒫sxωxs
5 1 4 eqtri s𝒫𝒫o|osxsoxsx𝒫sxωxs=s|s𝒫oosxsoxsx𝒫sxωxs
6 vex oV
7 pwexg oV𝒫oV
8 pwexg 𝒫oV𝒫𝒫oV
9 6 7 8 mp2b 𝒫𝒫oV
10 9 rabex s𝒫𝒫o|osxsoxsx𝒫sxωxsV
11 5 10 eqeltrri s|s𝒫oosxsoxsx𝒫sxωxsV