ThmOmegaTransitive (3.61, Theorem): ω is transitive

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

Formula Display:
Proof Trees:

ThmOmegaTransitive (3.61) — ω is transitive

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.61
Title ω is transitive #ThmOmegaTransitive #label-is-transitive
Classification Theorem
Formula
0Tr(ω)
0\(\href{../symbols/trans-pred.html}{\mathrm{Tr}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST TpTrans
Scheme of Types 0Tr(ω)
Verification Verified (Kernel) · Standalone Entry (ThmOmegaTransitive) → · (3.61) · #ThmOmegaTransitive