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	$$⊢\mathrm{UFil}=\left(g\in \mathrm{V}⟼\left\{f\in \mathrm{Fil}\left(g\right)|\forall x\in 𝒫g\left(x\in f\vee g\setminus x\in f\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cufil	$$class\mathrm{UFil}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		cfil	$$class\mathrm{Fil}$$
5	1	cv	$$setvarg$$
6	5 4	cfv	$$class\mathrm{Fil}\left(g\right)$$
7		vx	$$setvarx$$
8	5	cpw	$$class𝒫g$$
9	7	cv	$$setvarx$$
10	3	cv	$$setvarf$$
11	9 10	wcel	$$wffx\in f$$
12	5 9	cdif	$$class\left(g\setminus x\right)$$
13	12 10	wcel	$$wffg\setminus x\in f$$
14	11 13	wo	$$wff\left(x\in f\vee g\setminus x\in f\right)$$
15	14 7 8	wral	$$wff\forall x\in 𝒫g\left(x\in f\vee g\setminus x\in f\right)$$
16	15 3 6	crab	$$class\left\{f\in \mathrm{Fil}\left(g\right)|\forall x\in 𝒫g\left(x\in f\vee g\setminus x\in f\right)\right\}$$
17	1 2 16	cmpt	$$class\left(g\in \mathrm{V}⟼\left\{f\in \mathrm{Fil}\left(g\right)|\forall x\in 𝒫g\left(x\in f\vee g\setminus x\in f\right)\right\}\right)$$
18	0 17	wceq	$$wff\mathrm{UFil}=\left(g\in \mathrm{V}⟼\left\{f\in \mathrm{Fil}\left(g\right)|\forall x\in 𝒫g\left(x\in f\vee g\setminus x\in f\right)\right\}\right)$$