ZFC Addition Function 
Prove that for each $m \in \Bbb N$, there exists a unique $ f_m: \Bbb N \rightarrow \Bbb N$, such that $f_m(0)=m$ and $\forall n \in \Bbb N, f_m(S(n))=S(f_m(n))$. Where $S(n)$ denotes the successor of $n$, namely: $S(n)=n \cup \{n\}$.

The proof follows from application of the recursion theorem, however, I am trying to see if I could prove it from the Axioms directly. I am new to the subject of ZFC, so please bear with me.
By Axiom of Choice, considering the indexed family of sets $\{\Bbb N\}_{i \in \Bbb N}$ as follows:
$$\prod\{\Bbb N\}_{i \in \Bbb N} \neq \emptyset=\{f:\Bbb N \rightarrow \Bbb N\}$$
Hence the set of all possible functions $f:\Bbb N \rightarrow \Bbb N$ exists and is nonempty.
By Axiom of Union, the following set exists:
$$\bigcup \prod \{\Bbb N\}_{i \in \Bbb N}=\{z:\exists f \in \prod \{\Bbb N\}_{i \in \Bbb N} \;z \in f \}$$
which is the set of all possible ordered pairs.
By Axiom of Seperation, the following set exists:
$$f_m= \biggr\{z \in \bigcup \prod \{\Bbb N\}_{i \in \Bbb N}: (x(z)=0 \implies y(z)=m)\; \land \;\biggr(\forall n \in \Bbb N \;\;\; y(S(x(z)))=S(y(x(z)))\biggr) \biggr\}$$
The variable used in the quantifier $z$ is an ordered pair, where $x(z)$ and $y(z)$ denote the $x$ and $y$ components respectively. To the right of the colon, we have a formula that selects all the ordered pairs satisfying the criterion in the question. Hence, we have demonstrated that such $f_m$ exists.
Is this method valid? I am really unsure: when we invoke the Axiom of Choice, we simply state that the Generalised Cartesian Product or simply  the set of all functions $f:\Bbb N 
\rightarrow \Bbb N$ is nonempty, but we don't say anything about whether or not the given $f_m$ is a possible element of the product. So then we might end up with $f_m$ being the empty set when we apply the Axiom Schema of Separation.
I also have an additional concern, if you look at the criterion used when applying the Axiom of Separation, we check for $y(S(x(z)))$, which we wouldn't know unless we knew the successive ordered pair. This sounds problematic, however I've never seen a similar scenario where we consider the successive element, the existence of which is yet to be determined, as part of the formula.
 A: First off - this isn't a correctness issue, but doesn't this seem like a roundabout way to construct the set of ordered pairs? Why not just use the Cartesian product on the indexed family $\{\mathbb{N}\}_{i \in 2}$? This is related to one of your concerns - you're worried that $f_m$ might not be a member of that set of all functions, but notice that you discarded that set immediately. You're not drawing $f_m$ out as an element of that set, you're extracting it as a subset of the set of ordered pairs.
Unrelatedly: Your concern is essentially correct, though. Separation guarantees that the thing you're calling $f_m$ exists, but does not guarantee any of the following:

*

*$f_m$ is nonempty.

*$f_m$ is total (i.e., is defined on all of $\mathbb{N}$).

*$f_m$ is in fact a function.

You should prove each of these separately (although the first two can be bundled together). In other words, given an $a$, show that there's at least one pair $(a,b)$ meeting the described condition; then show that no other pair will work.
A: If you've defined ordinal addition, you can note that you can take $f_m(x) = m + x$. Uniqueness follows pretty easily by induction.
Your "proof" is flawed, incomplete, and convoluted. Here's a cleaner way to prove this.
General case: suppose we have $m \in B$ and $g : B \to B$. Then there is a unique $f : \mathbb{N} \to B$ such that $f(0) = m$ and for all $n \in \mathbb{N}$, $f(S(n)) = g(f(n))$.
Proof:
We say $f$ is a "good function" if
(1) $f$ is a function $D \to B$ where $D \subseteq \mathbb{N}$
(2) If $0 \in D$ then $f(0) = 0$.
(3) For every $n \in \mathbb{N}$, if $S(n) \in D$ then $n \in D$ and $f(S(n)) = g(f(n))$.
Claim: for every $n \in \mathbb{N}$, there is a unique $b \in B$ such that there's some good $f$ where $f(n) = b$ (and of course $f(n)$ is defined).
Proof: induction.
Base case: We can clearly define $f : \{0\} \to B$ by $f(0) = m$; this proves existence. Uniqueness follows from the fact that whenever $f(0)$ is defined, it must equal $m$ by the definition of a "good function."
Inductive step: let $w \in B$ be the unique such value corresponding to $n$, and let $f$ be a "good function" such that $f(n) = w$. Define $h = f \cup \{S(n), g(w)\}$. We see that $h$ is a good partial function, that $h(S(n))$ is defined, and that $h(S(n)) = g(h(n))$; existence is thus proved. Note that in some texts, a function $f$ is given as the ordered pair $(R, B)$ where $R \subseteq D \times B$; in this case, a minor change would be needed but nothing serious.  And of course, for any good function $h$ such that $h(S(n))$ is defined, we would have $h(S(n)) = g(h(n)) = g(w)$; uniqueness is also thereby proved.
Then we can define a function $f : \mathbb{N} \to B$ by $f(n) = $ the unique $b \in B$ such that there is a good $h$ where $h(n)$ is defined and $h(n) = b$. We see that it must be the case that $f(0) = m$ and that for all $n \in \mathbb{N}$, $f(S(n)) = g(f(n))$. Thus, the existence of the $f$ follows.
Finally, suppose that there is some other $h : \mathbb{N} \to B$ such that $g(0) = 0$ and for all $n$, $h(S(n)) = g(h(n))$. Then $h$ is a good function; then for every $n$, $h(n) = f(n)$; then $h = f$. Thus, uniqueness of the $f$ follows.
Clearly, your problem is just a special case of this.
Edit: going into more detail on the reasons why the questioner's attempted proof fails.
Firstly, you almost certainly don't need to demonstrate that $\mathbb{N} \to \mathbb{N}$ and $\mathbb{N}^2$ are sets, and the way you've done so is very roundabout and probably circular. Surely your textbook would have gone over more general versions of these facts first. I recommend you look over the proofs that such sets of functions and Cartesian products are well-defined. The axiom of choice has nothing to do with either.
Secondly, your construction
$$f_m= \biggr\{z \in \bigcup \prod \{\Bbb N\}_{i \in \Bbb N}: (x(z)=0 \implies y(z)=m)\; \land \;\biggr(\forall n \in \Bbb N \;\;\; y(S(x(z)))=S(y(x(z)))\biggr) \biggr\}$$
makes little sense. Let us rewrite it in more standard notation as
$$f_m= \biggr\{(a, b) \in \mathbb{N}^2 : (a=0 \implies b=m)\; \land \;\biggr(\forall n \in \Bbb N \;\;\; y(S(a))=S(y(a))\biggr) \biggr\}$$
Hopefully it is clear now that since your construction involves taking the components of the natural number $a$ as if it were an ordered pair shows that the construction doesn't make much sense.
