This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ufil

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)

Ref Expression
Assertion df-ufil ⊢ UFil = g ∈ V ⟼ f ∈ Fil ⁡ g | ∀ x ∈ 𝒫 g x ∈ f ∨ g ∖ x ∈ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cufil class UFil
1 vg setvar g
2 cvv class V
3 vf setvar f
4 cfil class Fil
5 1 cv setvar g
6 5 4 cfv class Fil ⁡ g
7 vx setvar x
8 5 cpw class 𝒫 g
9 7 cv setvar x
10 3 cv setvar f
11 9 10 wcel wff x ∈ f
12 5 9 cdif class g ∖ x
13 12 10 wcel wff g ∖ x ∈ f
14 11 13 wo wff x ∈ f ∨ g ∖ x ∈ f
15 14 7 8 wral wff ∀ x ∈ 𝒫 g x ∈ f ∨ g ∖ x ∈ f
16 15 3 6 crab class f ∈ Fil ⁡ g | ∀ x ∈ 𝒫 g x ∈ f ∨ g ∖ x ∈ f
17 1 2 16 cmpt class g ∈ V ⟼ f ∈ Fil ⁡ g | ∀ x ∈ 𝒫 g x ∈ f ∨ g ∖ x ∈ f
18 0 17 wceq wff UFil = g ∈ V ⟼ f ∈ Fil ⁡ g | ∀ x ∈ 𝒫 g x ∈ f ∨ g ∖ x ∈ f