Cauchy complete subspace of a metric space is closed. Is some version of the Axiom of Choice required to show that a complete subspace $A$ of a metric space $X$ is closed? By closed I mean that the set's complement is open, or equivalently that it contains all of its accumulation points.
I've been messing around it like this:
Let $l$ be a limit point of $A$. For each $\delta_n$ with $\delta_n \to 0$ as $n \to \infty$ there exists some $a_n \in A$ with $0 \lt d(a_n, l) \lt \delta_n$. This sequence $\{a_n\}$ a Cauchy sequence in $A$, and so converges to something in $A$. The limit has to be $l$.
If creating $\{a_n\}$ is using some variety of choice, then is there a way around it?
Thank you.
 A: This is a slight expansion of part of Disaster $4.53$ in Herrlich’s Axiom of Choice, Lecture Notes in Mathematics $1876$.
Take a model of $\mathsf{ZF}$ in which there is a bounded, infinite, Dedekind finite set $X\subseteq\Bbb R$. One can still prove that $X$ has a limit point $p\in\Bbb R$, and by replacing $X$ by $X\setminus\{p\}$ if necessary we may assume that $p\notin X$. Then $X$ is not closed in $\Bbb R$. However, $X$ is sequentially closed and therefore complete: since $X$ is Dedekind finite, every sequence in $X$ is eventually constant. Thus, some choice is needed even in $\Bbb R$.
A: Caveat: This is an attempt (pretty much just for my own benefit) to flesh out some of the details in @Brian M. Scott's answer.
I feel pretty solid about what comes next, but please feel free to point out errors (especially in Step 2)...
Goal: Show that if you have a model of ZF without Choice, then Cauchy complete does not imply closed.
Step 1)
Obtain a bounded, infinte, Dedekind-finite set $X \subseteq  \mathbb{R}$.
See https://mathoverflow.net/questions/68037/dedekinds-theorem.
Step 2)
X contains a limit point $p$ in $\mathbb{R}$.
You can do this without Choice. The set $X$ is assumed to be bounded, so is contained in some closed interval. $X$ is infinite, so you use repeated bisection to create a sequence of nested intervals, each of which contains an infinite # of points of $X$, whose endpoints converge to a single point. The limit of the endpoints is a limit point of $X$.
Another way is to first show that the closed interval $[0, 1]$ in $\mathbb{R}$ is compact, by considering (for some open cover of the interval) $\sup \{x: 0 \le x < 1 \text{ and } [0, x] \text{ is contained in a finite subcover} \}$. Then you show using compactness that if $X$ doesn't have a limit point in the interval then it must be finite. For each point in the interval, find the open interval around that point of radius $1/n$, with integer $n$ minimal, such that the interval intersects $X$ in at most one point, etc...
Step 3)
By replacing $X$ with $X \setminus \{p\}$, we can assume that $p \notin X$.
Why? If $X$ is Dedekind-finite, then so is $X\setminus \{p\}$. This is because an injection $f: X \setminus \{p\} \to A \subset X \setminus \{p\} $ yields an injection $g: X \to A \cup \{p\}$, with $g(x) = f(x)$ when $x \in X\setminus \{p\}$, and $g(p) = p$.
Step 4)
So $X$ has a limit point which is not contained in $X$, and so is not closed.
Step 5)
If $\{x_n\}$ is a sequence in $X$, then the set $\{x_n : n \in \mathbb{N}\}$ is finite.
If that were not true, then we can construct a subsequence  $\{y_n\}$ where all values are distinct. Do this inductively, and without Choice, by defining $y_1$ to be $x_1$, and $y_n$ to be the sequence element $x_k$ of smallest index $k$ is at least as big as any index used so far, and which is not contained in the set $\{y_j :  j < n\}$. This sequence $\{y_n\}$ provides an injection of $\mathbb{N}$ into $X$. That would mean that $X$ is not Dedekind-finite (shift the elements in the sequence to get the proper injection $X \to X$).
Step 6)
If $\{x_n\}$ is a Cauchy sequence in $X$, then it is eventually constant.
Why? The sequence only hits a finite number of values. The distances between these points is bounded away from zero.
Step 7)
So $X$ is a Cauchy complete space.
Steps 4) and 7) give what we wanted. 
