AxmOmegaIsSet (3.57, Axiom): “Infinity”(ω is a set)

AxmOmegaIsSet (3.57) — “Infinity”(ω is a set)

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	“Infinity”(ω is a set) `#AxmOmegaIsSet` `#label-infinity-is-a-set`
Classification	Axiom
Formula	0(ω set ) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`POmegaSetAx_prf`
Scheme of Types	0`(ω set)`
Kernel Note	Asserts that the ⊆-minimal successor-inductive (Peano-inductive) class ω is a set.
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmOmegaIsSet`) → · (3.57) · `#AxmOmegaIsSet`