Bourbaki–Witt fixed point theorem

Let $(P, \le)$ be a chain-complete poset and let $f : P \to P$ be progressive, that is $x \le f(x)$ for every $x \in P$ (Chain-complete poset). Then $f$ has a fixed point: there exists $c \in P$ with $f(c) = c$.

No form of the Axiom of Choice is used, and $f$ is not assumed to be monotone, injective, or continuous in any sense.

• Why this matters here. The usual route to Zorn's lemma runs through transfinite recursion, which needs ordinals, transfinite induction and replacement. Bourbaki–Witt replaces all of that with the smallest admissible set, so the foundations page that supports Zorn's lemma stays ordinal-free. Ordinals are still worth having, but nothing on the path to Zorn or to the ultrafilter lemma requires them.
• The theorem itself is choice-free. Choice enters only in Zorn's lemma, at the single step where a strict upper bound is selected for every chain simultaneously. Keeping the two separate is what lets later pages state honestly which of their results need choice.
• Both hypotheses are load-bearing. Progressivity without chain-completeness fails (A progressive map with no fixed point, on a poset that is not chain-complete ↗), and the fixed point is genuinely produced at the top of a chain, not by iterating $f$: no iteration argument is available, since $f$ need not be monotone and the chain $M$ need not be countable.
• The fixed point found is $\sup M$, and $M$ is the smallest admissible set, so the construction is canonical rather than a choice among many fixed points.