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 = (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)})

Distinct variable group:   𝑓,𝑔,𝑥

Detailed syntax breakdown of Definition df-ufil

Step	Hyp	Ref	Expression
1		cufil 21703	. 2 class UFil
2		vg	. . 3 setvar 𝑔
3		cvv 3200	. . 3 class V
4		vx	. . . . . . 7 setvar 𝑥
5		vf	. . . . . . 7 setvar 𝑓
6	4, 5	wel 1991	. . . . . 6 wff 𝑥 ∈ 𝑓
7	2	cv 1482	. . . . . . . 8 class 𝑔
8	4	cv 1482	. . . . . . . 8 class 𝑥
9	7, 8	cdif 3571	. . . . . . 7 class (𝑔 ∖ 𝑥)
10	5	cv 1482	. . . . . . 7 class 𝑓
11	9, 10	wcel 1990	. . . . . 6 wff (𝑔 ∖ 𝑥) ∈ 𝑓
12	6, 11	wo 383	. . . . 5 wff (𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)
13	7	cpw 4158	. . . . 5 class 𝒫 𝑔
14	12, 4, 13	wral 2912	. . . 4 wff ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)
15		cfil 21649	. . . . 5 class Fil
16	7, 15	cfv 5888	. . . 4 class (Fil‘𝑔)
17	14, 5, 16	crab 2916	. . 3 class {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)}
18	2, 3, 17	cmpt 4729	. 2 class (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)})
19	1, 18	wceq 1483	1 wff UFil = (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)})

This definition is referenced by:  isufil  21707