Metamath Proof Explorer

Theorem isrnsiga

Description: The property of being a sigma-algebra on an indefinite base set. (Contributed by Thierry Arnoux, 3-Sep-2016) (Proof shortened by Thierry Arnoux, 23-Oct-2016)

Ref Expression
Assertion isrnsiga 
|- ( S e. U. ran sigAlgebra <-> ( S e. _V /\ E. 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) } )
2 sigaex 
 |-  { 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
3 sseq1 
 |-  ( s = S -> ( s C_ ~P o <-> S C_ ~P o ) )
4 eleq2 
 |-  ( s = S -> ( o e. s <-> o e. S ) )
5 eleq2 
 |-  ( s = S -> ( ( o \ x ) e. s <-> ( o \ x ) e. S ) )
6 5 raleqbi1dv 
 |-  ( s = S -> ( A. x e. s ( o \ x ) e. s <-> A. x e. S ( o \ x ) e. S ) )
7 pweq 
 |-  ( s = S -> ~P s = ~P S )
8 eleq2 
 |-  ( s = S -> ( U. x e. s <-> U. x e. S ) )
9 8 imbi2d 
 |-  ( s = S -> ( ( x ~<_ _om -> U. x e. s ) <-> ( x ~<_ _om -> U. x e. S ) ) )
10 7 9 raleqbidv 
 |-  ( s = S -> ( A. x e. ~P s ( x ~<_ _om -> U. x e. s ) <-> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
11 4 6 10 3anbi123d 
 |-  ( s = S -> ( ( 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 ) ) ) )
12 3 11 anbi12d 
 |-  ( 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 ) ) ) <-> ( 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 ) ) ) ) )
13 1 2 12 abfmpunirn 
 |-  ( S e. U. ran sigAlgebra <-> ( S e. _V /\ E. o e. _V ( 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 ) ) ) ) )
14 rexv 
 |-  ( E. o e. _V ( 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. 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 ) ) ) )
15 14 anbi2i 
 |-  ( ( S e. _V /\ E. o e. _V ( 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 e. _V /\ E. 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 ) ) ) ) )
16 13 15 bitri 
 |-  ( S e. U. ran sigAlgebra <-> ( S e. _V /\ E. 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 ) ) ) ) )