Set Theoretic Explanation of Existence of Convergent Sequence

Question

Suppose that we have some set $A \subseteq \mathbb R$ whose infimum is $m$. Now, generally, we simply say that in such a situation, there is a sequence $\{a_n\}_{n \in \mathbb N} \subseteq A$ which converges to $m$. However, is there a way to prove this statement with ZF axioms? I want to say that with ZFC, we should use Axiom of Choice to give a function $f: \mathbb N \mapsto a_n$ with $a_n \in A \cap B_{1/n}(m)$ where $B_\epsilon(a)$ is the $\epsilon$-ball around $a$. This certainly suffices, but presentation of mathematics generally distinguishes proofs which require the Axiom of Choice versus those which don't, so I'm thinking I might be overlooking a proof which uses only ZF.

Answer 1

Some choice is needed for this claim.

Suppose that $D'$ is a Dedekind finite infinite set of reals, meaning that it has no countable subsets (there are models of $\mathsf{ZF}$ where such things exist). Such a set must have an accumulation point, call it $p$, and we can assume wlog that $p$ is an accumulation point of $D=D'\cap(p,\infty)$ (by replacing $D'$ with $-D'$ and $p$ with $-p$ if needed). Now $p=\inf D$, but no sequence in $D$ can converge to $p$, since all sequences in $D$ are eventually constant (otherwise the image of a sequence which is not eventually constant would be a countable subset of $D$, hence of $D'$, which was Dedekind finite).

On the other this claim is provable from $\mathsf{ZF}+\mathsf{AC}_\omega$, the axiom of countable choice, and the more general claim that if $X$ is a metric space and $p\in X$ is an accumulation point of $D\subseteq X$, then there is a sequence in $D$ converging to $p$ is actually equivalent to the axiom of countable choice over $\mathsf{ZF}$.