Metamath Proof Explorer

Theorem sigaval

Description: The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016)

Ref Expression
Assertion sigaval 
|- ( O e. _V -> ( sigAlgebra ` O ) = { s | ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } )

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { s e. ~P ~P O | ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) } = { s | ( s e. ~P ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) }
2 velpw 
 |-  ( s e. ~P ~P O <-> s C_ ~P O )
3 2 anbi1i 
 |-  ( ( s e. ~P ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) <-> ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) )
4 3 abbii 
 |-  { s | ( s e. ~P ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } = { s | ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) }
5 1 4 eqtri 
 |-  { s e. ~P ~P O | ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) } = { s | ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) }
6 pwexg 
 |-  ( O e. _V -> ~P O e. _V )
7 pwexg 
 |-  ( ~P O e. _V -> ~P ~P O e. _V )
8 rabexg 
 |-  ( ~P ~P O e. _V -> { s e. ~P ~P O | ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) } e. _V )
9 6 7 8 3syl 
 |-  ( O e. _V -> { s e. ~P ~P O | ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) } e. _V )
10 5 9 eqeltrrid 
 |-  ( O e. _V -> { s | ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } e. _V )
11 pweq 
 |-  ( o = O -> ~P o = ~P O )
12 11 sseq2d 
 |-  ( o = O -> ( s C_ ~P o <-> s C_ ~P O ) )
13 eleq1 
 |-  ( o = O -> ( o e. s <-> O e. s ) )
14 difeq1 
 |-  ( o = O -> ( o \ x ) = ( O \ x ) )
15 14 eleq1d 
 |-  ( o = O -> ( ( o \ x ) e. s <-> ( O \ x ) e. s ) )
16 15 ralbidv 
 |-  ( o = O -> ( A. x e. s ( o \ x ) e. s <-> A. x e. s ( O \ x ) e. s ) )
17 13 16 3anbi12d 
 |-  ( o = O -> ( ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) <-> ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) )
18 12 17 anbi12d 
 |-  ( o = O -> ( ( s C_ ~P o /\ ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) <-> ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) ) )
19 18 abbidv 
 |-  ( o = O -> { s | ( s C_ ~P o /\ ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } = { s | ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } )
20 df-siga 
 |-  sigAlgebra = ( o e. _V |-> { s | ( s C_ ~P o /\ ( o e. s /\ A. x e. s ( o \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } )
21 19 20 fvmptg 
 |-  ( ( O e. _V /\ { s | ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } e. _V ) -> ( sigAlgebra ` O ) = { s | ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } )
22 10 21 mpdan 
 |-  ( O e. _V -> ( sigAlgebra ` O ) = { s | ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) ) } )