Note that you need to use the axiom of choice at some point there. Otherwise the definition of "finite" which you are using (also known as Dedekind-finiteness) may include sets which are strictly larger than all the natural numbers, but not larger than $\Bbb N$.
So here you need to assume that if a set is infinite, then it has a countably infinite subset (which is precisely where you are using the axiom of choice). But this makes an easy way of finding an injection which is not surjective. Just note that we can find such function for $\Bbb N$.
To answer your last question first, if $f\in Y^X$, the notation $f^{-1}$ has two possible meanings. If $f$ is a bijection, it can denote the inverse function to $f$. In all cases, however, it can be applied to subsets of $Y$: for any $A\subseteq Y$,
$$f^{-1}[A]=\{x\in X:f(x)\in A\}\,.$$
In particular, $f_4^{-1}[\{1\}]$ is $\{x_1,x_2\}$ in your example. (See Tao’s Definition $\mathbf{3.4.4}$.)
It should be intuitively clear that
$$\{Y:Y\subseteq X\}=\left\{f^{-1}[\{1\}]:f\in\{0,1\}^X\right\}\,,\tag{1}$$
so we have two tasks: we must show that $(1)$ is actually true, and we must show that the object on the righthand side of $(1)$ is a set.
It’s for the second task that we want replacement. For each $f\in\{0,1\}^X$ let $P(f,y)$ be the statement
$$y=\{x\in X:f(x)=1\}\,.$$
It is straightforward to prove that for each $f$ in $X^{\{0,1\}}$ there is a unique $y$ such that $P(f,y)$ is true, and that $y$ is evidently $f^{-1}[\{1\}]$, so we can apply replacement to conclude that
$$\left\{f^{-1}[\{1\}]:f\in\{0,1\}^X\right\}$$
is a set.
I’ll leave it to you to prove $(1)$.
Best Answer
The proof of the title is logical. If there exists a bijection $f$ between $X$ and a finite set $F$, then we say that $\forall f\in F,\exists x\in X:f(x)=f$, and $\forall x\in X,\exists f\in F:f(x)=f$. Thus, there is a one to one correspondence between elements of $X$ and $F$. Therefore, if $F$ is finite, $X$ is finite, i.e., it has $n$ elements.
In axiomatic set theory, the existence of a bijection $X\to F$ is taken to be the definition of "same number of elements".