AxmSizeLimitation (3.43, Axiom): Size limitation axiom related statement

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

Formula Display:
Proof Trees:

AxmSizeLimitation (3.43) — Size limitation axiom related statement

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.43
Title Size limitation axiom related statement #AxmSizeLimitation #label-size-limitation-axiom-related-statement
Classification Axiom
Formula
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/in-pred.html}{\in} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/card-op.html}{ \mid } \href{../symbols/variables.html}{X} \href{../symbols/card-op.html}{ \mid } \href{../symbols/card-lt-pred.html}{\prec} \href{../symbols/card-op.html}{ \mid } \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/card-op.html}{ \mid } \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST PSizeLimAx_prf
Scheme of Types 0(∀([X@Variable]:[Class@Type])(([X@Class.Expression]∈V)⟷(|[X@Class.Expression]|≺|V|)))
Verification Postulated (Kernel Axiom) · Standalone Entry (AxmSizeLimitation) → · (3.43) · #AxmSizeLimitation