Uniqueness Condition for Relation Value

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\RR$ be a relation.

Let $\tuple {x, y} \in \RR$.

Let:

$\exists ! y: \tuple {x, y} \in \RR$


Then:

$\map \RR x = y$

where $\map \RR x$ denotes the image of $\RR$ at $x$.


If $y$ is not unique, then:

$\map \RR x = \O$


Proof

\(\text {(1)}: \quad\) \(\ds z \in \map \RR x\) \(\implies\) \(\ds \exists y: \paren {z \in y \land \tuple {x, y} \in \RR} \land \exists ! y: \tuple {x, y} \in \RR\) Definition of Image of Element under Relation
\(\ds \) \(\implies\) \(\ds \forall w: \paren {\tuple {x, w} \in \RR \iff w = y}\) Definition of Unique and by hypothesis that $\tuple {x, y} \in \RR$
\(\ds \) \(\implies\) \(\ds z \in w \land \tuple {x, w} \in \RR\) Existential Instantiation from $(1)$
\(\ds \) \(\implies\) \(\ds z \in y\) Substitutivity of Equality from $z \in w \land w = y$


Conversely:

\(\ds z \in y\) \(\implies\) \(\ds \paren {z \in y \land \tuple {x, y} \in \RR}\) by hypothesis that $\tuple {x, y} \in \RR$
\(\ds \) \(\) \(\ds \exists ! y: \tuple {x, y} \in \RR\) by hypothesis
\(\ds \) \(\implies\) \(\ds z \in \map \RR x\) Definition of Image of Element under relation

Generalizing:

$\forall z: \paren {z \in y \iff z \in \map \RR x}$

Therefore:

$y = \map \RR x$

by the definition of class equality.

$\Box$


Suppose that $\neg \exists ! y: \tuple {x, y} \in \RR$.

Then:

\(\ds \neg \exists ! y: \tuple {x, y} \in \RR\) \(\implies\) \(\ds z \notin \map \RR x\) Definition of Image of Element under relation

Thus:

$\forall z: z \notin \map \RR x$

Therefore:

$\map \RR x = \O$

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Uniqueness_Condition_for_Relation_Value&oldid=574168"