Solution (source code)

= Solution

<Hartogs theorem> says that for every <set> $X$ there is a least <ordinal> $h(X)$ for which no <injection> $h(X)\to X$ exists. This does not require the <axiom of choice>. Form the <set> $W$ of <well-orderings> of <subsets> of $X$. It can be defined by the <axiom schema of specification> inside
$$
\mathcal P(X)\times\mathcal P(X\times X),
$$
recording a <subset> and its <well-order>. Each member of $W$ has a unique <ordinal> <order type>. \b[<Axiom schema of replacement> is used to collect those order types into a <set>]
$$
H=\{\operatorname{otp}(Y,R):(Y,R)\in W\}.
$$
Every member of an <ordinal> in $H$ is the <order type> of an initial segment of the corresponding <well-ordering>, so also belongs to $H$. Thus $H$ is a <transitive set> of <ordinals> and is itself an <ordinal>. An <ordinal> $\alpha$ belongs to $H$ exactly when it injects into $X$: use a <bijection> to a <well-ordered> <subset> in one direction, and transport the <ordinal> order along the <injection> in the other. If $H$ injected into $X$, this characterization would give $H\in H$, impossible for an <ordinal>. All smaller <ordinals> lie in $H$ and do inject into $X$. Therefore $H=h(X)$. Apart from the standard order-type theorem, the explicit collection of all order types is the <Axiom schema of replacement> step; no <axiom of choice> of a representative ordering for each type is needed.

<Zorn's lemma> states that a nonempty <partially ordered set> in which every <chain> has an <upper bound> has a <maximal element>. Use the <Hartogs bound on partial ordinal injections> to obtain a set-sized <partially ordered set>. Consider the partial <injections> into $X$ whose domains are <ordinals>. <Hartogs theorem> bounds every such domain strictly below $h=h(X)$. Their <graphs of a function> therefore form a <set>
$$
P=\{f\subseteq h\times X:f\text{ is an injective function and }\operatorname{dom}f\text{ is an ordinal}\},
$$
obtained by the <axiom schema of specification> from $\mathcal P(h\times X)$. Order $P$ by extension. It is nonempty because it contains the empty <function>. A <chain> has as an <upper bound> the <union> of its <graphs of a function>: extension makes this a <function>, <injectivity> is preserved, and its domain is an <union> of <ordinals> and hence an <ordinal>. Its range is contained in $X$, so <Hartogs theorem> forces its domain to be strictly below $h$; thus it belongs to $P$. The empty <chain> also has the empty <function> as an <upper bound>.

By <Zorn's lemma> choose a maximal $f:\alpha\to X$. If an element $x\in X$ lay outside its range, appending $f(\alpha)=x$ would give a larger <injection> on $\alpha+1$. Such an <injection> itself guarantees $\alpha+1<h$ by <Hartogs theorem>, so it is a legitimate member of $P$, contradicting <maximality in a partially ordered set>. Therefore $f$ is <surjective>, and
$$
\boxed{X\text{ is equinumerous with an ordinal}.}
$$
For this single extension one only selects an element of one specified nonempty <set>; no additional simultaneous choices are hidden in the argument. <Zorn's lemma> is the form of the <axiom of choice> used to obtain <maximality in a partially ordered set>.

Finally work with <cardinals>, represented by initial <ordinals>, and put $\mu=\max(\kappa,\lambda)$. It is infinite by hypothesis. Nonzeroness of each factor gives an <injection> of the larger <cardinal> into the <Cartesian product> by holding a coordinate of the other fixed. The supplied infinite-ordinal square result gives $|\mu\times\mu|=\mu$. Hence
$$
\mu\leq\kappa\lambda\leq|\mu\times\mu|=\mu.
$$
For the sum, use <disjoint union>:
$$
\mu\leq\kappa+\lambda\leq|\mu\times\{0,1\}|\leq|\mu\times\mu|=\mu.
$$
The last <injection> exists because $\mu$ is infinite and contains two distinct elements. <Cantor-Schröder-Bernstein theorem> turns both pairs of bounds into equalities, proving
$$
\boxed{\kappa+\lambda=\kappa\lambda=\max(\kappa,\lambda).}
$$
These final operations are <cardinal sum> and <multiplication>, measuring disjoint <unions> and Cartesian products. They are not the noncommutative <ordinal arithmetic> considered in question 5.