Definition df-ufl

Description: Define the class of base sets for which the ultrafilter lemma filssufil holds. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	df-ufl	|- UFL = { x | A. f e. ( Fil ` x ) E. g e. ( UFil ` x ) f C_ g }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cufl	|- UFL
1		vx	|- x
2		vf	|- f
3		cfil	|- Fil
4	1	cv	|- x
5	4 3	cfv	|- ( Fil ` x )
6		vg	|- g
7		cufil	|- UFil
8	4 7	cfv	|- ( UFil ` x )
9	2	cv	|- f
10	6	cv	|- g
11	9 10	wss	|- f C_ g
12	11 6 8	wrex	|- E. g e. ( UFil ` x ) f C_ g
13	12 2 5	wral	|- A. f e. ( Fil ` x ) E. g e. ( UFil ` x ) f C_ g
14	13 1	cab	|- { x | A. f e. ( Fil ` x ) E. g e. ( UFil ` x ) f C_ g }
15	0 14	wceq	|- UFL = { x | A. f e. ( Fil ` x ) E. g e. ( UFil ` x ) f C_ g }