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