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<m$ for $n \in m$.)
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.
 A: 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<n$ if and only if whenever $M,N$ are sets of cardinality $m,n$ respectively, there is an injection from $M$ into $N$, but there is no injection from $N$ into $M$. The latter may be easier to prove by using the pigeonhole principle (which you can prove independently by induction, see [1]).
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)<n+(k-1)$ whenever $m<n$.
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<n+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:


*

*Subset of a finite set is finite
A: Let us define addition in a slightly different way. Let $n$ and $m$ be two natural numbers. Then we will define $n+m$ to be the unique element of $\mathbb{N}$ such that there exists sets $X_n, X_m$ such that if $X_n\sim n$ and $X_m\sim m$ and $X_n\cap X_m=\emptyset$, then $n+m\sim X_n\cup X_m$. We may also define $m\leq n$ if their is an injection of sets, $Y_n\hookrightarrow Y_m$ and $Y_n\sim n$ and $Y_m\sim m$. One may readily show that this is well defined given the following proposition.
Proposition: Let $X$ be any set such that $X\sim n$ and $X\sim m$. Then $n=m$.
Now to show your Theorem. If $m\leq n$, then their are is an injection ,$Y_m\hookrightarrow Y_n$. Now pick a set $X_k\sim k$ such that $X_k\cap Y_m=\emptyset$ and $X_k\cap Y_n=\emptyset$. Then we have $Y_m\cup X_k\hookrightarrow Y_n\cup X_k$ which proves the theorem.
Edit In the comments, the OP notes that we must show that the two definitions of $<$  is the same (the new one was implicitly defined in terns of  $\leq$). To this end let us first assume that $<$ is transitive that is if $n\in m\in k$, then $n\in k$. This means that $m=\{l:l<m\}$ and $k=\{l:l<k\}$. Then we get a map $m\hookrightarrow k$ which sends $l\mapsto l$. 
Proof of Transitivity
Let us consider the set, $P=\{k\in\mathbb{N}:l\in n\in k\implies l\in k\}$. Certainly the empty set is in $P$ vacuously. Now suppose that $p\in P$ let us now show that $p\cup\{p\}\in P$, making $P$ an inductive set sitting inside if $\mathbb{N}$, amd therefore equal to $\mathbb{N}$. We must show that if we have a chain, $n\in k \in p\cup\{p\}$, then $k\in p\cup\{p\}$. If $n\in k\in p$ we are done since $p\in P$. On the other hand if $k\notin p$, then $k\in\{p\}$ which means that $k=p$. But then $n\in k=p\subset p\cup\{p\}$. Thus $P\subset\mathbb{N}$ is inductive and so $P=\mathbb{N}$, and so $,$ is transitive
A: We begin here by only assuming that the addition of finite cardinals is a well-defined associative binary operation on the the set $\mathbb N$ satisfying, for any $m,n \in \mathbb N$
$\tag 1 m + 0 = m \; \text{ and } \; m + (n + 1) =  (m+n) + 1$
(c.f. Appendix I of Serge Lang's Undergraduate Algebra).
We also define $m \lt n$ to mean that there is a set of cardinality $m$ that can be non-surjectively injected into a set of cardinality $n$.
Proposition 1: For $m, n, k \in \mathbb N$, the statement $n \lt m$ is equivalent to $n + k \lt m+ k$.
Proof
We show that
$\tag 1 n + k \lt m+ k \text{ implies } m \lt n$
using induction on $k$. 
For $k = 0$ there is only one set with cardinality $0$, the empty set, and $\text{(1)}$ is true.
For the inductive step, assume that $\text{(1)}$ is true for an arbitrary $k$. We have
$\quad n + (k+1) = (n + k) + 1$
and 
$\quad m + (k+1) = (m + k) + 1$
Now adding $1$ to two finite cardinals can be accomplished by finding a singleton set $\{\hat d\}$ disjoint from both of them. So we can extend our proper injection of the sets corresponding to $n + k$ and $m+k$ by mapping $\hat d \mapsto \hat d$. So we have another proper injection.
We leave the other direction to the reader. $\quad \blacksquare$
