Order Isomorphism between Ordinals and Proper Class/Lemma

Lemma for Order Isomorphism between Ordinals and Proper Class

Suppose the following conditions are met:

Let $A$ be a class.

We allow $A$ to be a proper class or a set.

Let $\left({A, \prec}\right)$ be a strict well-ordering.

Let every $\prec$-initial segment be a set, not a proper class.

Let $\operatorname{Im} \left({x}\right)$ denote the image of a subclass $x$.

Let $G$ equal the class of all ordered pairs $\left({x, y}\right)$ satisfying:

$y \in \left({A \setminus \operatorname{Im} \left({x}\right)}\right)$
The initial segment $A_y$ of $\left({A, \prec}\right)$ is a subset of $\operatorname{Im} \left({x}\right)$

Let $F$ be a mapping with a domain of $\operatorname{On}$.

Let $F$ also satisfy:

$F \left({x}\right) = G \left({F \restriction x}\right)$

Then:

$G$ is a mapping
$G \left({x}\right) \in \left({A \setminus \operatorname{Im} \left({x}\right)}\right) \iff \left({A \setminus \operatorname{Im} \left({x}\right)}\right) \ne \varnothing$

Note that only the first four conditions need hold: we may construct classes $F$ and $G$ satisfying the other conditions using transfinite recursion.

Proof

 $\displaystyle$  $\displaystyle \left({\left({x, y}\right) \in G \land \left({x, z}\right) \in G}\right)$ $\displaystyle$ $\implies$ $\displaystyle \left({y \in \left({A \setminus \operatorname{Im} \left({x}\right)}\right) \land z \in \left({A \setminus \operatorname{Im} \left({x}\right)}\right)}\right)$ Definition of $G$ $\displaystyle$ $\implies$ $\displaystyle \left({y \notin A_z \land y \notin A_y}\right)$ $A_y$ is disjoint with $\left({A \setminus \operatorname{Im} \left({x}\right)}\right)$. Same with $A_z$. $\displaystyle$ $\implies$ $\displaystyle \left({y \not \prec z \land z \not \prec y}\right)$ Definition of initial segment $\displaystyle$ $\implies$ $\displaystyle y = z$ $\prec$ is a strict well-ordering

Therefore, we may conclude, that $G$ is a single-valued relation and therefore a mapping.

For the second part:

 $\displaystyle$  $\displaystyle \left({A \setminus \operatorname{Im} \left({x}\right)}\right) \ne \varnothing$ $(1):\quad$ $\displaystyle$ $\implies$ $\displaystyle \exists y \in \left({A \setminus \operatorname{Im} \left({x}\right)}\right): \left({A \cap A_y}\right) \setminus \operatorname{Im} \left({x}\right) = \varnothing$ Proper Well-Ordering Determines Smallest Elements $\displaystyle$ $\implies$ $\displaystyle G \left({x}\right) = y$ Conditions are satisfied for $\left({x, y}\right) \in G$. Follows from first part. $\displaystyle$ $\implies$ $\displaystyle G \left({x}\right) \in \left({A \setminus \operatorname{Im} \left({x}\right)}\right)$ equation $(1)$, $y \in \left({A \setminus \operatorname{Im} \left({x}\right)}\right)$

Furthermore:

$G \left({x}\right) \in \left({A \setminus \operatorname{Im} \left({x}\right)}\right) \implies \left({A \setminus \operatorname{Im} \left({x}\right)}\right) \ne \varnothing$ by the definition of nonempty.

$\blacksquare$