I've been working on a proof that states if $X$ is an infinite set, then there exists an injection $f: \mathbb{N} \to X$.
Here is the proof I came up with:
Let $X$ be an infinite set.
We will construct the injection $f: \mathbb{N} \to X$ inductively.
For the base case, define $f_1: \{1\} \to X$ by setting $f_1(1)=x_1$ for some $x_1 \in X$.
Now, assume that for some $n \in \mathbb{N}$, we have an injective function $f_n: \{1, \ldots, n\} \to X$.
We can extend $f_n$ to $f_{n+1}: \{1, \ldots, n+1\} \to X$ as follows: $$ f_{n+1}(k) = \begin{cases} f_n(k) & \text{if } k \in \{1, \ldots, n\} \\ x_{n+1} & \text{if } k = n+1 \end{cases} $$ where $x_{n+1}$ is an element of $X$ not in the image of $f_n$. Such an element exists because $X$ is infinite and the image of $f_n$ is finite. By construction, $f_{n+1}$ is injective.
Therefore, by the principle of induction, there exists an injection $f: \mathbb{N} \to X$.
While working on this proof, I realized, that I don't really understand Induction. For example, in the above proof, does induction imply the existence of an injective function $f: \mathbb{N} \to X$ or does it only give me an injective function $f_n: \{1, \ldots, n\} \to X$ for some arbitrary $n \in \mathbb{N}$? In other words, does induction extend the domain of the function from the finite set $\{1, \ldots, n\}$ to the infinite set $\mathbb{N}$?
The way I understand it, the proof constructs infinitely many injective functions $f_1, f_2, f_3 \ldots$ and as $n \to \infty$ the domain should eventually be $\mathbb{N}$.
I would really appreciate if you could help me understand if this is actually the case.
What you have written constructs a function $f_n : \{1, \ldots, n\} \to X$ for each $n \in \mathbb{N}$, with the additional properties that each $f_n$ is injective and for each $n$ we have $f_{n+1}|_{\{1, \ldots, n\}} = f_n$. There's still one more step to do to get a single function $f : \mathbb{N} \to X$. Here it is.
Define $f : \mathbb{N} \to X$ by $f(n) = f_n(n)$. Let's prove that $f$ is injective. Suppose that we have $n$ and $m$ such that $n \neq m$. We'll assume $n < m$, as the other case is essentially identical. Since we are assuming $n < m$, $n$ is in the domain of $f_m$, and $f_m(n) = f_m|_{\{1, \ldots, n\}}(n) = f_n(n)$. We therefore have $f(n) = f_n(n) = f_m(n)$, while $f(m) = f_m(m)$. Since $n \neq m$ and $f_m$ is injective, we have $f_m(n) \neq f_m(m)$ and hence $f(n) \neq f(m)$.
If you are comfortable thinking of functions as sets of ordered pairs, this construction is simply $f = \bigcup_{n=1}^{\infty}f_n$.
To be slightly more general, the fact that each $f_{n+1}$ extends $f_n$ ensures that we can define $f(n)$ to be $f_k(n)$ for any $k$ where $n$ is in the domain of $f_k$, and this definition does not depend on the choice of $k$. So in the example we used $f(n) = f_n(n)$, but we could just as well have chosen $f(n) = f_{n+7}(n)$ without changing anything. Then, to check that a function is injective you only have to consider how it behaves when you give it $n$ and $m$ with $n\neq m$, and you can figure that out by looking at $f_k(n)$ and $f_k(m)$ for some (it doesn't matter which!) $k$ large enough so that $n$ and $m$ are both in the domain of $f_k$.
Many authors would omit mention of the functions $f_n$ altogether and just say that they are recursively defining $f$, but it is probably good to do this carefully at least once while you are learning how it works.