Lexicographic Order Initial Segments
 It has been suggested that this article or section be renamed:
|
There is a definition and a proof here -- they need to be separated out.
Until this has been finished, please leave {{refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
If you are fairly certain that there are none, please remove {{proofread}} from the code.
Theorem
Let $\operatorname{Le}$ denote the lexicographic order for the set $\left({\operatorname{On} \times \operatorname{On} }\right)$.
Let the ordinal number $1$ denote the successor of $\varnothing$.
Then the initial segment of $ \left({1, \varnothing}\right)$ with respect to the lexicographic order $\operatorname{Le}$ is a proper class.
This initial segment shall be denoted $\left({\operatorname{On} \times \operatorname{On} }\right)_{\left({1, \varnothing}\right)}$.
The connection between these two statements is not clear.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
Proof
Define the mapping $F: \operatorname{On} \to \operatorname{On} \times \operatorname{On}$ as:
- $\forall x \in \operatorname{On}: F \left({x}\right) = \left({\varnothing, x}\right)$
Then, $F: \operatorname{On} \to \left({\operatorname{On} \times \operatorname{On}}\right)_{\left({1, \varnothing}\right)}$, since $\varnothing < 1$.
The above statement does not make linguistic sense. The entity $F: \operatorname{On} \to \left({\operatorname{On} \times \operatorname{On} }\right)_{\left({1, \varnothing}\right)}$ is a noun, and there is no verb in the "then" clause.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
That is, $F$ is a mapping from the class of all ordinals to the initial segment of $\left({1, \varnothing}\right)$ with respect to lexicographic order.
By Equality of Ordered Pairs, $F$ is injective.
But since $\operatorname{On}$ is a proper class by the Burali-Forti Paradox, the initial segment of $\left({1, \varnothing}\right)$ is a proper class as well.
$\blacksquare$
Sources
- 1971: Gaisi Takeuti and Wilson M. Zaring: Introduction to Axiomatic Set Theory: $\S 7.54 \ (2)$
