Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  issgon Structured version   Unicode version

Theorem issgon 26734
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.)
Assertion
Ref Expression
issgon  |-  ( S  e.  (sigAlgebra `  O )  <->  ( S  e.  U. ran sigAlgebra  /\  O  = 
U. S ) )

Proof of Theorem issgon
Dummy variables  x  o are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvssunirn 5825 . . . 4  |-  (sigAlgebra `  O
)  C_  U. ran sigAlgebra
21sseli 3463 . . 3  |-  ( S  e.  (sigAlgebra `  O )  ->  S  e.  U. ran sigAlgebra )
3 elex 3087 . . . 4  |-  ( S  e.  (sigAlgebra `  O )  ->  S  e.  _V )
4 issiga 26722 . . . . 5  |-  ( 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 4369 . . . . . . . 8  |-  ( O  e.  S  ->  ( S  C_  ~P O  <->  U. S  =  O ) )
65biimpa 484 . . . . . . 7  |-  ( ( O  e.  S  /\  S  C_  ~P O )  ->  U. S  =  O )
7 ancom 450 . . . . . . 7  |-  ( ( S  C_  ~P O  /\  O  e.  S
)  <->  ( O  e.  S  /\  S  C_  ~P O ) )
8 eqcom 2463 . . . . . . 7  |-  ( O  =  U. S  <->  U. S  =  O )
96, 7, 83imtr4i 266 . . . . . 6  |-  ( ( S  C_  ~P O  /\  O  e.  S
)  ->  O  =  U. S )
1093ad2antr1 1153 . . . . 5  |-  ( ( 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 )
114, 10syl6bi 228 . . . 4  |-  ( S  e.  _V  ->  ( S  e.  (sigAlgebra `  O
)  ->  O  =  U. S ) )
123, 11mpcom 36 . . 3  |-  ( S  e.  (sigAlgebra `  O )  ->  O  =  U. S )
132, 12jca 532 . 2  |-  ( S  e.  (sigAlgebra `  O )  -> 
( S  e.  U. ran sigAlgebra  /\  O  =  U. S ) )
14 elex 3087 . . . . 5  |-  ( S  e.  U. ran sigAlgebra  ->  S  e.  _V )
15 isrnsiga 26724 . . . . . . . 8  |-  ( 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
) ) ) ) )
1615simprbi 464 . . . . . . 7  |-  ( 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 4369 . . . . . . . . . . . . 13  |-  ( o  e.  S  ->  ( S  C_  ~P o  <->  U. S  =  o ) )
1817biimpa 484 . . . . . . . . . . . 12  |-  ( ( o  e.  S  /\  S  C_  ~P o )  ->  U. S  =  o )
19 ancom 450 . . . . . . . . . . . 12  |-  ( ( S  C_  ~P o  /\  o  e.  S
)  <->  ( o  e.  S  /\  S  C_  ~P o ) )
20 eqcom 2463 . . . . . . . . . . . 12  |-  ( o  =  U. S  <->  U. S  =  o )
2118, 19, 203imtr4i 266 . . . . . . . . . . 11  |-  ( ( S  C_  ~P o  /\  o  e.  S
)  ->  o  =  U. S )
22213ad2antr1 1153 . . . . . . . . . 10  |-  ( ( 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 3974 . . . . . . . . . . . 12  |-  ( o  =  U. S  ->  ~P o  =  ~P U. S )
2423sseq2d 3495 . . . . . . . . . . 11  |-  ( o  =  U. S  -> 
( S  C_  ~P o 
<->  S  C_  ~P U. S
) )
25 eleq1 2526 . . . . . . . . . . . 12  |-  ( o  =  U. S  -> 
( o  e.  S  <->  U. S  e.  S ) )
26 difeq1 3578 . . . . . . . . . . . . . 14  |-  ( o  =  U. S  -> 
( o  \  x
)  =  ( U. S  \  x ) )
2726eleq1d 2523 . . . . . . . . . . . . 13  |-  ( o  =  U. S  -> 
( ( o  \  x )  e.  S  <->  ( U. S  \  x
)  e.  S ) )
2827ralbidv 2846 . . . . . . . . . . . 12  |-  ( o  =  U. S  -> 
( A. x  e.  S  ( o  \  x )  e.  S  <->  A. x  e.  S  ( U. S  \  x
)  e.  S ) )
2925, 283anbi12d 1291 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
3024, 29anbi12d 710 . . . . . . . . . 10  |-  ( 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 ) ) ) ) )
3122, 30syl 16 . . . . . . . . 9  |-  ( ( 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 ) ) ) ) )
3231ibi 241 . . . . . . . 8  |-  ( ( 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 ) ) ) )
3332exlimiv 1689 . . . . . . 7  |-  ( 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 ) ) ) )
3416, 33syl 16 . . . . . 6  |-  ( 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 ) ) ) )
3534simprd 463 . . . . 5  |-  ( 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 ) ) )
3614, 35jca 532 . . . 4  |-  ( 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 2526 . . . . . . . 8  |-  ( O  =  U. S  -> 
( O  e.  S  <->  U. S  e.  S ) )
38 difeq1 3578 . . . . . . . . . 10  |-  ( O  =  U. S  -> 
( O  \  x
)  =  ( U. S  \  x ) )
3938eleq1d 2523 . . . . . . . . 9  |-  ( O  =  U. S  -> 
( ( O  \  x )  e.  S  <->  ( U. S  \  x
)  e.  S ) )
4039ralbidv 2846 . . . . . . . 8  |-  ( O  =  U. S  -> 
( A. x  e.  S  ( O  \  x )  e.  S  <->  A. x  e.  S  ( U. S  \  x
)  e.  S ) )
4137, 403anbi12d 1291 . . . . . . 7  |-  ( 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 ) ) ) )
4241biimprd 223 . . . . . 6  |-  ( 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 4634 . . . . . . 7  |-  S  C_  ~P U. S
44 pweq 3974 . . . . . . 7  |-  ( O  =  U. S  ->  ~P O  =  ~P U. S )
4543, 44syl5sseqr 3516 . . . . . 6  |-  ( O  =  U. S  ->  S  C_  ~P O )
4642, 45jctild 543 . . . . 5  |-  ( 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
) ) ) ) )
4746anim2d 565 . . . 4  |-  ( 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 ) ) ) ) ) )
484biimpar 485 . . . 4  |-  ( ( 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
) )
4936, 47, 48syl56 34 . . 3  |-  ( O  =  U. S  -> 
( S  e.  U. ran sigAlgebra 
->  S  e.  (sigAlgebra `  O ) ) )
5049impcom 430 . 2  |-  ( ( S  e.  U. ran sigAlgebra  /\  O  =  U. S )  ->  S  e.  (sigAlgebra `  O ) )
5113, 50impbii 188 1  |-  ( S  e.  (sigAlgebra `  O )  <->  ( S  e.  U. ran sigAlgebra  /\  O  = 
U. S ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1370   E.wex 1587    e. wcel 1758   A.wral 2799   _Vcvv 3078    \ cdif 3436    C_ wss 3439   ~Pcpw 3971   U.cuni 4202   class class class wbr 4403   ran crn 4952   ` cfv 5529   omcom 6589    ~<_ cdom 7421  sigAlgebracsiga 26718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-fv 5537  df-siga 26719
This theorem is referenced by:  sgon  26735  unisg  26754  sxsigon  26774  sxuni  26775  1stmbfm  26842  2ndmbfm  26843  mbfmvolf  26848
  Copyright terms: Public domain W3C validator