DefIsCardinal (3.64, Theorem): “Is cardinal” predicate

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

Formula Display:
Proof Trees:

DefIsCardinal (3.64) — “Is cardinal” predicate

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.64
Title “Is cardinal” predicate #DefIsCardinal #label-is-cardinal-predicate
Classification Theorem
Formula
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{C} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/card-pred.html}{\mathrm{Card}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{C} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/exists-binder.html}{\exists} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{K} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/card-op.html}{ \mid } \href{../symbols/variables.html}{K} \href{../symbols/card-op.html}{ \mid } \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{C} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST TpCard
Scheme of Types 0(∀([C@Variable]:[Class@Type])(Card([C@Class.Expression])⟷(∃([K@Variable]:[Class@Type])(|[K@Class.Expression]|=[C@Class.Expression]))))
Verification Verified (Kernel) · Standalone Entry (DefIsCardinal) → · (3.64) · #DefIsCardinal