DefHasConcentratedValues (3.29, Definition): “Has concentrated set values” predicate

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

Formula Display:
Proof Trees:

DefHasConcentratedValues (3.29) — “Has concentrated set values” 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.29
Title “Has concentrated set values” predicate #DefHasConcentratedValues #label-has-concentrated-set-values-predicate
Classification Definition
Formula
0(∀(F:Class)((F concentrated set values)⟷(∀(x:Class)((x∈Dom(F))→((F(x) set)→∃!(y:Class)((x,y)∈F))))))
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/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/iff-conn.html}{\longleftrightarrow} \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/dom-op.html}{\mathrm{Dom}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{F} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{F} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/exists-uniq-binder.html}{\exists!} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{y} \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/comma-delim.html}{,} \href{../symbols/variables.html}{y} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{F} \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 TpConcentrated
Scheme of Types 0(∀([F@Variable]:[Class@Type])(([F@Class.Expression] concentrated set values)⟷(∀([x@Variable]:[Class@Type])(([x@Class.Expression]∈Dom([F@Class.Expression]))→(([F@Class.Expression]([x@Class.Expression]) set)→∃!([y@Variable]:[Class@Type])(([x@Class.Expression],[y@Class.Expression])∈[F@Class.Expression]))))))
Verification Definitional (Kernel AST) · Standalone Entry (DefHasConcentratedValues) → · (3.29) · #DefHasConcentratedValues