"Power set axiom"

Bonjour,

J'étudie actuellement le chapitre "Set theory" des cours d'analyse de Terence Tao.
Parmi les exercices, figure notamment celui-ci :

Terence Tao a écrit:

Prove lemma 3.4.9. (Hint: start with the set $\{0,1\}^X$ and apply the replacement axiom, replacing each function $f$ with the object $f^{-1}(\{1\})$.)

Clarifions les choses. :-D Dans son chapitre, Tao propose une version (visiblement présentée de façon pas totalement classique) de l'axiomatique de ZFC. Il énonce notamment :

Terence Tao a écrit:

Replacement axiom. Let $A$ be a set. For any object $x \in A$, and any object $y$, suppose we have a statement $P(x,y)$ pertaining to $x$ and $y$, such that for each $x \in A$ there is at most one $y$ for which $P(x,y)$ is true. Then there exists a set $\{y \; | \; P(x,y) \text{ is true for some } x \in A\}$, such that for any object $z$,
\[ z \in \{y \; | \; P(x,y) \text{ is true for some } x \in A\} \Longleftrightarrow P(x,z) \text{ is true for some } x \in A\]

Power set axiom. Let $X$ and $Y$ be sets. There there exists a set, denoted $Y^X$, which consists of all the function from $X$ to $Y$:
\[f \in Y^X \Longleftrightarrow (f \text{ is a function from $X$ to $Y$}\}\]

Lemma 3.4.9. Let $X$ be a set. Then the set $\{Y \; | \; Y \text{ is a subset of X}\}$ is a set.

Le but est donc de prouver ce dernier lemme à partir des deux axiomes précédents. (Comme tous les exercices du chapitre de Tao,) c'est intuitivement évident, mais pas si simple à écrire. Est-ce que la démarche suivante vous semble correcte, et est-ce qu'elle peut être améliorée ?

1. On considère un ensemble $X$, et $Y = \{0,1\}$. Par le "power set axiom", $\{0,1\}^X$ est bien un ensemble, et contient l'ensemble des fonctions $f : X \rightarrow \{0,1\}$.

2. Soit $A$ une partie quelconque de $X$ : on peut définir la fonction $f_A : X \rightarrow \{0,1\}$ telle que pour tout $x \in X$, $f(x) = 1$ si $x \in A$, et $f(x)=0$ sinon. Mieux :

• Si $A$ est une partie de $X$, il existe un élément $f \in \{0,1\}^X$ tel que $A = f^{-1}(\{1\})$ : c'est précisément $f_A$.
• Réciproquement, si $f \in \{0,1\}^X$, alors $f^{-1}(\{1\})$ est par définition une partie de $X$.

Ainsi, les deux assertions « $A$ est une partie de $X$ », et « il existe $f \in \{0,1\}^X$ telle que $A = f^{-1}(\{1\})$ » sont équivalentes.

3. Soit $A \subset X$ et $f \in \{0,1\}^X$. On appelle $P(f,A)$ l'assertion "$A = f^{-1}(\{1\})$". Pour chaque $f$, il y a bien au plus un $A$ (en fait, exactement un $A$) tel que $P(f,A)$ soit vraie. Alors, par l'axiome du remplacement, il existe un ensemble :
\[\mathcal{P} = \{A \; | \; A = f^{-1}(\{1\}) \text{ pour une certaine } f \in \{0,1\}^X\}\]
Et, d'après l'équivalence démontrée en 2. :
\[ \mathcal{P} = \{A \; | \; A \text{ est une partie de } X\} \]
est un ensemble bien définie, ce que l'on voulait démontrer.

Is this correct?

Merci !