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