263: For 2 Sets, Collection of Functions Between Sets Is Set

<The previous article in this series | The table of contents of this series | The next article in this series>

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
• Target Context
• Orientation
• Main Body
• 1: Description
• 2: Proof

---

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)|f:S_1\to S_2\}$, is a set.

---

2: Proof

${}^{S_1}{S}_2=\{f\in Pow(S_1\times S_2)|(\mathrm{\forall }{s}_1\in S_1,\mathrm{\exists }{s}_2\in S_2,⟨s_1,s_2⟩\in f)\wedge ((\mathrm{\exists }{s}_1\in S_1,\mathrm{\exists }{s}_2\in S_2,\mathrm{\exists }{s_2}^{\prime }\in S_2,⟨s_1,s_2⟩\in f\wedge ⟨s_1,{s_2}^{\prime }⟩\in f)⟹(s_2={s_2}^{\prime }))\}$. 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.

---

References

<The previous article in this series | The table of contents of this series | The next article in this series>