Equivalence between two definitions of successor ordinal

Question

So, here am I again struggling with Schimmerling. Now I just want to check if understood correctly how to relate the two definitions of a successor ordinal. We can define the successor of $\alpha$ either as $\alpha + 1$, or, alternatively, as $\alpha \cup \{\alpha\}$, right? Further, $\alpha + 1$ can be defined as $\text{type}(\langle \alpha, < \rangle\frown\langle 1, <\rangle)$, which is the order type of the well order defined over the concatenation of the ordinals $\alpha$ and $1$ (the concatenation itself is defined, in this case, as $(\{0\} \times \alpha) \cup (\{1\} \times 1)$, and the well order is defined as $(i, j) < (i,x)$ iff (i) $i=j=0$ and $x <_\alpha y$, or (ii) $i=0$ and $j=1$). So, basically, I need to prove that the order type of this concatenation just is $\alpha \cup \{\alpha\}$. I thought of setting an isomorphism like this: if $i=0$, then $\pi(i, \beta) = \beta$ for $\beta < \alpha$; if $i=1$, then we have the ordered pair $\langle 1, 0 \rangle$, such that $\pi(\langle 1, 0 \rangle) = \{\alpha\}$. Does that solve it?

Answer 1

That's not quite correct, because the element that $\langle 1,0\rangle$ is supposed to be mapped to is $\alpha$ itself rather than $\{\alpha\}$. But other than that it's just fine.

I find the other direction somewhat easier to see, $$f(\beta)=\begin{cases}\langle 0,\beta\rangle & \beta<\alpha\\\langle1,0\rangle&\beta=\alpha\end{cases}$$ but of course the two are equivalent.