[proofplan] We prove directly from the definition of an ordinal as a transitive set well-ordered by membership. First we verify that $\alpha + 1 = \alpha \cup \{\alpha\}$ is transitive by separating the cases where an element lies in an old element of $\alpha$ or in the new element $\alpha$. Then we show that membership well-orders $\alpha + 1$: every nonempty subset either already meets $\alpha$, in which case the old well-order gives a least element, or is exactly $\{\alpha\}$. Finally, $\alpha \in \alpha + 1$ follows immediately from the definition of adjoining $\alpha$ as a singleton. [/proofplan]

[step:Define the successor set and record the old ordinal structure] Let \begin{align*} \beta := \alpha + 1 := \alpha \cup \{\alpha\}. \end{align*} Since $\alpha$ is an ordinal, $\alpha$ is transitive and the membership relation $\in$ well-orders $\alpha$. Thus for every nonempty subset $B \subseteq \alpha$, there exists an element $b_0 \in B$ such that no element $b \in B$ satisfies $b \in b_0$. We will prove that $\beta$ is transitive and that $\in$ well-orders $\beta$. [/step]

[step:Prove that $\alpha$ is not an element of itself] We first note that $\alpha \notin \alpha$. If $\alpha \in \alpha$, then $\{\alpha\}$ is a nonempty subset of $\alpha$. Since $\in$ well-orders $\alpha$, the set $\{\alpha\}$ has an $\in$-least element, namely $\alpha$. But $\alpha \in \alpha$ gives an element of $\{\alpha\}$ lying in $\alpha$, contradicting the defining property of being $\in$-least in $\{\alpha\}$. Hence $\alpha \notin \alpha$. [/step]

[step:Show that the successor set is transitive] Let $x$ and $y$ be sets such that $x \in y$ and $y \in \beta$. We must prove $x \in \beta$. Since $y \in \beta = \alpha \cup \{\alpha\}$, either $y \in \alpha$ or $y = \alpha$. If $y \in \alpha$, then the transitivity of $\alpha$ and $x \in y$ imply $x \in \alpha$, hence $x \in \beta$. If $y = \alpha$, then $x \in y$ becomes $x \in \alpha$, again giving $x \in \beta$. Therefore $\beta$ is transitive. [/step]

[step:Show that membership is a strict total order on the successor set] Let $x,y \in \beta$ with $x \neq y$. Since $\beta = \alpha \cup \{\alpha\}$, each of $x$ and $y$ is either an element of $\alpha$ or equal to $\alpha$. If $x,y \in \alpha$, then the membership order on $\alpha$ is total, so either $x \in y$ or $y \in x$. If $x \in \alpha$ and $y = \alpha$, then $x \in y$. If $x = \alpha$ and $y \in \alpha$, then $y \in x$. The remaining case $x = \alpha$ and $y = \alpha$ is impossible because $x \neq y$. Thus any two distinct elements of $\beta$ are comparable by membership. The relation is irreflexive on $\beta$. If $x \in \alpha$, then $x \notin x$ because the membership relation well-orders $\alpha$ and hence is irreflexive on $\alpha$. If $x = \alpha$, then $x \notin x$ is exactly $\alpha \notin \alpha$, proved above. The relation is asymmetric on $\beta$. Suppose $x,y \in \beta$ and $x \in y$. If also $y \in x$, then $x \in y \in \beta$ implies $x \in \beta$ and $y \in x \in \beta$. If $x,y \in \alpha$, asymmetry of the membership order on $\alpha$ gives a contradiction. If $x \in \alpha$ and $y = \alpha$, then $y \in x$ says $\alpha \in x$; since $x \in \alpha$ and $\alpha$ is transitive, this implies $\alpha \in \alpha$, contradicting $\alpha \notin \alpha$. If $x = \alpha$ and $y \in \alpha$, then $x \in y$ says $\alpha \in y$; since $y \in \alpha$ and $\alpha$ is transitive, this again implies $\alpha \in \alpha$, a contradiction. The case $x = y = \alpha$ contradicts $\alpha \notin \alpha$. The relation is transitive on $\beta$. Let $x,y,z \in \beta$ satisfy $x \in y$ and $y \in z$. If $z = \alpha$, then $y \in \alpha$, and transitivity of the set $\alpha$ gives $x \in \alpha = z$. If $z \in \alpha$, then transitivity of the set $\alpha$ applied to $y \in z \in \alpha$ gives $y \in \alpha$, and then transitivity of the set $\alpha$ applied to $x \in y \in \alpha$ gives $x \in \alpha$. Thus $x,y,z \in \alpha$, and transitivity of the membership order on $\alpha$ gives $x \in z$. Therefore membership is a strict total order on $\beta$. [/step]

[step:Show that every nonempty subset of the successor has a least element] Let $A \subseteq \beta$ be nonempty. Define \begin{align*} A_0 := A \cap \alpha. \end{align*} If $A_0 \neq \varnothing$, then $A_0$ is a nonempty subset of $\alpha$. Since $\in$ well-orders $\alpha$, there exists $a_0 \in A_0$ such that no $a \in A_0$ satisfies $a \in a_0$. We claim that $a_0$ is also $\in$-least in $A$. Let $a \in A$. If $a \in \alpha$, then $a \in A_0$, so $a \notin a_0$ by the choice of $a_0$. If $a \notin \alpha$, then because $a \in A \subseteq \beta = \alpha \cup \{\alpha\}$, we must have $a = \alpha$. Since $a_0 \in \alpha$, we have $a_0 \in \alpha = a$. We now prove directly that $a \notin a_0$: if $a \in a_0$, then $\alpha \in a_0$; because $a_0 \in \alpha$ and $\alpha$ is transitive, this would imply $\alpha \in \alpha$, contradicting $\alpha \notin \alpha$. Hence no element of $A$ lies in $a_0$, so $a_0$ is $\in$-least in $A$. If $A_0 = \varnothing$, then every element of $A$ lies in $\beta \setminus \alpha = \{\alpha\}$, so the nonemptiness of $A$ gives $A = \{\alpha\}$. Since $\alpha \notin \alpha$, no element of $A$ lies in $\alpha$, and therefore $\alpha$ is the $\in$-least element of $A$. Thus every nonempty subset of $\beta$ has an $\in$-least element. [/step]

[step:Conclude that the successor is an ordinal and contains the original ordinal] We have proved that $\beta$ is transitive and that membership well-orders $\beta$. Therefore $\beta$ is an ordinal. Since \begin{align*} \beta = \alpha \cup \{\alpha\}, \end{align*} we also have $\alpha \in \{\alpha\} \subseteq \beta$. Hence $\alpha \in \alpha + 1$. Substituting back $\beta = \alpha + 1$, we conclude that $\alpha + 1$ is an ordinal and $\alpha \in \alpha + 1$. [/step]