DefInjectiveFunction (3.33, Definition): “Is injective” predicate

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

Formula Display:
Proof Trees:

DefInjectiveFunction (3.33) — “Is injective” 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.33
Title “Is injective” predicate #DefInjectiveFunction #label-is-injective-predicate
Classification Definition
Formula
0(∀(F:Class)((F injective)⟷(((F family)∧(F set-valued))∧∀(x:Class)∀(y:Class)((((x∈Dom(F))∧(y∈Dom(F)))∧(F(x)=F(y)))→(x=y)))))
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/injective-pred.html}{\mathsf{injective}} \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/variables.html}{F} \href{../symbols/family-pred.html}{\mathsf{family}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{F} \href{../symbols/set-valued-pred.html}{\mathsf{set\text{-}valued}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \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/forall-binder.html}{\forall} \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/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/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{y} \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/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \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/eq-pred.html}{=} \href{../symbols/variables.html}{F} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{y} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{y} \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 TpInjective
Scheme of Types 0(∀([F@Variable]:[Class@Type])(([F@Class.Expression] injective)⟷((([F@Class.Expression] family)∧([F@Class.Expression] set-valued))∧∀([x@Variable]:[Class@Type])∀([y@Variable]:[Class@Type])(((([x@Class.Expression]∈Dom([F@Class.Expression]))∧([y@Class.Expression]∈Dom([F@Class.Expression])))∧([F@Class.Expression]([x@Class.Expression])=[F@Class.Expression]([y@Class.Expression])))→([x@Class.Expression]=[y@Class.Expression])))))
Verification Definitional (Kernel AST) · Standalone Entry (DefInjectiveFunction) → · (3.33) · #DefInjectiveFunction