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

Definition df-ufil 17926
 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-ufil
StepHypRef Expression
1 cufil 17924 . 2
2 vg . . 3
3 cvv 2949 . . 3
4 vx . . . . . . 7
5 vf . . . . . . 7
64, 5wel 1726 . . . . . 6
72cv 1651 . . . . . . . 8
84cv 1651 . . . . . . . 8
97, 8cdif 3310 . . . . . . 7
105cv 1651 . . . . . . 7
119, 10wcel 1725 . . . . . 6
126, 11wo 358 . . . . 5
137cpw 3792 . . . . 5
1412, 4, 13wral 2698 . . . 4
15 cfil 17870 . . . . 5
167, 15cfv 5447 . . . 4
1714, 5, 16crab 2702 . . 3
182, 3, 17cmpt 4259 . 2
191, 18wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  isufil  17928
 Copyright terms: Public domain W3C validator