Theorem. The collection of all partial functions from $X$ to $Y$ is a set.

Proof.

$\textit{Note:}$ Where one could think that the notions $\textit{collection}$ and $\textit{set}$ can be used interchangeably, this exercise seems to aim at mathematical rigour when deriving the implication that a given object is indeed a set, based only on some axioms of set theory.

Given a set $Y$ and an element $X'$ of the power set $\mathcal{X} = \{ X' : X' \subseteq X \}$ such that there is a unique power set $Y^{X'}$ for every $X' \in \mathcal{X}$. Then there is a set $\{ Y^{X'} : X' \subseteq X \}$ such that for every $z$: $$z \in \{ Y^{X'} : X' \subseteq X \} \leftrightarrow z \:\: \text{is the unique power set for some} \: X'.$$ Now that $\{ Y^{X'} : X' \subseteq X \}$ is a set (of sets of partial functions from $X$ to $Y$) the union axiom may be applied to define the $set$ of all partial functions from $X$ to $Y$ to be $$\bigcup \{ Y^{X'} : X' \subseteq X \}.$$ $\Box$

2015 JAN 14 (v1.0)
Contact me: m.herrmann followed by an -at- followed by blaetterundsterne.org.

This document created with the help of MathJax (Thank you guys!)