Theorem: Maximal Injective Mapping from Ordinals to a Set

Let $F$ be a mapping satisfying the following properties:
{{explain|What is $G$?}}
:The domain of $F$ is $\On$, the class of all ordinals
:For all ordinals $x$, $\map F x = \map G {F \restriction x}$.
:For all ordinals $x$, if $A \setminus \Img x \ne \O$, then $\map G {F \restriction x} \in A \setminus \Img x$ where $\Img x$ 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: A \setminus \Img x \ne \O$
:$\Img y = 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 the First Principle of Transfinite Recursion.

Proof:
Set $B$ equal to the class of all ordinals $x$ such that $A \setminus \Img x \ne \O$.
Assume $B = \On$.  
Then:
{{begin-eqn}}
{{eqn | l = B
      | r = \On
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | l = \map F x
      | r = \map G {F \restriction x}
      | c = Definition of $B$
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | l = \map G {F \restriction x}
      | o = \in
      | r = A \setminus \Img F
      | c = {{hypothesis}}
}}
{{end-eqn}}
By Condition for Injective Mapping on Ordinals, $A$ is a proper class.
This contradicts the fact that $A$ is a set.
Therefore $B \subsetneq \On$.
Because $B$ is bounded above, $\bigcup B \in \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 A \setminus \Img x = \O \land \forall y \in x: A \setminus \Img y \ne \O$
The first condition is satisfied.
In addition:
:$(2): \quad A \subseteq \Img x$
Take any $y \in \Img x$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \Img x
}}
{{eqn | ll= \leadsto
      | q = \exists z \in x
      | l = y
      | r = \map F z
      | c = {{Defof|Image of Element under Mapping}}
}}
{{eqn | ll= \leadsto
      | q = \exists z
      | l = y
      | r = \map F z
      | c = Equation $(1)$
}}
{{eqn | lo= \land
      | l = A \setminus \Img z
      | o = \ne
      | r = \O
}}
{{eqn | ll= \leadsto
      | q = \exists z
      | l = y
      | r = \map F z
      | c = {{hypothesis}}
}}
{{eqn | lo= \land
      | l = \map F z
      | o = \in
      | r = A \setminus \Img z
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = A
}}
{{end-eqn}}
This means that:
:$\Img x \subseteq A$
Combining with $(2)$:
:$\Img x = A$
$F$ is a mapping, so $F \restriction x$ is a mapping. 
Take any $y, z \in x$ such that $y$ and $z$ are distinct.
{{WLOG}}, allow $y \in z$ (justified by Ordinal Membership Trichotomy).
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = z
}}
{{eqn | lo= \land
      | l = z
      | o = \in
      | r = x
}}
{{eqn | ll= \leadsto
      | l = \map F y
      | o = \in
      | r = \Img z
      | c = {{hypothesis}}
}}
{{eqn | lo= \land
      | l = \map F z
      | o = \in
      | r = A \setminus \Img z
}}
{{eqn | ll= \leadsto
      | l = \map F y
      | o = \in
      | r = \Img z
      | c = {{Defof|Set Difference}}
}}
{{eqn | lo= \land
      | l = \map F z
      | o = \notin
      | r = \Img z
}}
{{eqn | ll= \leadsto
      | l = \map F y
      | o = \ne
      | r = \map F z
}}
{{end-eqn}}
From this, we may conclude that $F$ is injective.
{{qed}}