Is the inverse of surreal numbers actually well-defined?

J.Conway wrote in his book "On numbers and games" (1st edition, 1976) on p. 66

> It seems to us, however, that mathematics has now reached the stage where formalization within some particular axiomatic set theory is irrelevant, even for foundational studies.

I happen to disagree. In fact, I'm having some fun formalizing mathematics in the Mizar system, which has just [one article][1] on Conway games yet. I want to find out if further formalization would be fruitful, i.e. if the operations defined in the book can be formalized at all. The cited article only defines $-x$ for a game $x$, but gives a pretty good idea how to deal with the highly inductive nature of games and I'm certain I could formalize addition and multiplication. What bothers me is the definition of $y=\frac{1}{x}$, given by $$y=\left\{\left.0,\frac{1+(x^R-x)y^L}{x^R},\frac{1+(x^L-x)y^R}{x^L}\right|\frac{1+(x^L-x)y^L}{x^L},\frac{1+(x^R-x)y^R}{x^R}\right\}$$
for $x$ positive and only positive $x^L$ considered, which is needed for defining division. Conway, after giving this definition on p.21, writes himself

> Note that expressions involving $y^L$ and $y^R$ appear in the definition of $y$. It is this that requires us to "explain" the definition. The explanation is that we regard these parts of the definition as defining new options for $y$ in terms of old ones.

In a footnote, the rather trivial example of $\frac{1}{3}=\{0,\frac{1}{4},\frac{5}{16},\ldots|\frac{1}{2},\frac{3}{8},\ldots\}$ is given to show "how the definition works".

I can't see why $y$ is well defined in general. For example, given two uncountable cardinals $\alpha<\beta$ I'm having a hard time seeing how $\frac{1}{\beta-\alpha}$ should be computed. The emphasis here lies on "uncountable".

Claus Tøndering gave a seemingly equivalent definition of the inverse [here on p.44][2] (if the definition should not be equivalent, please point out why). He defines $y$ through $y^L$ and $y^R$ as such:
$$0\in y^L$$
$$z\in y^L \Rightarrow \tfrac{1+(x^R-x)z}{x^R}\in y^L, \tfrac{1+(x^L-x)z}{x^L}\in y^R$$
$$z\in y^R \Rightarrow \tfrac{1+(x^L-x)z}{x^L}\in y^L, \tfrac{1+(x^R-x)z}{x^R}\in y^R$$

This is still "too" recursive to be formalized. One of my problems is that I can't comprehend the cardinality of $y^L$ and $y^R$. I mean, I could define $y^L_0 = \{0\}, y^R_0 = \{\}$ and for $n\in\mathbb{N}, n>0$ change Tønderings definitions to $z\in y^L_{n-1} \Rightarrow \ldots\in y^L_n$ and so on (or better: $$y^L_n = \left\{\left.\tfrac{1+(x^R-x)z}{x^R}\right|z\in y^L_{n-1}\right\}\cup\left\{\left.\tfrac{1+(x^L-x)z}{x^L}\in y^L \right|z\in y^R_{n-1}\right\}$$ and $y^R$ analogue) and conjecture $$y^L = \{0\}\cup\bigcup_{n\in\mathbb{N}} y^L_n,\quad y^R = \bigcup_{n\in\mathbb{N}} y^R_n$$

**Here is my problem:** I really doubt I could prove that. First off, I'm having trouble believing the equality holds, that I could miss something by merely having a countable union. Secondly, $y^L$ and $y^R$ are required to be sets and I can image how they accidentally could become classes this way with some $x$ nefarious enough (maybe $x=\beta-\alpha$ is enough already?), because maybe the set generation process never stops at a certain day. I get couldn't information about this topic at all. In papers about surreal numbers either they are just given like here without further doubt or not explicitly given at all. Some papers, like these from Philip Ehrlich, go deeper into cardinality or other theories above my understanding, so if the issue would be resolved there, I wouldn't have noticed.

On the matter of the $y^L_n$ and $y^R_n$ being sets, Conway writes
> **Theorem 10.** *We have (i) $xy^L<1<xy^R$ for all $y^L,y^R$.*<br>
> *(ii) $y$ is a number.* [(iii) and (iv) left out]<br>
> *Proof.* We observe that the options of $y$ are defined by formulae of the form $$y''=\frac{1+(x'-x)y'}{x'}$$ where $y''$ is an earlier option of $y$, and $x'$ some non-zero-option of $x$. This formula can be written $$1-xy'' = (1-xy')\frac{x'-x}{x'}$$ which shows that $y''$ satisfies (i) if $y'$ does. Plainly $0$ does. Part (ii) now follows, since we cannot have any inequality $y^L\geq y^R$. [...]

As far as my understanding goes, with "$y$ is a number" he means "if $y$ is a game, then it's a number", as this proof (directly following the remark after the definition) does not indicate the sethood of $y^L$ or $y_R$ in my eyes.

  [1]: http://mizar.org/version/current/html/cgames_1.html "Conway's Games and Some of Their Basic Properties"
  [2]: http://share.dschola.it/giordanobruno/physic@/100%20PAROLE%20PERla%20scienza/Infinito/Surreal%20Numbers%20-%20Tondering.pdf "Surreal Numbers - An introduction"