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)\exists g\in \mathrm{UFil}\left(x\right)f\subseteq g\right\}$$

Detailed syntax breakdown

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