DefFamily (3.31, Definition): “Is a family” predicate

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

Formula Display:
Proof Trees:

DefFamily (3.31) — “Is a family” 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.31
Title “Is a family” predicate #DefFamily #label-is-a-family-predicate
Classification Definition
Formula
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{F} \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}{F} \href{../symbols/family-pred.html}{\mathsf{family}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{F} \href{../symbols/concentrated-pred.html}{\mathsf{concentrated}} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/values-pred.html}{\mathsf{values}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{F} \href{../symbols/flat-pred.html}{\mathsf{flat}} \href{../symbols/proper-pred.html}{\mathsf{proper}} \href{../symbols/values-pred.html}{\mathsf{values}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST TpFamily
Scheme of Types 0(∀([F@Variable]:[Class@Type])(([F@Class.Expression] family)⟷(([F@Class.Expression] concentrated set values)∧([F@Class.Expression] flat proper values))))
Verification Definitional (Kernel AST) · Standalone Entry (DefFamily) → · (3.31) · #DefFamily