Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ufil Structured version   Visualization version   GIF version

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
StepHypRef 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 𝑓
64, 5wel 1978 . . . . . 6 wff 𝑥𝑓
72cv 1474 . . . . . . . 8 class 𝑔
84cv 1474 . . . . . . . 8 class 𝑥
97, 8cdif 3537 . . . . . . 7 class (𝑔𝑥)
105cv 1474 . . . . . . 7 class 𝑓
119, 10wcel 1977 . . . . . 6 wff (𝑔𝑥) ∈ 𝑓
126, 11wo 382 . . . . 5 wff (𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)
137cpw 4108 . . . . 5 class 𝒫 𝑔
1412, 4, 13wral 2896 . . . 4 wff 𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)
15 cfil 21459 . . . . 5 class Fil
167, 15cfv 5804 . . . 4 class (Fil‘𝑔)
1714, 5, 16crab 2900 . . 3 class {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)}
182, 3, 17cmpt 4643 . 2 class (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)})
191, 18wceq 1475 1 wff UFil = (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)})
 Colors of variables: wff setvar class This definition is referenced by:  isufil  21517
 Copyright terms: Public domain W3C validator