Solution (source code)

= Solution

Interpret the assertion in the usual well-founded, class-theoretic version of <Zermelo set theory>, including <foundation>, class comprehension and separation with class parameters. Classes are not extra sets. The <axiom of limitation of size>, in the form used here, says that every proper class is in bijection with the universe $V$.

First derive <replacement>. Let a functional class relation map a set $a$ onto its image class $B$. If $B$ were proper, the limitation axiom would give a bijection $h:B\to V$. Its composite with the original map would be a surjection $g:a\to V$. Class-parameter <separation> forms
$$
D=\{x\in a:x\notin g(x)\}.
$$
Surjectivity gives $d\in a$ with $g(d)=D$, whence $d\in D$ iff $d\notin D$, a contradiction. Thus $B$ is a set, proving each instance of replacement. The argument also gives class replacement when the functional class is a parameter.

The class $\mathrm{On}$ of <ordinals> is proper: were it a set, its union and successor would be ordinals larger than every ordinal in it. Limitation gives a bijection $e:\mathrm{On}\to V$. Ordering $V$ by the ordinal indices of $e$ gives a global well-order; each nonempty set has a member with least index. Choosing that member defines <global choice>.

Conversely assume replacement and global choice. Ordinary choice well-orders each rank segment, and global choice selects such a well-order uniformly, since the collection of well-orders of each fixed rank segment is a nonempty set. Order all sets first by their <rank of a set> and then by the selected order within that rank. The resulting global order is set-like: the predecessors of any element are contained in a rank segment and form a set. Restrict it to a proper class $A$. By <transfinite recursion>, enumerate $A$ in this order. It cannot be exhausted at a set ordinal, since <replacement> would then make $A$ a set. Every member appears, because its predecessors form a set, whose well-order has an ordinal order type. Hence $A$ has order type $\mathrm{On}$. The same applies to $V$, and composing the two enumerations gives a bijection $A\cong V$. Thus \b[limitation of size is equivalent to replacement plus global choice] in this class-theoretic setting.