How to write a set that is a function using set notation

Question

I want to define (defining it as set) that $F$ is an arbitrary function from $X$ to $Y$ so I could use expressions like $(x,y)\in F$.

This is what I have managed to write:

$$F = \left\{ (x,y) \mid x\in X, y\in Y \right\}$$

What I struggle is to write single-valueness - the fact that any $x$ appears in at most one pair.

Edit

I am looking exactly for a way to write in the way that would read (in order) something like this: "$F$ is a set consisting of ordered pairs where the first element belongs to $X$, the second belongs to $Y$ and the first element must be different in each pair."

My current idea is to do this: $$F = \left\{ (x,y) \mid x\in X \land y\in Y \land \forall (x, y')\in F\Rightarrow y'=y) \right\}$$

I am just not that sure that this is easily readablle and correct to impose restriction using self-reference.

Answer 1

You can think of a function from $X$ to $Y$ as a subset $F\subset X\times Y$ which satisfies $$\forall x\forall y\forall z\Big(((x,y)\in F\wedge (x,z)\in F)\Rightarrow y=z\Big)$$

Answer 2

It is customary to write $f: X \rightarrow Y$, but that is probably not what you are after.

I would introduce the notation, where $f: X \rightarrow Y$, of

$$\textrm{graph}(F) = \{ (x,y) \in X \times Y \mid y = f(x) \}$$

and then state that whenever we write $(x,y) \in F$, this is a shorthand for $(x,y) \in \textrm{graph}(F)$.

Answer 3

If I understand correctly, you want to express that $F$ is a function from $X$ to $Y$ using an expression like $F = \{\,(x,y)\mid\cdots\,\}$ (and nothing else). I don’t think that is possible because “$F$ is a function” is not an equality.

Another way to look at it: Whatever you substitute for the dots in $\{\,(x,y)\mid\cdots\,\}$, you are describing a single specific set hence a specific function (if it is a function at all). But you just want to say that $F$ is a function, not that $F$ is a specific function.