Ensemble des fonctions partielles

Bonjour,

Voici la suite de mes aventures dans un chapitre de théorie des ensembles du livre de Terence Tao, aventures entamées ici. (Merci aux précédents contributeurs !)

Il s'agirait cette fois de résoudre un autre exercice du livre. En voici l'énoncé (en VO) :

Let $X, Y$ be sets. Define a partial function from $X$ to $Y$ to be any function $f: X' \rightarrow Y'$ with $X' \subseteq X$ and $Y'\subseteq Y$. Show that the collection of all partial functions from $X$ to $Y$ is itself a set.

Terence Tao fournit un indice : il faudra utiliser les 4 résultats suivants, qui figurent dans son chapitre (je les abrège un peu) :

1. Lemme 3.4.9. Soit $X$ un ensemble. Alors il existe un ensemble $\{Y \, : \, Y \text{ est une partie de } X\}$. On le note $2^X$.
2. Axiome 3.10. Soient deux ensembles $X$ et $Y$. Alors il existe un ensemble, noté $Y^X$, qui consiste en l'ensemble des fonctions de $X$ vers $Y$.
3. Axiome 3.6. L'axiome du remplacement (rappelé ici).
4. Axiome 3.11. L'axiome de l'union : soit $A$ un ensemble, dont tous les éléments sont eux-mêmes des ensembles. Alors il existe un ensemble $\bigcup A$ dont les éléments sont les objets appartenant aux éléments de $A$, i.e., $x \in \bigcup A$ ssi $x \in S$ pour un certain $S \in A$. Une conséquence: si on a un ensemble $I$, et qu'à tout élément $\alpha \in I$ correspond un ensemble $A_\alpha$, alors on peut former l'union $\bigcup_{\alpha \in I} A_\alpha$ ainsi définie : $\bigcup_{\alpha \in I} A_\alpha := \bigcup \{ A_\alpha \, | \, \alpha \in I\}$.

Il y a sur internet certaines solutions très longues et laborieuses, par exemple ici. La solution que j'avais écrite est beaucoup plus courte, et je suppose donc qu'elle est erronée et/ou incomplète. La voici :

1. Soient $X' \subseteq X$ et $Y' \subseteq Y$ deux sous-ensembles fixés de $X$ et $Y$. Alors, par l'axiome (3.10), il existe un ensemble $Y'^{X'}$ qui est composé de toutes les fonctions de $X'$ vers $Y'$.

2. Par le lemme 3.4.9, il existe un ensemble $2^X$ qui consiste en l'ensemble des parties de $X$, et un ensemble $2^Y$ qui consiste en l'ensemble des parties de $Y$.

3. À présent, on fixe un élément $X'$ de $2^X$. Soient $Y'$ un élément de $2^Y$, $f$ une fonction, et $P$ la propriété « $P(Y', f)$: $f$ est une fonction de $X'$ vers $Y'$ ». Par l'axiome du remplacement, il existe un ensemble $\{f \, | \, P(Y', f) \text{ est vraie pour un certain } Y' \in 2^Y\} = \{f \, | \, f: X' \rightarrow Y' \text{ pour un certain } Y' \in 2^Y\}$. Cet ensemble est obtenu pour un élément fixé $X' \subseteq X$, donc on peut le noter $S_{X'} = \{f \, | \, f: X' \rightarrow Y' \text{ pour un certain } Y' \in 2^Y\}$.

4. Enfin, on applique l'axiome de l'union (3.11), en particulier via sa seconde formulation. Ici, l'ensemble d'indexation est $I = 2^X$ ; ainsi, à chaque élément $X' \in I$ correspond en effet un ensemble $S_{X'}$, défini au point 3. Donc, il existe un ensemble $\bigcup_{X' \in 2^X} S_{X'} := \bigcup \{S_{X'} \, | \, X' \in 2^X\}$. Et, pour toute fonction $f$, on a $f \in \bigcup \{S_{X'} \, | \, X' \in 2^X\}$ si et seulement si il existe $X' \in 2^X$ tel que $f \in S_{X'}$, i.e. s'il existe $X' \subset X$ et $Y' \subset Y$ tels que $f: X' \rightarrow Y'$. (C'est-à-dire, $f$ est une fonction partielle de $X$ vers $Y$.)

5. Ainsi, il existe bien un ensemble défini comme la collection de toutes les fonctions partielles de $X$ vers $Y$.

Cette preuve n'est probablement pas correcte ou suffisante : où sont les erreurs ?
Merci !

(P.-S. : pour cet exercice, on est supposé ne pas utiliser la notion de produit cartésien, qui n'est introduite que plus tard dans le livre.)