Question about cardinals in ZF In Lévy's basic set theory refers a theorem of Bernstein as exercise problem:

Theorem. (Bernstein) Let $\mathfrak{a,b}$ be cardinals. If $\mathfrak{a+a=a+b}$, then $\mathfrak{b\le a}$.

I try to prove it using the following theorem:

Theorem. If $\mathfrak{a+c=b+c}$ then there are cardinals $\mathfrak{a',b',d}$ such that $\mathfrak{a'+c=b'+c=c}$, $\mathfrak{a=a'+d}$ and $\mathfrak{b=b'+d}$.

If we assume the choice then this theorem is quite trivial. However I want to prove it without choice. Any hint or help would be appreciated.

Lets say you have a bijection $\mathfrak{b}\cup \mathfrak{a}\rightarrow \mathfrak{a}\times\{0,1\}$ where we assume that $\mathfrak{b}$ and  $\mathfrak{a}$ are disjoint.
Consider the sequence
$$b\rightarrow (a_1,0)$$ 
$$a_1\rightarrow (a_2,0)$$ 
$$a_2\rightarrow (a_3,0)$$ 
$$\vdots$$
$$a_{n-1}\rightarrow (a_n,1)$$
Let us define $a_1, \ldots a_{n-1}$ to be the sequence associated with $b$ and $a_n$, the terminal element of $b$.
Note that the sequences associated to distinct $b$'s are disjoint, and the terminal elements are also unique, which can be seen just by back tracking. However the terminal element of one $b$ can belong to the associated sequence of another.
Further there may be some $b$ with an infinite ($\omega$ type) associated sequence and no terminal element. 
Let $b$ be such an element with infinite associated sequence $a_1, a_2 \ldots$
Assume that each $a_i$ is the terminal element of $b_i$ (the case where one $a_i$ is not a terminal element I leave to you) Now define $f(b)=a_1$ and $f(b_i)=a_{i+1}$.  So for each $b$ with infinite sequence we make this definition. Since the associated sequences are disjoint this is well defined.
There may be some elements of $\mathfrak{b}$ left over we then send them to their terminal elements. One can see that this is a well defined injection.
To summarize, an element $b$ is mapped to its terminal element, except if this terminal element belongs to the infinite associated sequence of another element, in which case it is mapped to the next element in the sequence.  
