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

Definition df-ufil 21457
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 21455 . 2 class UFil
2 vg . . 3 setvar 𝑔
3 cvv 3172 . . 3 class V
4 vx . . . . . . 7 setvar 𝑥
5 vf . . . . . . 7 setvar 𝑓
64, 5wel 1977 . . . . . 6 wff 𝑥𝑓
72cv 1473 . . . . . . . 8 class 𝑔
84cv 1473 . . . . . . . 8 class 𝑥
97, 8cdif 3536 . . . . . . 7 class (𝑔𝑥)
105cv 1473 . . . . . . 7 class 𝑓
119, 10wcel 1976 . . . . . 6 wff (𝑔𝑥) ∈ 𝑓
126, 11wo 381 . . . . 5 wff (𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)
137cpw 4107 . . . . 5 class 𝒫 𝑔
1412, 4, 13wral 2895 . . . 4 wff 𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)
15 cfil 21401 . . . . 5 class Fil
167, 15cfv 5790 . . . 4 class (Fil‘𝑔)
1714, 5, 16crab 2899 . . 3 class {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)}
182, 3, 17cmpt 4637 . 2 class (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)})
191, 18wceq 1474 1 wff UFil = (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)})
Colors of variables: wff setvar class
This definition is referenced by:  isufil  21459
  Copyright terms: Public domain W3C validator