How to rigorously prove from set theory that functions can be composed?

This is a follow up to my previous question about existence and uniqueness of piecewise functions. Suppose we are given two functions $$f:S \rightarrow T$$ and $$g:T \rightarrow U$$. How does one prove from ZFC set theory that there is a unique function $$h:S \rightarrow U$$ which is the composition of those two functions?

I'm using the definition $$A \to B = \{f \in P(A \times B) | \forall x \in A \exists ! y \in B (x, y) \in f\}$$. That is, a function is a set of input-output pairs such that every input corresponds to a unique output.

Define $$h = \{(x, y) \in S \times U | \exists z \in T ((x, z) \in f \land (z, y) \in g)\}$$. I claim that $$h$$ forms a function $$h : S \to U$$.

First, we must prove that $$h$$ is a set at all. But we know that $$h$$ is a set because $$S \times U$$ is a set (by other axioms) and we can pick $$h$$ out as a subset of $$U$$ using the axiom schema of separation.

Now, we must prove that $$h$$ is a function (proving uniqueness). Suppose we have $$(x, y) \in h$$ and $$(x, y') \in h$$. Then take $$z \in T$$ such that $$(x, z) \in f$$ and $$(z, y) \in g$$. And take $$z' \in T$$ such that $$(x, z') \in f$$ and $$(z', y') \in g$$. Then since $$f$$ is a function, $$z = z'$$. So we see that $$(z, y) \in g$$ and $$(z, y') \in g$$. Then since $$g$$ is a function, we have $$y = y'$$.

Now, we prove that $$h \subseteq S \times U$$. Suppose we have $$(x, y) \in h$$. Then take $$z \in T$$ such that $$(x, z) \in f$$ and $$(z, y) \in g$$. Since $$f \subseteq S \times T$$, we see that $$x \in S$$. And since $$g \subseteq T \times U$$, we see that $$y \in U$$. Then $$(x, y) \in S \times U$$.

Finally, we prove existence. Suppose we have $$x \in S$$. Then take some $$z \in T$$ such that $$(x, z) \in f$$. Then take some $$y \in U$$ such that $$(z, y) \in g$$. Then $$(x, y) \in h$$.

Thus, we see that $$h : S \to U$$.

Note that we do not ever need the axiom schema of replacement, the axiom of foundation, or the axiom of choice in proving this theorem.

• I don't think you need to prove $h \subseteq S \times U$, or can justify it just by noting its definition is $h = \{(x,y) \in S \times U|...\}$ May 8 '21 at 19:48
• @aschepler Good point. May 8 '21 at 23:37