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 \| \forall f \in Fil (x) \exists g \in UFil (x) f \subseteq g\}$

Step	Hyp	Ref	Expression
0		cufl	$class UFL$
1		vx	$setvar x$
2		vf	$setvar f$
3		cfil	$class Fil$
4	1	cv	$setvar x$
5	4 3	cfv	$class Fil (x)$
6		vg	$setvar g$
7		cufil	$class UFil$
8	4 7	cfv	$class UFil (x)$
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 UFil (x) f \subseteq g$
13	12 2 5	wral	$wff \forall f \in Fil (x) \exists g \in UFil (x) f \subseteq g$
14	13 1	cab	$class \{x \| \forall f \in Fil (x) \exists g \in UFil (x) f \subseteq g\}$
15	0 14	wceq	$wff UFL = \{x \| \forall f \in Fil (x) \exists g \in UFil (x) f \subseteq g\}$

Metamath Proof Explorer