Order Isomorphism between Ordinals and Proper Class/Lemma

From ProofWiki
Jump to navigation Jump to search

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$


Also see


Sources