Definition df-ufil 22503

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 22501	. 2 class UFil
2		vg	. . 3 setvar 𝑔
3		cvv 3494	. . 3 class V
4		vx	. . . . . . 7 setvar 𝑥
5		vf	. . . . . . 7 setvar 𝑓
6	4, 5	wel 2111	. . . . . 6 wff 𝑥 ∈ 𝑓
7	2	cv 1532	. . . . . . . 8 class 𝑔
8	4	cv 1532	. . . . . . . 8 class 𝑥
9	7, 8	cdif 3932	. . . . . . 7 class (𝑔 ∖ 𝑥)
10	5	cv 1532	. . . . . . 7 class 𝑓
11	9, 10	wcel 2110	. . . . . 6 wff (𝑔 ∖ 𝑥) ∈ 𝑓
12	6, 11	wo 843	. . . . 5 wff (𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)
13	7	cpw 4538	. . . . 5 class 𝒫 𝑔
14	12, 4, 13	wral 3138	. . . 4 wff ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)
15		cfil 22447	. . . . 5 class Fil
16	7, 15	cfv 6349	. . . 4 class (Fil‘𝑔)
17	14, 5, 16	crab 3142	. . 3 class {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)}
18	2, 3, 17	cmpt 5138	. 2 class (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)})
19	1, 18	wceq 1533	1 wff UFil = (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)})

This definition is referenced by:  isufil  22505