DefClassOfOrdinals (3.17, Definition): Class of all ordinal sets(ordinal numbers)

DefClassOfOrdinals (3.17) — Class of all ordinal sets(ordinal numbers)

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

Num Entity Database Record (Vertical Field Table)

Title	Class of all ordinal sets(ordinal numbers) `#DefClassOfOrdinals` `#label-class-of-all-ordinal-sets-ordinal-numbers`
Classification	Definition
Formula	0(On={w\|Ord(w)}) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/on-const.html}{\mathbf{On}} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{w} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/ord-pred.html}{\mathrm{Ord}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{w} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpOn`
Scheme of Types	0`(On={[w@Class.Expression]\|Ord([w@Class.Expression])})`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefClassOfOrdinals`) → · (3.17) · `#DefClassOfOrdinals`