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 = ( 𝑔 ∈ V ↦ { 𝑓 ∈ ( Fil ‘ 𝑔 ) ∣ ∀ 𝑥 ∈ 𝒫 𝑔 ( 𝑥𝑓 ∨ ( 𝑔𝑥 ) ∈ 𝑓 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cufil UFil
1 vg 𝑔
2 cvv V
3 vf 𝑓
4 cfil Fil
5 1 cv 𝑔
6 5 4 cfv ( Fil ‘ 𝑔 )
7 vx 𝑥
8 5 cpw 𝒫 𝑔
9 7 cv 𝑥
10 3 cv 𝑓
11 9 10 wcel 𝑥𝑓
12 5 9 cdif ( 𝑔𝑥 )
13 12 10 wcel ( 𝑔𝑥 ) ∈ 𝑓
14 11 13 wo ( 𝑥𝑓 ∨ ( 𝑔𝑥 ) ∈ 𝑓 )
15 14 7 8 wral 𝑥 ∈ 𝒫 𝑔 ( 𝑥𝑓 ∨ ( 𝑔𝑥 ) ∈ 𝑓 )
16 15 3 6 crab { 𝑓 ∈ ( Fil ‘ 𝑔 ) ∣ ∀ 𝑥 ∈ 𝒫 𝑔 ( 𝑥𝑓 ∨ ( 𝑔𝑥 ) ∈ 𝑓 ) }
17 1 2 16 cmpt ( 𝑔 ∈ V ↦ { 𝑓 ∈ ( Fil ‘ 𝑔 ) ∣ ∀ 𝑥 ∈ 𝒫 𝑔 ( 𝑥𝑓 ∨ ( 𝑔𝑥 ) ∈ 𝑓 ) } )
18 0 17 wceq UFil = ( 𝑔 ∈ V ↦ { 𝑓 ∈ ( Fil ‘ 𝑔 ) ∣ ∀ 𝑥 ∈ 𝒫 𝑔 ( 𝑥𝑓 ∨ ( 𝑔𝑥 ) ∈ 𝑓 ) } )