Row-and-column enumeration of an ordinal square (source code)

= Row-and-column enumeration of an ordinal square
{title2=$g_\alpha:\alpha^2\longrightarrow\gamma_\alpha$}

A compatible transfinite family of <bijections> can enumerate the square of an <ordinal> by adjoining a new row and then the remaining new column. Starting with $g_0=\varnothing$, extend at a successor by $g_{\alpha+1}(\alpha,\beta)=\gamma_\alpha+\beta$ for $\beta\leq\alpha$ and $g_{\alpha+1}(\beta,\alpha)=\gamma_\alpha+(\alpha+1)+\beta$ for $\beta<\alpha$. Thus $\gamma_{\alpha+1}=\gamma_\alpha+(\alpha+1)+\alpha$. At limits take compatible unions. The two new domain pieces are disjoint; the column is empty at the initial step $\alpha=0$. Each step enumerates consecutive <ordinal> intervals, proving bijectivity by <transfinite induction>. Finite stages have $\gamma_n=n^2$. Successor and limit <cardinality> arguments then give the square equality for well-orderable infinite cardinals without using that equality to justify the construction.