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 21925
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 21923 . 2 class UFil
2 vg . . 3 setvar 𝑔
3 cvv 3351 . . 3 class V
4 vx . . . . . . 7 setvar 𝑥
5 vf . . . . . . 7 setvar 𝑓
64, 5wel 2146 . . . . . 6 wff 𝑥𝑓
72cv 1630 . . . . . . . 8 class 𝑔
84cv 1630 . . . . . . . 8 class 𝑥
97, 8cdif 3720 . . . . . . 7 class (𝑔𝑥)
105cv 1630 . . . . . . 7 class 𝑓
119, 10wcel 2145 . . . . . 6 wff (𝑔𝑥) ∈ 𝑓
126, 11wo 834 . . . . 5 wff (𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)
137cpw 4297 . . . . 5 class 𝒫 𝑔
1412, 4, 13wral 3061 . . . 4 wff 𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)
15 cfil 21869 . . . . 5 class Fil
167, 15cfv 6031 . . . 4 class (Fil‘𝑔)
1714, 5, 16crab 3065 . . 3 class {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)}
182, 3, 17cmpt 4863 . 2 class (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)})
191, 18wceq 1631 1 wff UFil = (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥𝑓 ∨ (𝑔𝑥) ∈ 𝑓)})
Colors of variables: wff setvar class
This definition is referenced by:  isufil  21927
  Copyright terms: Public domain W3C validator