= Solution
Use the <Kuratowski ordered pair>
$$
\boxed{\langle x,y\rangle=\{\{x\},\{x,y\}\}.}
$$
The <axiom of pairing> first constructs $\{x\}$ and $\{x,y\}$, then constructs the displayed <pair> of those <sets>, proving that it is a <set>.
For any $a,b$, the <intersection> of the members of this <pair> is $\{a\}$, and their <union> is $\{a,b\}$. Thus equality of two <ordered pairs> first gives $\{a\}=\{c\}$, hence $a=c$, and then $\{a,b\}=\{a,d\}$. If $b=a$, this latter <set> is a <singleton> and forces $d=a$. If $b\ne a$, its unique member distinct from $a$ is $b$, forcing $d=b$. Hence equality of <ordered pairs> gives equality of both coordinates.
For a <set> $R$ of <ordered pairs>, both coordinates of every <pair> belong to
$$
U=\bigcup\bigcup R,
$$
which is a <set> by two applications of the <Axiom of union>. <Axiom of separation> inside $U$ gives
$$
\operatorname{dom}R=\{x\in U:\exists y\,\langle x,y\rangle\in R\},\qquad
\operatorname{ran}R=\{y\in U:\exists x\,\langle x,y\rangle\in R\}.
$$
These are <sets>, including when $R$ is empty.
The <Axiom of foundation> asserts that every nonempty <set> $A$ has an element $a$ with $a\cap A=\varnothing$. If a <descending membership sequence> $f:\omega\to V$ existed, <replacement> would give the nonempty range <set> $S=\{f(n):n\in\omega\}$. <Foundation> would give some $f(n)$ disjoint from $S$. But $f(n^+)\in f(n)$ and $f(n^+)\in S$, contradicting that disjointness. Thus <foundation> rules out every such <sequence>.
Conversely suppose there is no <descending membership sequence>, but <foundation> fails. There is then a nonempty <set> $A$ such that $a\cap A\ne\varnothing$ for every $a\in A$. The <axiom of choice> selects a <function> $h$ on $A$ with $h(a)\in a\cap A$. Choose $a_0\in A$ and use <recursion> to define
$$
f(0)=a_0,\qquad f(n^+)=h(f(n)).
$$
Every value remains in $A$, and $f(n^+)\in f(n)$ for every $n$. This is the forbidden <sequence>. Therefore, with the stated <choice> assumption, \b[<foundation> is equivalent to the absence of <descending membership sequences>]. The selection step explains exactly where <choice> is used; <dependent choice> would suffice.
Back to article page
