ThmOrdinalsIsOrdinal (3.18, Theorem): The class of all ordinals is an ordinal class

Standalone kernel entity record from 3. Set/Class-Theoretic Foundations (3.01–3.78) — View in Complete Entity Database (#ThmOrdinalsIsOrdinal) →

Formula Display:
Proof Trees:

ThmOrdinalsIsOrdinal (3.18) — The class of all ordinals is an ordinal class

Morse-Kelley / Von Neumann-Bernays-Gödel class comprehension, sethood, ordinals, Dunaev pairs, cardinals, universes, and reflection.

Num Entity Database Record (Vertical Field Table)
3.18
Title The class of all ordinals is an ordinal class #ThmOrdinalsIsOrdinal #label-the-class-of-all-ordinals-is-an-ordinal-class
Classification Theorem
Formula
0Ord(On)
0\(\href{../symbols/ord-pred.html}{\mathrm{Ord}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/on-const.html}{\mathbf{On}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST TpOrd
Scheme of Types 0Ord(On)
Verification Verified (Kernel) · Standalone Entry (ThmOrdinalsIsOrdinal) → · (3.18) · #ThmOrdinalsIsOrdinal