Definition df-ufil 23052

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 23050	. 2 class UFil
2		vg	. . 3 setvar 𝑔
3		cvv 3432	. . 3 class V
4		vx	. . . . . . 7 setvar 𝑥
5		vf	. . . . . . 7 setvar 𝑓
6	4, 5	wel 2107	. . . . . 6 wff 𝑥 ∈ 𝑓
7	2	cv 1538	. . . . . . . 8 class 𝑔
8	4	cv 1538	. . . . . . . 8 class 𝑥
9	7, 8	cdif 3884	. . . . . . 7 class (𝑔 ∖ 𝑥)
10	5	cv 1538	. . . . . . 7 class 𝑓
11	9, 10	wcel 2106	. . . . . 6 wff (𝑔 ∖ 𝑥) ∈ 𝑓
12	6, 11	wo 844	. . . . 5 wff (𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)
13	7	cpw 4533	. . . . 5 class 𝒫 𝑔
14	12, 4, 13	wral 3064	. . . 4 wff ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)
15		cfil 22996	. . . . 5 class Fil
16	7, 15	cfv 6433	. . . 4 class (Fil‘𝑔)
17	14, 5, 16	crab 3068	. . 3 class {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)}
18	2, 3, 17	cmpt 5157	. 2 class (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)})
19	1, 18	wceq 1539	1 wff UFil = (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)})

This definition is referenced by:  isufil  23054