ThmOrdinalsInductive (3.60, Theorem): Class of all ordinal numbers is successor-inductive (Peano-inductive)

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

Formula Display:
Proof Trees:

ThmOrdinalsInductive (3.60) — Class of all ordinal numbers is successor-inductive (Peano-inductive)

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.60
Title Class of all ordinal numbers is successor-inductive (Peano-inductive) #ThmOrdinalsInductive #label-class-of-all-ordinal-numbers-is-successor-inductive-peano-inductive
Classification Theorem
Formula
0Ind(On)
0\(\href{../symbols/ind-pred.html}{\mathrm{Ind}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/on-const.html}{\mathbf{On}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST TpInd
Scheme of Types 0Ind(On)
Verification Verified (Kernel) · Standalone Entry (ThmOrdinalsInductive) → · (3.60) · #ThmOrdinalsInductive