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

Definition df-ufil 17596
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 17594 . 2  class  UFil
2 vg . . 3  set  g
3 cvv 2788 . . 3  class  _V
4 vx . . . . . . 7  set  x
5 vf . . . . . . 7  set  f
64, 5wel 1685 . . . . . 6  wff  x  e.  f
72cv 1622 . . . . . . . 8  class  g
84cv 1622 . . . . . . . 8  class  x
97, 8cdif 3149 . . . . . . 7  class  ( g 
\  x )
105cv 1622 . . . . . . 7  class  f
119, 10wcel 1684 . . . . . 6  wff  ( g 
\  x )  e.  f
126, 11wo 357 . . . . 5  wff  ( x  e.  f  \/  (
g  \  x )  e.  f )
137cpw 3625 . . . . 5  class  ~P g
1412, 4, 13wral 2543 . . . 4  wff  A. x  e.  ~P  g ( x  e.  f  \/  (
g  \  x )  e.  f )
15 cfil 17540 . . . . 5  class  Fil
167, 15cfv 5255 . . . 4  class  ( Fil `  g )
1714, 5, 16crab 2547 . . 3  class  { f  e.  ( Fil `  g
)  |  A. x  e.  ~P  g ( x  e.  f  \/  (
g  \  x )  e.  f ) }
182, 3, 17cmpt 4077 . 2  class  ( g  e.  _V  |->  { f  e.  ( Fil `  g
)  |  A. x  e.  ~P  g ( x  e.  f  \/  (
g  \  x )  e.  f ) } )
191, 18wceq 1623 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  17598
  Copyright terms: Public domain W3C validator