Metamath Proof Explorer


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 }