DefGrothendieckUniverse (3.68, Definition): “Is a universe” predicate

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

Formula Display:

Proof Trees:

DefGrothendieckUniverse (3.68) — “Is a universe” 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 a universe” predicate `#DefGrothendieckUniverse` `#label-is-a-universe-predicate`
Classification	Definition
Formula	0(∀(U:Class)((U universe )⟷(((ω∈U)∧((Tr(U)∧Hereditary(U))∧(Powerful(U)∧Tight(U))))∧Pairful(U)))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{U} \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}{U} \href{../symbols/universe-pred.html}{\mathsf{universe}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/omega-const.html}{\omega} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{U} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/trans-pred.html}{\mathrm{Tr}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{U} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/hereditary-pred.html}{\mathsf{Hereditary}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{U} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/powerful-pred.html}{\mathsf{Powerful}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{U} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/tight-pred.html}{\mathsf{Tight}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{U} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/pairful-pred.html}{\mathsf{Pairful}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{U} \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`(∀([U@Variable]:[Class@Type])(([U@Class.Expression] universe)⟷(((ω∈[U@Class.Expression])∧((Tr([U@Class.Expression])∧Hereditary([U@Class.Expression]))∧(Powerful([U@Class.Expression])∧Tight([U@Class.Expression]))))∧Pairful([U@Class.Expression]))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefGrothendieckUniverse`) → · (3.68) · `#DefGrothendieckUniverse`