DefHereditaryClass (3.44, Definition): “Is hereditary” predicate

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

Formula Display:

Proof Trees:

DefHereditaryClass (3.44) — “Is hereditary” 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)

Title	“Is hereditary” predicate `#DefHereditaryClass` `#label-is-hereditary-predicate`
Classification	Definition
Formula	0(∀(A:Class)(Hereditary(A)⟷(∀(B:Class)((B∈A)→∀(X:Class)((X⊆B)→(X∈A)))))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{A} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/hereditary-pred.html}{\mathsf{Hereditary}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{A} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{B} \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}{B} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{A} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \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/sub-pred.html}{\subseteq} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{A} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PKernelDef_prf`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])(Hereditary([A@Class.Expression])⟷(∀([B@Variable]:[Class@Type])(([B@Class.Expression]∈[A@Class.Expression])→∀([X@Variable]:[Class@Type])(([X@Class.Expression]⊆[B@Class.Expression])→([X@Class.Expression]∈[A@Class.Expression]))))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefHereditaryClass`) → · (3.44) · `#DefHereditaryClass`