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

Theorem issgon 27948
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 5895 . . . 4  |-  (sigAlgebra `  O
)  C_  U. ran sigAlgebra
21sseli 3505 . . 3  |-  ( S  e.  (sigAlgebra `  O )  ->  S  e.  U. ran sigAlgebra )
3 elex 3127 . . . 4  |-  ( S  e.  (sigAlgebra `  O )  ->  S  e.  _V )
4 issiga 27936 . . . . 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 4419 . . . . . . . 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 2476 . . . . . . 7  |-  ( O  =  U. S  <->  U. S  =  O )
96, 7, 83imtr4i 266 . . . . . 6  |-  ( ( S  C_  ~P O  /\  O  e.  S
)  ->  O  =  U. S )
1093ad2antr1 1161 . . . . 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 3127 . . . . 5  |-  ( S  e.  U. ran sigAlgebra  ->  S  e.  _V )
15 isrnsiga 27938 . . . . . . . 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 4419 . . . . . . . . . . . . 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 2476 . . . . . . . . . . . 12  |-  ( o  =  U. S  <->  U. S  =  o )
2118, 19, 203imtr4i 266 . . . . . . . . . . 11  |-  ( ( S  C_  ~P o  /\  o  e.  S
)  ->  o  =  U. S )
22213ad2antr1 1161 . . . . . . . . . 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 4019 . . . . . . . . . . . 12  |-  ( o  =  U. S  ->  ~P o  =  ~P U. S )
2423sseq2d 3537 . . . . . . . . . . 11  |-  ( o  =  U. S  -> 
( S  C_  ~P o 
<->  S  C_  ~P U. S
) )
25 eleq1 2539 . . . . . . . . . . . 12  |-  ( o  =  U. S  -> 
( o  e.  S  <->  U. S  e.  S ) )
26 difeq1 3620 . . . . . . . . . . . . . 14  |-  ( o  =  U. S  -> 
( o  \  x
)  =  ( U. S  \  x ) )
2726eleq1d 2536 . . . . . . . . . . . . 13  |-  ( o  =  U. S  -> 
( ( o  \  x )  e.  S  <->  ( U. S  \  x
)  e.  S ) )
2827ralbidv 2906 . . . . . . . . . . . 12  |-  ( o  =  U. S  -> 
( A. x  e.  S  ( o  \  x )  e.  S  <->  A. x  e.  S  ( U. S  \  x
)  e.  S ) )
2925, 283anbi12d 1300 . . . . . . . . . . 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 1698 . . . . . . 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 2539 . . . . . . . 8  |-  ( O  =  U. S  -> 
( O  e.  S  <->  U. S  e.  S ) )
38 difeq1 3620 . . . . . . . . . 10  |-  ( O  =  U. S  -> 
( O  \  x
)  =  ( U. S  \  x ) )
3938eleq1d 2536 . . . . . . . . 9  |-  ( O  =  U. S  -> 
( ( O  \  x )  e.  S  <->  ( U. S  \  x
)  e.  S ) )
4039ralbidv 2906 . . . . . . . 8  |-  ( O  =  U. S  -> 
( A. x  e.  S  ( O  \  x )  e.  S  <->  A. x  e.  S  ( U. S  \  x
)  e.  S ) )
4137, 403anbi12d 1300 . . . . . . 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 4684 . . . . . . 7  |-  S  C_  ~P U. S
44 pweq 4019 . . . . . . 7  |-  ( O  =  U. S  ->  ~P O  =  ~P U. S )
4543, 44syl5sseqr 3558 . . . . . 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 973    = wceq 1379   E.wex 1596    e. wcel 1767   A.wral 2817   _Vcvv 3118    \ cdif 3478    C_ wss 3481   ~Pcpw 4016   U.cuni 4251   class class class wbr 4453   ran crn 5006   ` cfv 5594   omcom 6695    ~<_ cdom 7526  sigAlgebracsiga 27932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-fv 5602  df-siga 27933
This theorem is referenced by:  sgon  27949  unisg  27968  sxsigon  27988  sxuni  27989  1stmbfm  28056  2ndmbfm  28057  mbfmvolf  28062
  Copyright terms: Public domain W3C validator