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

Definition df-siga 26563
Description: Define a sigma-algebra, i.e. a set closed under complement and countable union. Litterature usually uses capital greek sigma and omega letters for the algebra set, and the base set respectively. We are using  S and  O as a parallel. (Contributed by Thierry Arnoux, 3-Sep-2016.)
Assertion
Ref Expression
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 ) ) ) } )
Distinct variable group:    o, s, x

Detailed syntax breakdown of Definition df-siga
StepHypRef Expression
1 csiga 26562 . 2  class sigAlgebra
2 vo . . 3  setvar  o
3 cvv 2984 . . 3  class  _V
4 vs . . . . . . 7  setvar  s
54cv 1368 . . . . . 6  class  s
62cv 1368 . . . . . . 7  class  o
76cpw 3872 . . . . . 6  class  ~P o
85, 7wss 3340 . . . . 5  wff  s  C_  ~P o
92, 4wel 1757 . . . . . 6  wff  o  e.  s
10 vx . . . . . . . . . 10  setvar  x
1110cv 1368 . . . . . . . . 9  class  x
126, 11cdif 3337 . . . . . . . 8  class  ( o 
\  x )
1312, 5wcel 1756 . . . . . . 7  wff  ( o 
\  x )  e.  s
1413, 10, 5wral 2727 . . . . . 6  wff  A. x  e.  s  ( o  \  x )  e.  s
15 com 6488 . . . . . . . . 9  class  om
16 cdom 7320 . . . . . . . . 9  class  ~<_
1711, 15, 16wbr 4304 . . . . . . . 8  wff  x  ~<_  om
1811cuni 4103 . . . . . . . . 9  class  U. x
1918, 5wcel 1756 . . . . . . . 8  wff  U. x  e.  s
2017, 19wi 4 . . . . . . 7  wff  ( x  ~<_  om  ->  U. x  e.  s )
215cpw 3872 . . . . . . 7  class  ~P s
2220, 10, 21wral 2727 . . . . . 6  wff  A. x  e.  ~P  s ( x  ~<_  om  ->  U. x  e.  s )
239, 14, 22w3a 965 . . . . 5  wff  ( o  e.  s  /\  A. x  e.  s  (
o  \  x )  e.  s  /\  A. x  e.  ~P  s ( x  ~<_  om  ->  U. x  e.  s ) )
248, 23wa 369 . . . 4  wff  ( 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 ) ) )
2524, 4cab 2429 . . 3  class  { 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 ) ) ) }
262, 3, 25cmpt 4362 . 2  class  ( 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 ) ) ) } )
271, 26wceq 1369 1  wff 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 ) ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  sigaval  26565  issiga  26566  isrnsigaOLD  26567  isrnsiga  26568
  Copyright terms: Public domain W3C validator