Definition df-ufil 16648

Description: Define the class of all ultrafilters.

Assertion

Ref	Expression
df-ufil	|- UFil = {f e. Fil | A.x e. ~P U.f(x e. f \/ (U.f \ x) e. f)}

Distinct variable group:   x,f

Detailed syntax breakdown of Definition df-ufil

Step	Hyp	Ref	Expression
1		cufil 16647	. 2 class UFil
2		vx	. . . . . . 7 set x
3	2	cv 1614	. . . . . 6 class x
4		vf	. . . . . . 7 set f
5	4	cv 1614	. . . . . 6 class f
6	3, 5	wcel 1617	. . . . 5 wff x e. f
7	5	cuni 3398	. . . . . . 7 class U.f
8	7, 3	cdif 2856	. . . . . 6 class (U.f \ x)
9	8, 5	wcel 1617	. . . . 5 wff (U.f \ x) e. f
10	6, 9	wo 432	. . . 4 wff (x e. f \/ (U.f \ x) e. f)
11	7	cpw 3259	. . . 4 class ~PU.f
12	10, 2, 11	wral 2385	. . 3 wff A.x e. ~P U.f(x e. f \/ (U.f \ x) e. f)
13		cfil 11260	. . 3 class Fil
14	12, 4, 13	crab 2388	. 2 class {f e. Fil | A.x e. ~P U.f(x e. f \/ (U.f \ x) e. f)}
15	1, 14	wceq 1615	1 wff UFil = {f e. Fil | A.x e. ~P U.f(x e. f \/ (U.f \ x) e. f)}

This definition is referenced by:  isufil 16649

Copyright terms: Public domain