Démonstration avec axiome de fondation

Je ne suis pas sûr qu'il faille l'axiome de fondation. En fait j'ai une preuve sans me semble-t-il. Puisque Poirot a de toute façon donné la réponse qui suppose AF (enfin non, sa solution ne marche pas notamment à cause de $\{\{\emptyset\}, \emptyset\}$ - mais elle marche presque, à modification rapide près), je me permets de mettre (en blanc pour celles et ceux qui voudraient chercher) ladite solution.

Soit $x$ quelconque. On cherche $a$ tel que $x\times \{a\}$ soit disjoint de $x$. Il ne l'est pas si et seulement si il existe $y\in x$ tel que $(y,a)\in x$. Si je trouve alors $a$ tel que $x$ ne contienne aucun $(y,a)$, c'est bon. Si $(y,a)\in x$, c'est que (définition) $\{\{y\}, \{y,a\}\}\in x$, donc en particulier $\{y,a\} \in z\in x$ pour un $z$, donc $\{y,a\} \in \bigcup x$, donc $a\in t\in \bigcup x$ pour un $t$, donc $a\in \bigcup\bigcup x$. Donc il suffit de trouver $a$ tel que $a\notin \bigcup\bigcup x$ pour conclure que $x$ et $x\times \{a\}$ sont disjoints.
L'axiome de fondation fournit un $a$ très facile. Mais sans l'axiome de fondation on peut conclure aussi : on cherche à prouver, pour un $W$ spécifique ($W=\bigcup\bigcup x$) que "il existe $a\notin W$" : il s'agit là du paradoxe de Russell; pour tout $W$ il existe $a$ tel que $a\notin W$ (en fait on peut l'exhiber : $\{s\in W\mid s\notin s\}$). On applique ça à $W=\bigcup\bigcup x$ pour obtenir que $x\times \{ \{s\in \bigcup\bigcup x\mid s\notin s \}\}$ est disjoint de $x$.

Une solution possible (sans fondation, je ne vois pas trop ce qu'il fait dans l'exercice): soit $X$ un ensemble.

Le schéma de compréhension fournit l'existence d'un $Y:= \{p \in X \mid \exists q,r: (q,r)=p\}$ ($(x,y)$ désignant à l'accoutumée$\{\{x\}, \{x,y\} \}$).
Le schéma de remplacement entraînel'existence de $Z:=\{x \mid \exists t: (t,x) \in Y\}$ (en français: $Z$ est l'image par la deuxième projection de l'ensemble des couples contenus dans $X$).

Soit $T:= \bigcup Z$ la réunion des élements de $Z$. Alors $\mathcal P(T) \notin Z$ (sinon on aurait $\mathcal P(T) \subseteq T$). En particulier il n'existe aucun $q$ tel que $\left(q, \mathcal P(T)\right)\in X$. Donc $q \mapsto \left ( q, \mathcal P(T)\right )$ est une bijection entre $X$ et un ensemble disjoint de $X$ (son existence est à nouveau garantie par le schéma de remplacement).

Poirot : j'ai peut-être fait un oubli d'accolades, mais tu vois bien qu'il y a un problème. Si tu préfères, $x=\{\emptyset, (\emptyset,\emptyset)\}$

Christophe : oui c'est le détail de ça qui se trouve sans nos zones blanches. En ayant lu très rapidement j'ai l'impression que j'utilise moins de ZF que Foys

Je n'ai hélas pas le temps et passe en coup de vent, mais d'instinct et en tant que "supposé spécialiste" de ZF, je suis pourtant d'accord, au pied levé avec foys que je ne vois pas ce qu'apporte AF

christophe et Foys : AF apporte la facilité de dire simplement $x\times \{x\}$ sans avoir à réfléchir à qui est le $a$ dont nous parle Christophe

@CC, j'imagine que ta preuve de $\forall $ x (x, E) $\notin $ E (pas besoin de condition sur x) repose sur AF ? Du style si {{x, E}, {x}} $\in$ E, alors E $\in $ k $\in$ h $\in $ E et {E , k, h} contredit AF.

Sans AF et pour varier les plaisirs, soient A et B deux ensembles quelconques. On cherche un ensemble en bijection avec A et disjoint de B.

Soit F(x, y) la relation $\exists $ z $\in$ A x=(z, y) fonctionnelle en y. Alors d'après le schéma de remplacement, l'image de la relation x $\in $ B et F (x, y) est un ensemble. Soit k hors de cet ensemble.
A x {k} est en bijection avec A et est disjoint de B.

Question : peut-on se passer à la fois de AF et du schéma de remplacement ?
(j'imagine que l'existence et la construction de la clôture transitive nécessitent le schéma de remplacement, sinon, il suffirait de prendre k $\notin $ cl (B) )

En définitive, pour répondre concisément à la question de LeMordus (si ça l'intéresse encore), il suffit de prendre k hors de la clôture transitive de x, et de poser y = x X {k}

Aah , mais c'est tout bête, il suffit de prendre k hors de UU B (pour LeMordus, hors de UU x), pas besoin de AF, ni de schéma !
Desolé si quelqu'un l'a déjà mentionné, je n'ai pas lu toutes les interventions, en particulier celles écrites à l'encre sympathique ! :-)