Formalization of an intuitive idea to construct a surjection Let $A$ be an arbitrary set and $B$ be any non-empty set. Furthermore, suppose that there is no injection from $A$ to $B$. I want to prove that it follows that there is a surjection from $A$ to $B$.
I have an intuitive argument in mind to prove this, but I do not know how to formalize it. Here is this intuitive argument:
Since $B$ is non-empty, there has to be a function from $A$ to $B$. Let us fix one such a function $f_0\colon A \to B$. The idea is to modify this function $f_0$ using the fact that there is no injection from $A$ to $B$ to  get a surjective function. If $f_0$ is surjective, then we are done. So the interesting case is the case where there are some elements of $B$ that are not in the image of $f_0$. Our job is to modify $f_0$ in such a way that these elements of $B$ are hit too. Let $b_0$ be an element of $B$ which is not in the image of $f_0$. Since $f_0$ is not injective, there are two distinct elements $a_0, {a_0}'\in A$ such that $f_0(a_0)=f_0({a_0}')$. Now we can define a function $f_1\colon A\to B$ as follows: if $a\not = {a_0}'$ then $f_1(a) := f_0(a)$, and if $a={a_0}'$ then $f_1(a):=b_0$. If $f_1$ is surjective, then we are done. Otherwise we can do the same again: Let $b_1$ be an element of $B$ which is not in the image of $f_1$. Since $f_1$ is not injective, there are two distinct elements $a_1, {a_1}'\in A$ such that $f_1(a_1)=f_1({a_1}')$. Now we can define a function $f_2\colon A\to B$ as follows: if $a\not = {a_1}'$ then $f_2(a) := f_1(a)$, and if $a={a_0}'$ then $f_2(a):=b_1$. We can iterate this process a finite number of times. Thus, if the image of $f_0$ is finite, then $f_n\colon A\to B$ is surjective, where $n$ is the cardinality of the image of $f_0$.
Intuitively I think that this argument also works if the image of $f_0$ is countably infinite. Then we can carry out the same process to construct functions $f_1$, $f_2$, $f_3$, $f_4$ and so on. Then the limit $f_\omega$ of this countably infinite process is a surjective function $A\to B$.
Indeed, I also think that this kind of argument always works. We can iterate this process until every element of $B$ is hit, if necessary by constructing functions $f_{\omega + 1}$, $f_{\omega + 2}$, $f_{\omega +3}$, ..., 
$f_{\omega\cdot 2}$, ..., $f_{\omega\cdot 3}$, ..., $f_{\omega\cdot\omega}$, ..., $f_{\alpha}$ (where $\alpha$ is an ordinal number).
How can one formalize this idea and turn it into a rigorous proof?

Transfinite induction allows you to iterate the process you describe, and when combined with the axiom of choice, can be used to make something much like your argument work. (You will have to be a bit careful with how you handle limit ordinals, though.) 
