A description/proof of that for 2 sets, collection of functions between sets is set
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of set.
- The reader knows a definition of function.
- The reader admits the proposition that the product of any finite number of sets is a set.
- The reader admits the proposition that some expressions can be parts of legitimate formulas for the ZFC set theory.
Target Context
- The reader will have a description and a proof of the proposition that for any 2 sets, the collection of all the functions between the sets is a set.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Description
For any sets, \(S_1, S_2\), the collection of all the functions from \(S_1\) to \(S_2\), \({}^{S_1} S_2 = \{f \in Pow (S_1 \times S_2)\vert f: S_1 \rightarrow S_2\}\), is a set.
2: Proof
\({}^{S_1} S_2 = \{f \in Pow (S_1 \times S_2)\vert (\forall s_1 \in S_1, \exists s_2 \in S_2, \langle s_1, s_2 \rangle \in f) \land ((\exists s_1 \in S_1, \exists s_2 \in S_2, \exists {s_2}' \in S_2, \langle s_1, s_2 \rangle \in f \land \langle s_1, {s_2}' \rangle \in f) \implies (s_2 = {s_2}'))\}\). By the proposition that the product of any finite number of sets is a set, \(S_1 \times S_2\) is a set. By the power set axiom, \(Pow (S_1 \times S_2)\) is a set. By the proposition that some expressions can be parts of legitimate formulas for the ZFC set theory, the subset axiom can be applied. So, \({}^{S_1} S_2\) is a set.
