# $\alpha < \beta \implies \gamma+\alpha < \gamma + \beta$ for ordinals

Let $$\alpha,\beta, \gamma$$ be ordinals. I'm trying to prove that:

$$\alpha < \beta \implies \gamma+\alpha < \gamma + \beta$$

I managed to prove that

$$\alpha < \beta \implies \gamma + \alpha \leq \gamma + \beta$$

by showing there is a strictly order preserving function $$\gamma+\alpha \to \gamma + \beta$$

but I struggle to show equality is impossible.

So suppose to the contrary that:

$$\gamma+\alpha= \gamma + \beta$$

This implies that

$$(\gamma \times 0) \cup (\alpha \times 1) \cong (\gamma \times 0) \cup (\beta \times 1)$$

But I don't think we really can get a contradiction from this.

I read that ordinal addition is left addition, so we should somehow be able to prove that $$\alpha = \beta$$ which will be a good contradiction.

Let $$f: (\gamma \times \{0\}) \sqcup (\alpha \times \{1\}) \to (\gamma \times \{0\}) \sqcup (\beta \times \{1\})$$ be an order isomorphism. We show by induction on $$\delta < \gamma$$ that $$f(\delta,0) = (\delta,0)$$.
Base case: $$f$$ is an order isomorphism, so it must send the least element of $$(\gamma \times \{0\}) \sqcup (\alpha \times \{1\})$$ to the least element of $$(\gamma \times \{0\}) \sqcup (\beta \times \{1\})$$. The least element in either case is $$(0,0)$$.
Induction step: Suppose $$f$$ is the identity below $$(\delta,0)$$. Because $$f$$ is an order isomorphism, it must map $$(\delta,0)$$ to the least element of $$(\gamma \times \{0\}) \sqcup (\beta \times \{1\})$$ not in $$f[\delta \times \{0\}]$$; but $$f[\delta \times \{0\}] = \delta \times \{0\}$$ by hypothesis, so $$f(\delta,0) = (\delta,0)$$.
Thus, by induction $$f$$ is the identity on $$\gamma \times \{0\}$$. It follows that $$f|_{\alpha \times\{1\}}$$ must be an isomorphism of $$\alpha \times \{1\}$$ onto $$\beta \times \{1\}$$ for $$f$$ to be an isomorphism (injectivity implies elements of $$\alpha \times \{1\}$$ must map into $$\beta \times \{1\}$$, surjectivity implies all element of $$\beta \times \{1\}$$ are mapped to in this way, and $$f$$ being order-preserving implies that $$f|_{\alpha \times \{1\}}$$ is as well). Contradiction.