写像の形式的定義

関数とか写像というのは，中学・高校時代から習っていています．
$f(x)=x^2$とか$f(x)=\sin (x)$です． $x$に$x^2$を対応させる関数を$f(x)$とする．
というように使うのですが，写像や関数は対象と対象を対応させる 機能や規則を表していて，$x$とか$x^2$と違い具体的な対象ではないようにみえます．
しかし，これも，数と同じように対象の一つとして扱います．
$x$から$y$への写像とか関数と呼ばれるものを数と同じように扱うことができるような定義を与えておきます． (これが唯一の方法ということではありません．)

材料は写像の定義域の集合$X$，値域の集合$Y$，それに$X$の要素$x$に$Y$の要素$y$を対応させる規則です．
$X$から$Y$への写像(あるいは関数)$f$は形式的に

$$f=(G_f,X,Y)$$

という3重の対として定義されます．
$G_f$は写像$f$のグラフと呼ばれます．これは，

$$X\times Y=\{ (x,y)\vert x\in X ~and~y\in Y\}$$

の部分集合，つまり $G_f \subseteq X\times Y$で，任意の $x\in X,y\in Y,z\in Y$について $~(x,y)\in G_f ,(x,z)\in G_f ~$なら$~y=z$になるものです．
また$X,Y$と$G_f$には

$$\{ x\vert(\exists y)((x,y)\in G_f )\} =X$$

$$\{ y\vert(\exists x)((x,y)\in G_f )\} \subseteq Y$$

が成り立つという条件を課します．$f$のグラフ$G_f$は， 例えば$f(x)=x^2$についてその曲線を座標に書くと判りますように 曲線上の点$(x,x^2)$全ての集合で文字通りグラフ$r$です．
以上の定義を記号論理で書けば