EDIT: The following addresses your edits.
You seem to misunderstand the axiom of Replacement. Replacement really does say that given any definable relation $R$, and any set $X$, if for all $x\in X$ there is exactly one $y$ such that $xRy$ (that is: $R$ is really a function), then the set $\{y: \exists x\in X(xRy)\}$ exists. Note that we don't need to talk about a "target class" $C$, either.
Specifically, Replacement is an axiom scheme: for every formula $\varphi$, there is an axiom $$R_\varphi:\quad \forall \overline{a}\forall X[\forall x\in X\exists!y(\varphi(x, y, \overline{a}))\implies \exists z\forall w(w\in z\iff \exists u\in X(\varphi(u, w, \overline{a})))].$$ (There are multiple ways of phrasing this; Collection e.g. is slightly different.) So you do not need to "prove that the function exists". Similarly, you don't need to prove that the target of the function exists.
The example you give is a misunderstanding of model theory. Neither of the sets $\{\emptyset, \{\emptyset\}\}$ and $\{\emptyset,\{\emptyset\}, \{42\}\}$ satisfy Replacement, but not because of the example you describe. In the former, you can't build $\{42\}$ though since the formula defining the function you want relies on having a parameter for $42$. That is, the issue with this relation isn't that it doesn't exist as a set in the first structure, but rather that it isn't even definable in the first structure!
The reason these structures don't satisfy Replacement is that Replacement implies that, as long as there is some set which is nonempty, then every set's singleton exists. Specifically, suppose $D$ satisfies replacement, and $x, y\in D$ with $a\in b$, and $c\in D$ is arbitrary. Then consider the formula $\varphi(x, y)\equiv$"$y=c$" (note that this formula uses a parameter in the structure, so that's fine). Applying Replacement to this formula, with starting set $b$, implies that $\{c\}$ exists.
The proof you've outlined isn't quite correct. Here's how it really goes:
We have the set of natural numbers $\omega$.
By the Powerset axiom and Separation, we can get the set $\mathcal{R}$ of (sets of ordered pairs of naturals).
Again via Separation, we get the subset $\mathcal{W}$ of $\mathcal{R}$ consisting of elements of $\mathcal{R}$ which are well-orderings of a subset of $\omega$: that is, $\mathcal{W}=\{S\in\mathcal{R}$: $S$ is a transitive, antisymmetric, total relation on a subset of $\omega$ with no descending chain$\}$.
Now we observe that for every $S\in\mathcal{W}$, there is exactly one ordinal $\alpha_S$ such that $S$ and $\alpha_S$ have the same order-type. (Note that this isn't obvious! I'll say more about it below, but for now I'll skip over it.)
Apply Replacement! (This is crucial, and without Replacement $\omega_1$ might not exist - see e.g. my answer to this questionthis question.) We get a set $B$ such that $x\in B\iff \exists S\in\mathcal{W}(x=\alpha_S)$. It's now not hard to show that this $B$ is indeed exactly the set of countable ordinals.
Why is it that every $S\in\mathcal{W}$ has a corresponding $\alpha_S$? Well, suppose otherwise. Then we can find an $S$ such that for every $n\in dom(S)$, the strictly smaller order $S_n$ of elements less than $n$ (formally: $S_n$ has domain $dom(S_n)=\{m\in dom(S): m<_{S}n\}$, and ordering $\{(a, b)\in dom(S_n)^2: a<_{S}b\}$) is in order-preserving bijection with some ordinal $\alpha_n$. (This is a good exercise.)
OK, now applying Replacement to $\{S_n: n\in dom(S)\}$ we get a set of countable ordinals $A=\{\alpha_n: n\in dom(S)\}$. But it is easy to show that $A$ is in fact an ordinal, and is in order-preserving bijection with $S$; a contradiction.