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 28944
Description: Define a sigma-algebra, i.e. a set closed under complement and countable union. Literature 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 28943 . 2  class sigAlgebra
2 vo . . 3  setvar  o
3 cvv 3085 . . 3  class  _V
4 vs . . . . . . 7  setvar  s
54cv 1437 . . . . . 6  class  s
62cv 1437 . . . . . . 7  class  o
76cpw 3987 . . . . . 6  class  ~P o
85, 7wss 3442 . . . . 5  wff  s  C_  ~P o
92, 4wel 1874 . . . . . 6  wff  o  e.  s
10 vx . . . . . . . . . 10  setvar  x
1110cv 1437 . . . . . . . . 9  class  x
126, 11cdif 3439 . . . . . . . 8  class  ( o 
\  x )
1312, 5wcel 1873 . . . . . . 7  wff  ( o 
\  x )  e.  s
1413, 10, 5wral 2776 . . . . . 6  wff  A. x  e.  s  ( o  \  x )  e.  s
15 com 6712 . . . . . . . . 9  class  om
16 cdom 7584 . . . . . . . . 9  class  ~<_
1711, 15, 16wbr 4429 . . . . . . . 8  wff  x  ~<_  om
1811cuni 4225 . . . . . . . . 9  class  U. x
1918, 5wcel 1873 . . . . . . . 8  wff  U. x  e.  s
2017, 19wi 4 . . . . . . 7  wff  ( x  ~<_  om  ->  U. x  e.  s )
215cpw 3987 . . . . . . 7  class  ~P s
2220, 10, 21wral 2776 . . . . . 6  wff  A. x  e.  ~P  s ( x  ~<_  om  ->  U. x  e.  s )
239, 14, 22w3a 983 . . . . 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 371 . . . 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 2408 . . 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 4488 . 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 1438 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  28946  issiga  28947  isrnsigaOLD  28948  isrnsiga  28949
  Copyright terms: Public domain W3C validator