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 28338
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 28337 . 2  class sigAlgebra
2 vo . . 3  setvar  o
3 cvv 3106 . . 3  class  _V
4 vs . . . . . . 7  setvar  s
54cv 1397 . . . . . 6  class  s
62cv 1397 . . . . . . 7  class  o
76cpw 3999 . . . . . 6  class  ~P o
85, 7wss 3461 . . . . 5  wff  s  C_  ~P o
92, 4wel 1824 . . . . . 6  wff  o  e.  s
10 vx . . . . . . . . . 10  setvar  x
1110cv 1397 . . . . . . . . 9  class  x
126, 11cdif 3458 . . . . . . . 8  class  ( o 
\  x )
1312, 5wcel 1823 . . . . . . 7  wff  ( o 
\  x )  e.  s
1413, 10, 5wral 2804 . . . . . 6  wff  A. x  e.  s  ( o  \  x )  e.  s
15 com 6673 . . . . . . . . 9  class  om
16 cdom 7507 . . . . . . . . 9  class  ~<_
1711, 15, 16wbr 4439 . . . . . . . 8  wff  x  ~<_  om
1811cuni 4235 . . . . . . . . 9  class  U. x
1918, 5wcel 1823 . . . . . . . 8  wff  U. x  e.  s
2017, 19wi 4 . . . . . . 7  wff  ( x  ~<_  om  ->  U. x  e.  s )
215cpw 3999 . . . . . . 7  class  ~P s
2220, 10, 21wral 2804 . . . . . 6  wff  A. x  e.  ~P  s ( x  ~<_  om  ->  U. x  e.  s )
239, 14, 22w3a 971 . . . . 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 367 . . . 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 2439 . . 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 4497 . 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 1398 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  28340  issiga  28341  isrnsigaOLD  28342  isrnsiga  28343
  Copyright terms: Public domain W3C validator