Functions Exist

Last updated Nov 1, 2022

Let $X$ be a Set and let $Y$ be a Nonempty Set. Then there exists a Function $f: X \to Y$.

Since $Y$ is Nonempty, there exists $y_{0} \in Y$. Take $f := {(x, y_{0}) \in X \times Y : x \in X}$. $f$ is a Function by construction because $x \in X$ is related to unique $y_{0}$. $\blacksquare$