Lexicographic orders: $\{0,1\}\times \mathbb{N}$ and $\mathbb{N}\times \mathbb{N}$

The relation $\prec$ is irreflexive on $\mathbb{N}\times \mathbb{N}$: $(m,n)\prec (m,n)$ would require $m<m$, or $m=m$ and $n<n$, and both fail by trichotomy of the order of $\mathbb{N}$.

The relation $\prec$ is transitive on $\mathbb{N}\times \mathbb{N}$: if $(m,n)\prec (m^{\mathrm{\prime }},n^{\mathrm{\prime }})$ and $(m^{\mathrm{\prime }},n^{\mathrm{\prime }})\prec (m^{\mathrm{\prime }\mathrm{\prime }},n^{\mathrm{\prime }\mathrm{\prime }})$, then the definition gives $m\le m^{\mathrm{\prime }}$ and $m^{\mathrm{\prime }}\le m^{\mathrm{\prime }\mathrm{\prime }}$. If $m<m^{\mathrm{\prime }}$ then $m<m^{\mathrm{\prime }\mathrm{\prime }}$ by transitivity of the order of $\mathbb{N}$ when $m^{\mathrm{\prime }}<m^{\mathrm{\prime }\mathrm{\prime }}$, and $m<m^{\mathrm{\prime }\mathrm{\prime }}$ directly when $m^{\mathrm{\prime }}=m^{\mathrm{\prime }\mathrm{\prime }}$, so $(m,n)\prec (m^{\mathrm{\prime }\mathrm{\prime }},n^{\mathrm{\prime }\mathrm{\prime }})$. If instead $m=m^{\mathrm{\prime }}$ and $n<n^{\mathrm{\prime }}$, then either $m^{\mathrm{\prime }}<m^{\mathrm{\prime }\mathrm{\prime }}$, giving $m<m^{\mathrm{\prime }\mathrm{\prime }}$ and hence $(m,n)\prec (m^{\mathrm{\prime }\mathrm{\prime }},n^{\mathrm{\prime }\mathrm{\prime }})$, or $m^{\mathrm{\prime }}=m^{\mathrm{\prime }\mathrm{\prime }}$ with $n^{\mathrm{\prime }}<n^{\mathrm{\prime }\mathrm{\prime }}$, giving $m=m^{\mathrm{\prime }\mathrm{\prime }}$ together with $n<n^{\mathrm{\prime }}<n^{\mathrm{\prime }\mathrm{\prime }}$ and hence $(m,n)\prec (m^{\mathrm{\prime }\mathrm{\prime }},n^{\mathrm{\prime }\mathrm{\prime }})$.

The initial segment of $W$ below $(1,0)$ is exactly $\{0\}\times \mathbb{N}$, and $e(n)=(0,n)$ is an order isomorphism of $(\mathbb{N},<)$ onto that initial segment: for a pair $(m,k)\in W$ the first coordinate satisfies $m\in \{0,1\}$, and $(m,k)\prec (1,0)$ means $m<1$, or $m=1$ and $k<0$. The case $m=0$ satisfies the first disjunct by $0<1$ from [F6]; the case $m=1$ satisfies neither disjunct, since $1<1$ is false in the total order and $k<0$ is impossible because $0\le k$ for every natural $k$ by [F6]. Hence $(m,k)\prec (1,0)$ if and only if $m=0$, which proves $W_{<(1,0)}=\{0\}\times \mathbb{N}$ by [F8]. The map $e$ is a bijection onto $\{0\}\times \mathbb{N}$ by [F1] and [F2], and for naturals $n,m$ one has $n\le m$ if and only if $e(n)\le e(m)$: if $n<m$ then $(0,n)\prec (0,m)$; if $n=m$ then $e(n)=e(m)$ by [F2]; conversely $e(n)\prec e(m)$ forces $n<m$, because the first coordinates are equal and the second coordinate decides, and $e(n)=e(m)$ forces $n=m$ by [F2]. Hence $e$ is an order isomorphism by [F9].

For every $n\in \mathbb{N}$ the predecessors of $(0,n)$ in $W$ are exactly the pairs $(0,j)$ with $j<n$: a pair $(m,k)\in W$ satisfies $(m,k)\prec (0,n)$ if and only if $m=0$ and $k<n$, since $m<0$ is impossible for $m\in \{0,1\}$ because $0\le m$ by [F6] and the order is total, and the cases $m=0$ and $m=1$ reduce to $k<n$ and to the false condition $1<0$.

Claim (i), least elements: let $S\subseteq W$ be nonempty. If $S$ meets $\{0\}\times \mathbb{N}$, the set $A=\{n\in \mathbb{N}:(0,n)\in S\}$ is a nonempty subset of $\mathbb{N}$, hence has a least element $n_0$ by [F5], and $(0,n_0)$ is $\prec$-least in $S$: a member $(0,n)$ of $S$ has $n\in A$, so $n_0\le n$, while a member $(1,n)$ of $S$ satisfies $(0,n_0)\prec (1,n)$ because $0<1$ by [F6]. If $S$ does not meet $\{0\}\times \mathbb{N}$ then $S\subseteq \{1\}\times \mathbb{N}$ by [F1], the set $B=\{n\in \mathbb{N}:(1,n)\in S\}$ is nonempty and has a least element $k$ by [F5], and $(1,k)$ is $\prec$-least in $S$, every member of $S$ being $(1,n)$ with $k\le n$.

Claim (ii), least elements: let $S\subseteq \mathbb{N}\times \mathbb{N}$ be nonempty. The set of first coordinates $A=\{m\in \mathbb{N}:\mathrm{\exists }n\in \mathbb{N}(m,n)\in S\}$ is a definable subcollection of $\mathbb{N}$, hence a set by [F12], and it is nonempty, so it has a least element $m_0$ by [F5]. The set $B=\{n\in \mathbb{N}:(m_0,n)\in S\}$ is then nonempty and has a least element $k$ by [F5], and $(m_0,k)$ is $\prec$-least in $S$: a member $(m,n)$ of $S$ has $m\ge m_0$, so if $m>m_0$ then $(m_0,k)\prec (m,n)$, while if $m=m_0$ then $n\in B$ and $n\ge k$, giving $(m_0,k)=(m,n)$ or $(m_0,k)\prec (m,n)$.

Trichotomy: given distinct pairs $(m,n)$ and $(m^{\mathrm{\prime }},n^{\mathrm{\prime }})$, totality of the order of $\mathbb{N}$ decides between $m<m^{\mathrm{\prime }}$, $m=m^{\mathrm{\prime }}$ and $m^{\mathrm{\prime }}<m$; the first gives $(m,n)\prec (m^{\mathrm{\prime }},n^{\mathrm{\prime }})$ and the third gives $(m^{\mathrm{\prime }},n^{\mathrm{\prime }})\prec (m,n)$. If $m=m^{\mathrm{\prime }}$, totality decides between $n<n^{\mathrm{\prime }}$, $n=n^{\mathrm{\prime }}$ and $n^{\mathrm{\prime }}<n$: the first gives $(m,n)\prec (m^{\mathrm{\prime }},n^{\mathrm{\prime }})$, the third gives $(m^{\mathrm{\prime }},n^{\mathrm{\prime }})\prec (m,n)$, and $n=n^{\mathrm{\prime }}$ together with $m=m^{\mathrm{\prime }}$ gives $(m,n)=(m^{\mathrm{\prime }},n^{\mathrm{\prime }})$ by [F2], contrary to distinctness. At most one alternative holds: equality together with either inequality substitutes to $(m,n)\prec (m,n)$, excluded by step 1.1; and $(m,n)\prec (m^{\mathrm{\prime }},n^{\mathrm{\prime }})$ together with $(m^{\mathrm{\prime }},n^{\mathrm{\prime }})\prec (m,n)$ is impossible, because combining the two defining disjunctions leaves the four alternatives $m<m^{\mathrm{\prime }}$ with $m^{\mathrm{\prime }}<m$; $m<m^{\mathrm{\prime }}$ with $m^{\mathrm{\prime }}=m$ and $n^{\mathrm{\prime }}<n$; $m=m^{\mathrm{\prime }}$ and $n<n^{\mathrm{\prime }}$ with $m^{\mathrm{\prime }}<m$; and $m=m^{\mathrm{\prime }}$ and $n<n^{\mathrm{\prime }}$ with $m^{\mathrm{\prime }}=m$ and $n^{\mathrm{\prime }}<n$, each contradicting trichotomy of the order of $\mathbb{N}$.

Claim (iii), first part: $F(0,n)=n$ for every $n\in \mathbb{N}$. Otherwise the set of naturals $n$ with $F(0,n)\mathrm{\ne }n$ is nonempty and has a least element $n_0$ by [F5]; then $F(0,j)=j$ for every $j<n_0$, and the defining equation of the collapse [F11] together with step 1.4 gives $F(0,n_0)=\{F(y):y\prec (0,n_0)\}=\{F(0,j):j<n_0\}=\{j:j<n_0\}=n_0$ by [F4], a contradiction.

Claim (i), the comparability consequence: step 1.3 exhibits an order isomorphism $\mathbb{N}\cong W_{<(1,0)}$, which is alternative (ii) of [F10] for the pair of well-orders $(\mathbb{N},<)$ and $(W,\prec )$ with witness $(1,0)$; by the mutual exclusivity in [F10] the alternative $\mathbb{N}\cong W$ fails, and the witness $(1,0)$ is unique.

Claim (iii), second part: $F(1,0)=\{F(y):y\prec (1,0)\}$ by the defining equation of [F11], and the predecessors of $(1,0)$ in $W$ are exactly the pairs $(0,n)$ with $n\in \mathbb{N}$ by step 1.3, so $F(1,0)=\{F(0,n):n\in \mathbb{N}\}=\{n:n\in \mathbb{N}\}=\mathbb{N}=\omega$ by step 2.2 and [F4]; since the image of $F$ is the order type $\mathrm{o}\mathrm{t}(W)$, an ordinal, we have $\omega \in \mathrm{o}\mathrm{t}(W)$.

The relation $\prec$ is irreflexive and transitive on $\mathbb{N}\times \mathbb{N}$ by steps 1.1 and 1.2 and trichotomous by step 2.1, so it is the strict presentation of a total order; $W$ inherits it and every nonempty subset of $W$ has a least element by step 1.5, while every nonempty subset of $\mathbb{N}\times \mathbb{N}$ has one by step 1.6, so both are well ordered in the sense of [F7]. Step 1.3 identifies $W_{<(1,0)}$ and the isomorphism $n\mapsto (0,n)$, and step 2.3 records that $\mathbb{N}$ is isomorphic to that proper initial segment and to no other initial segment and not to $W$ itself. Steps 2.2 and 3.1 compute the stated collapse values: $F(0,n)=n$ and $F(1,0)=\omega$, so the order type of $W$ is an ordinal containing $\omega$. No object is selected at any stage: the least elements come from the well-ordering of $\mathbb{N}$ and the collapse from uniqueness, so no choice principle is used.