Definition df-ufil 21705

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

Step	Hyp	Ref	Expression
1		cufil 21703	. 2 class UFil
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vx	. . . . . . 7 setvar x
5		vf	. . . . . . 7 setvar f
6	4, 5	wel 1991	. . . . . 6 wff x e. f
7	2	cv 1482	. . . . . . . 8 class g
8	4	cv 1482	. . . . . . . 8 class x
9	7, 8	cdif 3571	. . . . . . 7 class ( g \ x )
10	5	cv 1482	. . . . . . 7 class f
11	9, 10	wcel 1990	. . . . . 6 wff ( g \ x ) e. f
12	6, 11	wo 383	. . . . 5 wff ( x e. f \/ ( g \ x ) e. f )
13	7	cpw 4158	. . . . 5 class ~P g
14	12, 4, 13	wral 2912	. . . 4 wff A. x e. ~P g ( x e. f \/ ( g \ x ) e. f )
15		cfil 21649	. . . . 5 class Fil
16	7, 15	cfv 5888	. . . 4 class ( Fil ` g )
17	14, 5, 16	crab 2916	. . 3 class { f e. ( Fil ` g ) | A. x e. ~P g ( x e. f \/ ( g \ x ) e. f ) }
18	2, 3, 17	cmpt 4729	. 2 class ( g e. _V |-> { f e. ( Fil ` g ) | A. x e. ~P g ( x e. f \/ ( g \ x ) e. f ) } )
19	1, 18	wceq 1483	1 wff UFil = ( g e. _V |-> { f e. ( Fil ` g ) | A. x e. ~P g ( x e. f \/ ( g \ x ) e. f ) } )

This definition is referenced by:  isufil  21707