MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ufil Unicode version

Definition df-ufil 17612
Description: Define the set of ultrafilters on a set. An ultrafilter is a filter that gives a definite result for every subset. (Contributed by Jeff Hankins, 30-Nov-2009.)
Assertion
Ref Expression
df-ufil  |-  UFil  =  ( g  e.  _V  |->  { f  e.  ( Fil `  g )  |  A. x  e. 
~P  g ( x  e.  f  \/  (
g  \  x )  e.  f ) } )
Distinct variable group:    f, g, x

Detailed syntax breakdown of Definition df-ufil
StepHypRef Expression
1 cufil 17610 . 2  class  UFil
2 vg . . 3  set  g
3 cvv 2801 . . 3  class  _V
4 vx . . . . . . 7  set  x
5 vf . . . . . . 7  set  f
64, 5wel 1697 . . . . . 6  wff  x  e.  f
72cv 1631 . . . . . . . 8  class  g
84cv 1631 . . . . . . . 8  class  x
97, 8cdif 3162 . . . . . . 7  class  ( g 
\  x )
105cv 1631 . . . . . . 7  class  f
119, 10wcel 1696 . . . . . 6  wff  ( g 
\  x )  e.  f
126, 11wo 357 . . . . 5  wff  ( x  e.  f  \/  (
g  \  x )  e.  f )
137cpw 3638 . . . . 5  class  ~P g
1412, 4, 13wral 2556 . . . 4  wff  A. x  e.  ~P  g ( x  e.  f  \/  (
g  \  x )  e.  f )
15 cfil 17556 . . . . 5  class  Fil
167, 15cfv 5271 . . . 4  class  ( Fil `  g )
1714, 5, 16crab 2560 . . 3  class  { f  e.  ( Fil `  g
)  |  A. x  e.  ~P  g ( x  e.  f  \/  (
g  \  x )  e.  f ) }
182, 3, 17cmpt 4093 . 2  class  ( g  e.  _V  |->  { f  e.  ( Fil `  g
)  |  A. x  e.  ~P  g ( x  e.  f  \/  (
g  \  x )  e.  f ) } )
191, 18wceq 1632 1  wff  UFil  =  ( g  e.  _V  |->  { f  e.  ( Fil `  g )  |  A. x  e. 
~P  g ( x  e.  f  \/  (
g  \  x )  e.  f ) } )
Colors of variables: wff set class
This definition is referenced by:  isufil  17614
  Copyright terms: Public domain W3C validator