The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ be a set and let $\mathcal{F}_0$ be a filter on $X$ (Filter on a set). Then there is an ultrafilter $\mathcal{U}$ on $X$ (Ultrafilter) with $\mathcal{F}_0 \subseteq \mathcal{U}$.

The hypothesis is spent exactly once, through Zorn's lemma at step 4.1; the rest of the argument is a theorem of ZF.

In particular, every set that carries a filter carries an ultrafilter. The proof uses Zorn's lemma (Zorn's lemma) and therefore the Axiom of Choice. That some choice principle is unavoidable here, if ZF is consistent, is an external independence result, not proved in this library; see the remarks below.

• The empty chain is the load-bearing case. Zorn's lemma requires an upper bound for every chain of $P$, and the empty chain has one exactly when $P$ is nonempty. Step 3.1 discharges it with $\mathcal{F}_0$ itself, and step 2.2 is what makes that possible. This is not a formality: the conclusion of The union of a nonempty chain of filters is a filter fails for the empty chain, since $\bigcup \emptyset = \emptyset$ is not a filter, which is exactly why that lemma assumes its chain nonempty; so a proof that says "the union of a chain is a filter" without the case split has a genuine gap at the one chain the hypothesis of Zorn's lemma is easiest to forget.
• Why the poset is $P$ and not $\mathrm{Filt}(X)$. Applying Zorn to $\mathrm{Filt}(X)$ would produce a maximal filter unrelated to $\mathcal{F}_0$. Restricting to the filters above $\mathcal{F}_0$ costs nothing, because step 6.1 transfers maximality back: a filter above $\mathcal{U}$ is automatically above $\mathcal{F}_0$, so maximality in $P$ already means maximality among all filters. That transfer is the only step where the shape of $P$ is used.
• The conclusion is an ultrafilter, not the ultrafilter. Zorn's lemma delivers a maximal element and no construction, so nothing in the proof distinguishes the ultrafilter it produces from any other filter above $\mathcal{F}_0$; the statement asserts existence and no uniqueness whatever. FALSE, once the ultrafilter lemma is available: every ultrafilter is principal runs the argument on the filter of tails of $\mathbb{N}$ and obtains a single free ultrafilter, which it can describe no further. How many ultrafilters extend a given filter is a separate counting question, and this library neither states nor uses an answer to it.
• Combined with A family lies in a filter exactly when it has the finite intersection property, the lemma takes its most usable form: every family of subsets of $X$ with the finite intersection property is contained in an ultrafilter on $X$. That is the version applied in topology and in model theory.
• What this costs. The proof buys the conclusion with the full Axiom of Choice, through Zorn's lemma and The Axiom of Choice and Zorn's lemma are equivalent, but the statement is, if ZF is consistent, strictly weaker than the Axiom of Choice: it is then neither provable in ZF nor strong enough to recover choice. Both of those are external metamathematical results, conditional on the consistency of ZF, and are recorded, with references and without a claim to prove them, in What the ultrafilter lemma costs: a choice principle strictly weaker than AC.