Definition df-ufil 21515

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 21513	. 2 class UFil
2		vg	. . 3 setvar 𝑔
3		cvv 3173	. . 3 class V
4		vx	. . . . . . 7 setvar 𝑥
5		vf	. . . . . . 7 setvar 𝑓
6	4, 5	wel 1978	. . . . . 6 wff 𝑥 ∈ 𝑓
7	2	cv 1474	. . . . . . . 8 class 𝑔
8	4	cv 1474	. . . . . . . 8 class 𝑥
9	7, 8	cdif 3537	. . . . . . 7 class (𝑔 ∖ 𝑥)
10	5	cv 1474	. . . . . . 7 class 𝑓
11	9, 10	wcel 1977	. . . . . 6 wff (𝑔 ∖ 𝑥) ∈ 𝑓
12	6, 11	wo 382	. . . . 5 wff (𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)
13	7	cpw 4108	. . . . 5 class 𝒫 𝑔
14	12, 4, 13	wral 2896	. . . 4 wff ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)
15		cfil 21459	. . . . 5 class Fil
16	7, 15	cfv 5804	. . . 4 class (Fil‘𝑔)
17	14, 5, 16	crab 2900	. . 3 class {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)}
18	2, 3, 17	cmpt 4643	. 2 class (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)})
19	1, 18	wceq 1475	1 wff UFil = (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)})

This definition is referenced by:  isufil  21517