Metamath Proof Explorer

Theorem issgon

Description: Property of being a sigma-algebra with a given base set, noting that the base set of a sigma-algebra is actually its union set. (Contributed by Thierry Arnoux, 24-Sep-2016) (Revised by Thierry Arnoux, 23-Oct-2016)

Ref Expression
Assertion issgon 
|- ( S e. ( sigAlgebra ` O ) <-> ( S e. U. ran sigAlgebra /\ O = U. S ) )

Proof

Step Hyp Ref Expression
1 fvssunirn 
 |-  ( sigAlgebra ` O ) C_ U. ran sigAlgebra
2 1 sseli 
 |-  ( S e. ( sigAlgebra ` O ) -> S e. U. ran sigAlgebra )
3 elex 
 |-  ( S e. ( sigAlgebra ` O ) -> S e. _V )
4 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 ) ) ) ) )
5 elpwuni 
 |-  ( O e. S -> ( S C_ ~P O <-> U. S = O ) )
6 5 biimpa 
 |-  ( ( O e. S /\ S C_ ~P O ) -> U. S = O )
7 ancom 
 |-  ( ( S C_ ~P O /\ O e. S ) <-> ( O e. S /\ S C_ ~P O ) )
8 eqcom 
 |-  ( O = U. S <-> U. S = O )
9 6 7 8 3imtr4i 
 |-  ( ( S C_ ~P O /\ O e. S ) -> O = U. S )
10 9 3ad2antr1 
 |-  ( ( 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 = U. S )
11 4 10 biimtrdi 
 |-  ( S e. _V -> ( S e. ( sigAlgebra ` O ) -> O = U. S ) )
12 3 11 mpcom 
 |-  ( S e. ( sigAlgebra ` O ) -> O = U. S )
13 2 12 jca 
 |-  ( S e. ( sigAlgebra ` O ) -> ( S e. U. ran sigAlgebra /\ O = U. S ) )
14 elex 
 |-  ( S e. U. ran sigAlgebra -> S e. _V )
15 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 ) ) ) ) )
16 15 simprbi 
 |-  ( S e. U. ran sigAlgebra -> 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 ) ) ) )
17 elpwuni 
 |-  ( o e. S -> ( S C_ ~P o <-> U. S = o ) )
18 17 biimpa 
 |-  ( ( o e. S /\ S C_ ~P o ) -> U. S = o )
19 ancom 
 |-  ( ( S C_ ~P o /\ o e. S ) <-> ( o e. S /\ S C_ ~P o ) )
20 eqcom 
 |-  ( o = U. S <-> U. S = o )
21 18 19 20 3imtr4i 
 |-  ( ( S C_ ~P o /\ o e. S ) -> o = U. S )
22 21 3ad2antr1 
 |-  ( ( 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 = U. S )
23 pweq 
 |-  ( o = U. S -> ~P o = ~P U. S )
24 23 sseq2d 
 |-  ( o = U. S -> ( S C_ ~P o <-> S C_ ~P U. S ) )
25 eleq1 
 |-  ( o = U. S -> ( o e. S <-> U. S e. S ) )
26 difeq1 
 |-  ( o = U. S -> ( o \ x ) = ( U. S \ x ) )
27 26 eleq1d 
 |-  ( o = U. S -> ( ( o \ x ) e. S <-> ( U. S \ x ) e. S ) )
28 27 ralbidv 
 |-  ( o = U. S -> ( A. x e. S ( o \ x ) e. S <-> A. x e. S ( U. S \ x ) e. S ) )
29 25 28 3anbi12d 
 |-  ( o = U. S -> ( ( o e. S /\ A. x e. S ( o \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) <-> ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
30 24 29 anbi12d 
 |-  ( o = U. 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 U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) ) )
31 22 30 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 ) ) ) -> ( ( 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 U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) ) )
32 31 ibi 
 |-  ( ( 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 U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
33 32 exlimiv 
 |-  ( 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 ) ) ) -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
34 16 33 syl 
 |-  ( S e. U. ran sigAlgebra -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
35 34 simprd 
 |-  ( S e. U. ran sigAlgebra -> ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
36 14 35 jca 
 |-  ( S e. U. ran sigAlgebra -> ( S e. _V /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
37 eleq1 
 |-  ( O = U. S -> ( O e. S <-> U. S e. S ) )
38 difeq1 
 |-  ( O = U. S -> ( O \ x ) = ( U. S \ x ) )
39 38 eleq1d 
 |-  ( O = U. S -> ( ( O \ x ) e. S <-> ( U. S \ x ) e. S ) )
40 39 ralbidv 
 |-  ( O = U. S -> ( A. x e. S ( O \ x ) e. S <-> A. x e. S ( U. S \ x ) e. S ) )
41 37 40 3anbi12d 
 |-  ( O = U. S -> ( ( O e. S /\ A. x e. S ( O \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) <-> ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
42 41 biimprd 
 |-  ( O = U. S -> ( ( U. S e. S /\ A. x e. S ( U. S \ 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 ) ) ) )
43 pwuni 
 |-  S C_ ~P U. S
44 pweq 
 |-  ( O = U. S -> ~P O = ~P U. S )
45 43 44 sseqtrrid 
 |-  ( O = U. S -> S C_ ~P O )
46 42 45 jctild 
 |-  ( O = U. S -> ( ( U. S e. S /\ A. x e. S ( U. S \ 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 ) ) ) ) )
47 46 anim2d 
 |-  ( O = U. S -> ( ( S e. _V /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) -> ( 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 ) ) ) ) ) )
48 4 biimpar 
 |-  ( ( 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 ) ) ) ) -> S e. ( sigAlgebra ` O ) )
49 36 47 48 syl56 
 |-  ( O = U. S -> ( S e. U. ran sigAlgebra -> S e. ( sigAlgebra ` O ) ) )
50 49 impcom 
 |-  ( ( S e. U. ran sigAlgebra /\ O = U. S ) -> S e. ( sigAlgebra ` O ) )
51 13 50 impbii 
 |-  ( S e. ( sigAlgebra ` O ) <-> ( S e. U. ran sigAlgebra /\ O = U. S ) )