How can I write one-to-one and onto in predicate logic? How can I write one-to-one and onto in predicate logic?
$\forall a \forall b(a\in X  \land b\in Y, a \implies b)$
This seems very wrong, but I don't know any other way to do it.
 A: First of all you need a name for the function that you want to describe as a bijection from $X$ to $Y$; I’ll call it $f$.

*

*$f$ is a relation from $X$ to $Y$: $$\forall z\Big(z\in f\to\exists x\exists y\big(x\in X\land y\in Y\land z=\langle x,y\rangle\big)\Big)$$


*$f$ is a function with domain $X$: $$\forall x\left(x\in X\to\exists y\big(y\in Y\land \langle x,y\rangle\in f\land\forall z\big((z\in Y\land\langle x,z\rangle\in f)\to z=y\big)\Big)\right)$$


*$f$ is a surjection: $$\forall y\Big(y\in Y\to\exists x\big(x\in X\land\langle x,y\rangle\in f\big)\Big)$$


*$f$ is an injection: $$\forall x\forall y\forall z\Big(\big(x\in X\land z\in X\land\langle x,z\rangle\in f\land\langle y,z\rangle\in f\big)\to x=z\Big)$$
The conjunction of these three expressions says that $f$ is a bijection from $X$ onto $Y$.
I find them easier to read in the following form:
$$\begin{align*}
&\forall z\in f\,\exists x\in X\,\exists y\in Y\big(z=\langle x,y\rangle\big)\\\\
&\forall x\in X\,\exists y\in Y\Big(\langle x,y\rangle\in f\land\forall z\in Y(\langle x,z\rangle\in f\to z=y\Big)\\\\
&\forall y\in Y\,\exists x\in X\big(\langle x,y\rangle\in f\big)\\\\
&\forall x,y\in X\,\forall z\in Y\Big(\big(\langle x,y\rangle\in f\land\langle y,z\rangle\in f\big)\to x=z\Big)
\end{align*}$$
