Metamath Proof Explorer

Theorem issiga

Description: An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016)

Ref Expression
Assertion issiga 
|- ( S e. _V -> ( S e. ( sigAlgebra ` 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 elfvex 
 |-  ( S e. ( sigAlgebra ` O ) -> O e. _V )
2 elex 
 |-  ( S e. ( sigAlgebra ` O ) -> S e. _V )
3 1 2 jca 
 |-  ( S e. ( sigAlgebra ` O ) -> ( O e. _V /\ S e. _V ) )
4 3 a1i 
 |-  ( S e. _V -> ( S e. ( sigAlgebra ` O ) -> ( O e. _V /\ S e. _V ) ) )
5 simpr1 
 |-  ( ( 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 ) ) ) -> O e. S )
6 elex 
 |-  ( O e. S -> O e. _V )
7 5 6 syl 
 |-  ( ( 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 ) ) ) -> O e. _V )
8 7 a1i 
 |-  ( S 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 ) ) ) -> O e. _V ) )
9 8 anc2ri 
 |-  ( S 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 ) ) ) -> ( O e. _V /\ S e. _V ) ) )
10 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 ) ) ) } )
11 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
12 pweq 
 |-  ( o = O -> ~P o = ~P O )
13 12 sseq2d 
 |-  ( o = O -> ( s C_ ~P o <-> s C_ ~P O ) )
14 sseq1 
 |-  ( s = S -> ( s C_ ~P O <-> S C_ ~P O ) )
15 13 14 sylan9bb 
 |-  ( ( o = O /\ s = S ) -> ( s C_ ~P o <-> S C_ ~P O ) )
16 eleq12 
 |-  ( ( o = O /\ s = S ) -> ( o e. s <-> O e. S ) )
17 simpr 
 |-  ( ( o = O /\ s = S ) -> s = S )
18 difeq1 
 |-  ( o = O -> ( o \ x ) = ( O \ x ) )
19 18 adantr 
 |-  ( ( o = O /\ s = S ) -> ( o \ x ) = ( O \ x ) )
20 19 eleq1d 
 |-  ( ( o = O /\ s = S ) -> ( ( o \ x ) e. s <-> ( O \ x ) e. s ) )
21 eleq2 
 |-  ( s = S -> ( ( O \ x ) e. s <-> ( O \ x ) e. S ) )
22 21 adantl 
 |-  ( ( o = O /\ s = S ) -> ( ( O \ x ) e. s <-> ( O \ x ) e. S ) )
23 20 22 bitrd 
 |-  ( ( o = O /\ s = S ) -> ( ( o \ x ) e. s <-> ( O \ x ) e. S ) )
24 17 23 raleqbidv 
 |-  ( ( o = O /\ s = S ) -> ( A. x e. s ( o \ x ) e. s <-> A. x e. S ( O \ x ) e. S ) )
25 pweq 
 |-  ( s = S -> ~P s = ~P S )
26 eleq2 
 |-  ( s = S -> ( U. x e. s <-> U. x e. S ) )
27 26 imbi2d 
 |-  ( s = S -> ( ( x ~<_ _om -> U. x e. s ) <-> ( x ~<_ _om -> U. x e. S ) ) )
28 25 27 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 ) ) )
29 28 adantl 
 |-  ( ( o = O /\ s = S ) -> ( A. x e. ~P s ( x ~<_ _om -> U. x e. s ) <-> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
30 16 24 29 3anbi123d 
 |-  ( ( o = O /\ 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 ) ) ) )
31 15 30 anbi12d 
 |-  ( ( o = O /\ 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 ) ) ) ) )
32 10 11 31 abfmpel 
 |-  ( ( O e. _V /\ S e. _V ) -> ( S e. ( sigAlgebra ` 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 ) ) ) ) )
33 32 a1i 
 |-  ( S e. _V -> ( ( O e. _V /\ S e. _V ) -> ( S e. ( sigAlgebra ` 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 ) ) ) ) ) )
34 4 9 33 pm5.21ndd 
 |-  ( S e. _V -> ( S e. ( sigAlgebra ` 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 ) ) ) ) )