# 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 ${⊢}\mathrm{UFL}=\left\{{x}|\forall {f}\in \mathrm{Fil}\left({x}\right)\phantom{\rule{.4em}{0ex}}\exists {g}\in \mathrm{UFil}\left({x}\right)\phantom{\rule{.4em}{0ex}}{f}\subseteq {g}\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cufl ${class}\mathrm{UFL}$
1 vx ${setvar}{x}$
2 vf ${setvar}{f}$
3 cfil ${class}\mathrm{Fil}$
4 1 cv ${setvar}{x}$
5 4 3 cfv ${class}\mathrm{Fil}\left({x}\right)$
6 vg ${setvar}{g}$
7 cufil ${class}\mathrm{UFil}$
8 4 7 cfv ${class}\mathrm{UFil}\left({x}\right)$
9 2 cv ${setvar}{f}$
10 6 cv ${setvar}{g}$
11 9 10 wss ${wff}{f}\subseteq {g}$
12 11 6 8 wrex ${wff}\exists {g}\in \mathrm{UFil}\left({x}\right)\phantom{\rule{.4em}{0ex}}{f}\subseteq {g}$
13 12 2 5 wral ${wff}\forall {f}\in \mathrm{Fil}\left({x}\right)\phantom{\rule{.4em}{0ex}}\exists {g}\in \mathrm{UFil}\left({x}\right)\phantom{\rule{.4em}{0ex}}{f}\subseteq {g}$
14 13 1 cab ${class}\left\{{x}|\forall {f}\in \mathrm{Fil}\left({x}\right)\phantom{\rule{.4em}{0ex}}\exists {g}\in \mathrm{UFil}\left({x}\right)\phantom{\rule{.4em}{0ex}}{f}\subseteq {g}\right\}$
15 0 14 wceq ${wff}\mathrm{UFL}=\left\{{x}|\forall {f}\in \mathrm{Fil}\left({x}\right)\phantom{\rule{.4em}{0ex}}\exists {g}\in \mathrm{UFil}\left({x}\right)\phantom{\rule{.4em}{0ex}}{f}\subseteq {g}\right\}$