Consider surreal numbers as signed ordinals $\alpha\rightarrow\{-,+\}$. Suppose we already have $x<y$ defined for any two surreals, as well as $F|G$ as the simplest surreal $z$ strictly between the surreal-membered sets $F$ and $G$. We also have the canonical representation $(F(z),G(z))$ such that $F(z)|G(z) = z$.
Given these, how does one formally define addition on the surreal numbers?
The slightly informal way is to say that $$a+b:=\left.\bigcup_{x\in F(a),y\in F(b)}\{a+y,x+b\}\right|\bigcup_{x\in G(a),y\in G(b)}\{a+y,x+b\}$$ and reassure the reader that induction on the natural sum takes care of everything. I need that formalized though.
My idea is the following: For all surreals until day $\alpha$ define $f_\alpha$ by $$f_\alpha(a,b):=\left.\bigcup_{x\in F(a),y\in F(b)}\{f_\alpha(a,y),f_\alpha(x,b)\}\right|\bigcup_{x\in G(a),y\in G(b)}\{f_\alpha(a,y),f_\alpha(x,b)\}.$$ So $f_\alpha$ is defined on $S_\alpha\times S_\alpha$, i.e. a proper function.
My problem then is how to ensure that $f_\alpha$ exists. It seems like transfinite induction is needed for $\alpha\geq \aleph_0$, but I'm bad at transfinite induction.