Set theory, property of addition of natural numbers in the cardinal way

Consider the set of natural numbers $\mathbb N$. On this set we define an operation '+', as follows: for all $n,m \in \mathbb N$ we put $n+m$ to be the unique natural number $t \in \mathbb N$ such that there are $X,Y$ such that

$$ X \cap Y = \emptyset, \quad X \cup Y = t, \quad X \sim n, \quad Y \sim m.$$

This is called, for obvious reasons, the "cardinal definition" of addition on the natural numbers.

(You can assume that we already know (i.e. we've already proved) that there is such a natural number $t$, and moreover that this number is unique.)

Here '$X \sim n$' means that there is a bijection between $X$ and $n$.

I'm having a lot of trouble proving the following (quite elementary it seems) result:

Theorem. For all $m,n,k \in \mathbb N$ we have
$$ n < m \quad \Leftrightarrow \quad n + k < m + k.$$

(Here for any natural numbers $n,m$ we use the abbreviation $n

Of course one would think that a good first approach would be to go by induction; I've tried it on $k$ but it didn't work out. Well..., it is clear that induction on $k$ 'works' assuming the fact that we already know that $n+(k+1) = (n+k) + 1$ for all natural numbers $n,k$. So it is sufficient to show the latter statement. I've found a proof for it, but ironically in the proof I (have to) use the above (unproved) theorem, namely the implication from left to right. So I'm basically stuck in a circularity.

I also tried several other things, without success.

Comment. You are not allowed to use any 'theorems' about the natural numbers, except for the most basic ones. For example, you may use that they form a linear order, but not much more. Also, at this point there is no such thing as an 'ordinal definition' of the '+' on the natural numbers.

Answer

First note that the natural numbers in your definition are transitive sets. So if $m\in m$ then $m\subseteq n$, and furthermore $m\neq n$, otherwise you would have $n\in n$ in contradiction to the axiom of regularity.

Use this fact to deduce that $m

First note that if $m=0$ then this follows from the above directly regardless to the value of $k$. So we may assume that $m\neq 0$.

We next prove by induction on $k$. For $k=0$ this is obvious. Assume that for $k-1$ it is true that $m+(k-1)

Now suppose that $M\subsetneqq N$, and $K$ are sets of cardinality $m,n,k$ respectively, and $K$ is disjoint from $N$ (and so from $M$ as well). By the above it suffices to show that that there is no injection from $N\cup K$ into $M\cup K$ in order to show that $m+k

Suppose that there was an injection $g\colon N\cup K\to M\cup K$, restrict $g$ to $N$, since $M$ is a proper subset there has to be some $x\in N$ such that $g(x)\in K$, otherwise $g\upharpoonright N$ is an injection from $N$ into $M$. It follows that there exists some $u\in K$ such that $g(u)\in M$, otherwise $g\upharpoonright K$ would be an injection into $K\setminus\{g(x)\}$, which is impossible.

Define $f$ to be $(g\setminus\{\langle x,g(x)\rangle,\langle y,g(y)\rangle\})\cup\{\langle x,g(y)\rangle\}$. This is an injection from $N\cup K\setminus\{y\}$ into $M\cup K\setminus\{g(x)\}$. That is, an injection from a set of cardinality $n+(k-1)$ into a set of cardinality $m+(k-1)$. But the induction hypothesis tells us that this is a contradiction.

---

More:

1. Subset of a finite set is finite