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 22485
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 22483 . 2 class UFil
2 vg . . 3 setvar 𝑔
3 cvv 3471 . . 3 class V
4 vx . . . . . . 7 setvar 𝑥
5 vf . . . . . . 7 setvar 𝑓
64, 5wel 2116 . . . . . 6 wff 𝑥𝑓
72cv 1537 . . . . . . . 8 class 𝑔
84cv 1537 . . . . . . . 8 class 𝑥
97, 8cdif 3907 . . . . . . 7 class (𝑔𝑥)
105cv 1537 . . . . . . 7 class 𝑓
119, 10wcel 2115 . . . . . 6 wff (𝑔𝑥) ∈ 𝑓
126, 11wo 844 . . . . 5 wff (𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)
137cpw 4512 . . . . 5 class 𝒫 𝑔
1412, 4, 13wral 3126 . . . 4 wff 𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)
15 cfil 22429 . . . . 5 class Fil
167, 15cfv 6328 . . . 4 class (Fil‘𝑔)
1714, 5, 16crab 3130 . . 3 class {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)}
182, 3, 17cmpt 5119 . 2 class (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)})
191, 18wceq 1538 1 wff UFil = (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)})
Colors of variables: wff setvar class
This definition is referenced by:  isufil  22487
  Copyright terms: Public domain W3C validator