No infinite membership sequence implies Axiom of foundation/regularity

Question

I want to show that the assumption that there are no infinite descending membership sequences implies the axiom of foundation/regularity.

I have read that this requires the axiom of choice, but I am not sure where/why.

I am trying to prove the contrapositive, so suppose $X$ is a non-empty set such that $\forall y[y \in X \implies y \cap X \neq \emptyset]$.

I know that usually, the infinite descending membership sequence is represented as a function $f : \omega \rightarrow X$ such that $f(n+1) \in f(n)$ for all $n$ and the axiom of choice is used here somehow. Could someone please explain how I may define such a function?

My original proof attempt involved assuming that there are no infinite descending membership sequences which I stated as $\exists m [m \in X \land \forall n(n \in m \implies n \notin X)]$. This formal statement does not imply the non-existence of infinite descending membership sequences as pointed out by @spaceisdarkgreen in the comments.

Thanks!

Answer 1

As I mentioned in the comments, your proof is not correct since it doesn't interpret the statement "here is no infinite descending membership sequences" correctly.

Suppose, as you did, that foundation fails and $X$ is a non-empty set such that $\forall y[y \in X \implies y \cap X \neq \emptyset]$. The idea is to recursively construct an infinite descending membership sequence using dependent choice:

Let $x_0\in X$ and, given $x_n\in X$, choose an $x_{n+1}\in x_n\cap X.$