Inductive definition of a function in a formal language $
\newcommand{\emt}{\varnothing}
\newcommand{\N}{\mathbb{N}}
\newcommand{\dom}{\mathrm{dom}}
$
My new formal proof is updated at the end of the post:
I am trying to show the following proposition:
Let $I_n = \{i \in \N ~|~ i \le n \}$ and $X$ be a nonempty set.
Claim: If there is no bijection from $I_n$ onto $X$ for all $n \in \N$, then there is an injection from $I_n $ into $X$. In symbols,
$$
\forall n\in \N: |I_n| \neq |X|
\Rightarrow
\exists f \in \N \to X: f \text{ is an injection}
$$
Attempted informal proof:
Suppose $\forall n\in \N: |I_n| \neq |X|$. Because $X$ is nonempty, there is $x_1 \in X$. Suppose $X = \{x_1\}$. Then, we can construct $\{(1,x_1)\} = I_1 \times X$ that is a bijection from $I_1 $ to $X$, which is a contradiction. Therefore, there is $x_2 \in X$ that is different from $x_1$. Let $X = \{x_1, x_2\}$. We can construct the bijection $\{(1,x_1), (2, x_2)\}$ from $I_2$ onto $X$. This is a contradiction. We can repeat this process indefinitely, which implies the existence of an injection from $\N$ to $X$ (I think the conclusion is not rigorously derived though).
However, the problem is, I want the proof to be expressed in a formal first-order language. I've seen that some people call the process an inductive definition of a function. For instance,

An injection $g: \N \to X$ can be defined inductively.

But I haven't seen the formal definition of the inductive definition, and the underlying logic behind this is not clear to me. How can we express the defining process of $g$ and is it possible in ZFC? I prefer the process to be expressed symbolically if possible.
This question is motivated by the answers by

*

*Figurinha

*Shore.

Update:
Combining the comment of Schweber and the answers by Couchy, and Scott, I tried to make a proof by myself. This proof uses DC. To make use of DC, the key is to define a set $Y$ and an entire relation $R$ on the set.
Let
$$
Y = \{f \subseteq \N \times X~|~ f \text{ is an injection}, \exists n \in \N : I_n = \dom f\}\\
R = \{(f, g) \in Y \times Y ~|~ f \subsetneq g\}
$$
We have to show that $Y$ is nonempty and
$$
\forall f \in Y: \exists g \in Y: f R g
$$
$Y$ is nonempty because $X \neq \emt$ and $\{(1,x_1)\} \in Y$ for some $x_1 \in X$. Let $f \in Y$. Then, $f$ is an injection and there is $n \in \N$ such that $I_n = \dom f$. We have now two possible cases: $f[I_n] = X$ or $f[I_n] \subsetneq X$. The former directly yields a contradiction because $f$ becomes a bijection between $I_n$ and $X$. By the latter, there is $z \in X$ that is not in $f[I_n]$. We can now construct the function $g = f \cup \{(n+1, z)\}$. It is easy to show that $g$ is an injection, from $I_{n+1}$ to $X$, strictly larger than $f$. Therefore, we have $f R g$.
Now, by DC, there is a sequence $h: \N \to Y$ such that $h_n R h_{n+1}$ for all $n \in \N$. Construct a function $l: \N \to X$ such that
$$
\forall n \in \N: l(n) = h_n(\max \dom h_n)
$$
It is easy to see that $l$ is injective.
Is this acceptable?
 A: Any set $X$ that has a well-ordering can be inducted on. In particular the set of natural numbers is well-ordered.
For a set to be well ordered means every subset has a least element.
If a set is well-ordered, we can prove the following induction principle:

$(\forall x.(\forall y<x. \phi(y))\implies \phi(x))\implies (\forall x.\phi (x))$.

Indeed consider the set $N = \{x\in X\ |\ \neg\phi(x)\}$ then because $X$ is well-ordered, $N$ has a least element $x_0$, but now for any $y < x_0$, $\phi(y)$ because $y\not\in N$. But by our hypothesis, this implies $\phi(x_0)$, a contradiction. This means that $N$ is empty, and therefore $\forall x. \phi(x)$.

Now, we can obtain the following recursion theorem:

Suppose that for any $x\in X$, whenever there exists a function $f_x : X_{<x}\to Y$ (where $X_{<x} := \{y\in X\ |\ y < x\}$) we can extend it to a function $\hat f_x : X_{\leq x}\to Y$, then there exists a function $f : X\to Y$ whose restriction to $X_{<x}$ is $f_x$

by applying (I'll spare the details) the induction principle above with
$$\phi(x) := (\exists f_x:X_{<x}\to Y. \forall y<x. f_x\text{ is compatible  with }f_y)$$
where $f_x$ is compatible with $f_y$ if $f_x$ restricted to $X_{<y}$ agrees with the values of $f_y$.

Now the well-ordering principle says the the natural numbers is well-ordered, thus we can apply the above induction and recursion principles.
For the natural numbers, this simply means that if we know how to extend any function $f_n:\mathbb N_{<n}\to Y$ to a function $\hat f_n:\mathbb N_{\leq n}\to Y$, then we obtain $f : \mathbb N\to Y$.
Note that the base case is given by extending $f_0 : \mathbb N_{<0}\to Y$, which vacuously exists, to a function $\hat f_0: \mathbb N_{\leq 0}\to Y$, which is equivalent to selecting a single element of $Y$.
A: An more concrete approach is to assume you have a function for every set $Y$:
$\newcommand{\N}{\mathbb N}$
$$\texttt{rec}_Y : Y\to (\N\to Y\to Y)\to\N\to Y$$
satisfying the following equalities:
$$\texttt{rec}_Y(z,s,0) = z\\
\texttt{rec}_Y(z,s,n+1) = s(n,\texttt{rec}(z,s,n)).$$
Then any recursive function from $\N$ to $Y$ can be defined with $\texttt{rec}_Y$ by specifying its first two arguments.
The existence of $\texttt{rec}_Y$ can be proved using the method I described in my other answer (the recursion theorem).
