Definition df-ufil

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)

	Ref	Expression
Assertion	df-ufil	|- UFil = ( g e. _V |-> { f e. ( Fil ` g ) | A. x e. ~P g ( x e. f \/ ( g \ x ) e. f ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cufil	|- UFil
1		vg	|- g
2		cvv	|- _V
3		vf	|- f
4		cfil	|- Fil
5	1	cv	|- g
6	5 4	cfv	|- ( Fil ` g )
7		vx	|- x
8	5	cpw	|- ~P g
9	7	cv	|- x
10	3	cv	|- f
11	9 10	wcel	|- x e. f
12	5 9	cdif	|- ( g \ x )
13	12 10	wcel	|- ( g \ x ) e. f
14	11 13	wo	|- ( x e. f \/ ( g \ x ) e. f )
15	14 7 8	wral	|- A. x e. ~P g ( x e. f \/ ( g \ x ) e. f )
16	15 3 6	crab	|- { f e. ( Fil ` g ) | A. x e. ~P g ( x e. f \/ ( g \ x ) e. f ) }
17	1 2 16	cmpt	|- ( g e. _V |-> { f e. ( Fil ` g ) | A. x e. ~P g ( x e. f \/ ( g \ x ) e. f ) } )
18	0 17	wceq	|- UFil = ( g e. _V |-> { f e. ( Fil ` g ) | A. x e. ~P g ( x e. f \/ ( g \ x ) e. f ) } )