Ordinal Class is Ordinal
Theorem
The Ordinal Class $\On$ is an ordinal.
Proof
This whole proof probably needs to be rewritten from scratch.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by resolving the issues.
To discuss this proof in more detail, feel free to use the talk page.
If you are able to fix this page, then when you have done so you can remove this instance of {{Questionable}} from the code.
If you would welcome a second opinion as to whether your correction is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
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 see any proofs that link to this page, please insert this template at the top.
If you believe that the contents of this page can be reworked to allow ZFC, then you can discuss it at the talk page.
The epsilon relation is equivalent to the strict subset relation when restricted to ordinals by Transitive Set is Proper Subset of Ordinal iff Element of Ordinal.
It follows that:
- $\forall x \in \On: x \subset \On$
We have a problem here since $\On$ is a proper class. The notation $\in $ an $\subseteq$ can naturally be extended to classes, but one must be careful with their use.
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.
The initial segment of the class of ordinals is:
- $\set {x \in \On : x \subset \On}$
What is meant by $\subset$ here: $\subseteq$ or $\subsetneqq$?
Sorry, but "makes no sense" is a bit strong: "initial segment" has been defined on $\mathsf{Pr} \infty \mathsf{fWiki}$ in the context of a well-ordered set, but the term makes perfect sense if defined in the context of a class.
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.
Therefore, by the definition of ordinal, $\On$ is an ordinal.
$\blacksquare$
Sources
- 1971: Gaisi Takeuti and Wilson M. Zaring: Introduction to Axiomatic Set Theory: $7.12$
