# Maximal Injective Mapping from Ordinals to a Set

## Theorem

Let $F$ be a mapping satisfying the following properties:

The domain of $F$ is $\operatorname{On}$, the ordinal class
For all ordinals $x$, $F \left({x}\right) = G \left({F \restriction x}\right)$.
For all ordinals $x$, if $(A \setminus \operatorname{Im} \left({x}\right) ) \ne \varnothing$, then $G \left({F \restriction x}\right) \in (A \setminus \operatorname{Im} \left({x}\right))$ where $\operatorname{Im} \left({x}\right)$ is the image of the subset $x$ under $F$.
$A$ is a set.

Then there exists an ordinal $y$ satisfying the following properties:

$\forall x \in y: \left({A \setminus \operatorname{Im} \left({x}\right)}\right) \ne \varnothing$
$\operatorname {Im} \left({y}\right) = A$
$F \restriction y$ is an injective mapping.

Note that the first third and fourth properties of $F$ are the most important. For any mapping $G$, a mapping $F$ can be constructed satisfying the first two properties using transfinite recursion.

## Proof

This page is beyond the scope of ZFC, and should not be used in anything other than the theory in which it resides.

If you believe that the contents of this page can be reworked to allow ZFC, then you can discuss it at the talk page.

Set $B$ equal to the class of all ordinals $x$ such that $\left({A \setminus \operatorname{Im} \left({x}\right)}\right) \ne \varnothing$.

Assume $B = \operatorname{On}$.

Then:

 $\displaystyle B = \operatorname{On}$ $\implies$ $\displaystyle \forall x: F \left({x}\right) = G \left({F \restriction x}\right)$ by definition of $B$ $\displaystyle$ $\implies$ $\displaystyle \forall x: G \left({F \restriction x}\right) \in \left({A \setminus \operatorname{Im}(F)}\right)$ by hypothesis

This contradicts the fact that $A$ is a set.

Therefore $B \subsetneq \operatorname{On}$.

Because $B$ is bounded above, $\bigcup B \in \operatorname{On}$.

By Union of Ordinals is Least Upper Bound, the union of ordinals is the least upper bound of $B$.

Setting $\bigcup B = x$:

$(1): \quad \left({A \setminus \operatorname{Im} \left({x}\right)}\right) = \varnothing \land \forall y \in x: \left({A \setminus \operatorname{Im} \left({y}\right)}\right) \ne \varnothing$

The first condition is satisfied.

$(2): \quad A \subseteq \operatorname{Im} \left({x}\right)$

Take any $y \in \operatorname{Im} \left({x}\right)$.

Then:

 $\displaystyle y \in \operatorname{Im} \left({x}\right)$ $\implies$ $\displaystyle \exists z \in x: \left({y = F \left({z}\right)}\right)$ Definition of Image of Element $\displaystyle$ $\implies$ $\displaystyle \exists z: \left({y = F \left({z}\right) \land \left({A \setminus \operatorname{Im} \left({z}\right)}\right) \ne \varnothing}\right)$ Equation $(1)$ $\displaystyle$ $\implies$ $\displaystyle \exists z: \left({y = F \left({z}\right) \land F \left({z}\right) \in \left({A \setminus \operatorname{Im} \left({z}\right)}\right)}\right)$ by hypothesis $\displaystyle$ $\implies$ $\displaystyle y \in A$

This means that:

$\operatorname{Im} \left({x}\right) \subseteq A$

Combining with $(2)$:

$\operatorname{Im} \left({x}\right) = A$

$F$ is a mapping, so $\left({F \restriction x}\right)$ is a mapping.

Take any $y, z \in x$ such that $y$ and $z$ are distinct.

Without loss of generality, allow $y \in z$ (justified by Ordinal Membership Trichotomy).

 $\displaystyle y \in z \land z \in x$ $\implies$ $\displaystyle F \left({y}\right) \in \operatorname{Im} \left({z}\right) \land F \left({z}\right) \in \left({A \setminus \operatorname{Im} \left({z}\right)}\right)$ by hypothesis $\displaystyle$ $\implies$ $\displaystyle F \left({y}\right) \in \operatorname{Im} \left({z}\right) \land F \left({z}\right) \notin \operatorname{Im} \left({z}\right)$ Definition of Set Difference $\displaystyle$ $\implies$ $\displaystyle F \left({y}\right) \ne F \left({z}\right)$

From this, we may conclude that $F$ is injective.

$\blacksquare$