= Hartogs bound on partial ordinal injections
{title2=$P_X\subseteq\mathcal P(h(X)\times X)$}
Every <injection> from an <ordinal> into a <set> $X$ has domain strictly below the <Hartogs number> $h(X)$. Therefore all partial <injections> with <ordinal> domain and range in $X$ form a <set> of <graph of a function>[graphs] contained in $\mathcal P(h(X)\times X)$. Under extension, the <union> of a <chain> remains a partial <injection> of this kind. <Zorn's lemma> then supplies a maximal one, and extending at an unused range element shows that it must be a <bijection> onto $X$. This gives the <well-ordering theorem> with the set-sizedness of the poset made explicit.
Back to article page
