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 } |
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 } |