ThmOmegaInductive (3.59, Theorem): Intersection of all successor-inductive (Peano-inductive) classes is a successor-inductive class itself (ω is the ⊆-least successor-inductive class)

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

Formula Display:
Proof Trees:

ThmOmegaInductive (3.59) — Intersection of all successor-inductive (Peano-inductive) classes is a successor-inductive class itself (ω is the ⊆-least successor-inductive 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.59
Title Intersection of all successor-inductive (Peano-inductive) classes is a successor-inductive class itself (ω is the ⊆-least successor-inductive class) #ThmOmegaInductive #label-intersection-of-all-successor-inductive-peano-inductive-classes-is-a-successor-inductive-class-itself-is-the-least-successor-inductive-class
Classification Theorem
Formula
0Ind(ω)
0\(\href{../symbols/ind-pred.html}{\mathrm{Ind}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST TpInd
Scheme of Types 0Ind(ω)
Kernel Note Establishes that ω itself satisfies Ind(ω), making ω the ⊆-least (minimal) element among all successor-inductive classes in the ⊆ order.
Verification Verified (Kernel) · Standalone Entry (ThmOmegaInductive) → · (3.59) · #ThmOmegaInductive