[proofplan]
If $X$ is empty then $\operatorname{Fin}(X) = \{\varnothing\}$ is finite and so countable. Otherwise we compose two surjections: by the [Countability of $X^\star$](/theorems/1774) there is a surjection $\mathbb{N} \to X^\star$, and the forgetful map $X^\star \to \operatorname{Fin}(X)$ sending a string to its set of letters is surjective because every finite subset of $X$ can be listed as a string. The composition is a surjection $\mathbb{N} \to \operatorname{Fin}(X)$, which witnesses countability.
[/proofplan]
[step:Handle the empty case separately]
If $X = \varnothing$, then $\operatorname{Fin}(X) = \{F \subseteq \varnothing : F \text{ finite}\} = \{\varnothing\}$, a one-element set. A finite set is countable, so the theorem holds. We assume $X \neq \varnothing$ for the remainder of the proof.
[/step]
[step:Obtain a surjection $\mathbb{N} \to X^\star$ from the preceding theorem]
Since $X$ is nonempty and countable, by the [Countability of $X^\star$](/theorems/1774) there exists a surjection
\begin{align*}
\sigma: \mathbb{N} &\to X^\star.
\end{align*}
Fix such a $\sigma$.
[/step]
[step:Define the forgetful map from strings to finite subsets]
Define
\begin{align*}
f: X^\star &\to \operatorname{Fin}(X) \\
(x_1, x_2, \dots, x_n) &\mapsto \{x_1, x_2, \dots, x_n\},
\end{align*}
with the convention that $f(\varepsilon) = \varnothing$ for the empty string $\varepsilon$. For any string $w = (x_1, \dots, x_n) \in X^\star$ the image $\{x_1, \dots, x_n\}$ is a subset of $X$ of cardinality at most $n < \infty$, hence an element of $\operatorname{Fin}(X)$. Thus $f$ is well-defined.
[/step]
[step:Show that the forgetful map $f$ is surjective]
Let $F \in \operatorname{Fin}(X)$. We construct a string $w \in X^\star$ with $f(w) = F$.
If $F = \varnothing$, take $w = \varepsilon$; then $f(\varepsilon) = \varnothing = F$.
Otherwise $F$ is a nonempty finite subset of $X$, say $F = \{y_1, y_2, \dots, y_k\}$ with $k \geq 1$ and the $y_j$ pairwise distinct. Let $\pi: \mathbb{N} \to X$ be a fixed surjection (available because $X$ is nonempty and countable). For each $j \in \{1, \dots, k\}$ the preimage $\pi^{-1}(\{y_j\}) \subseteq \mathbb{N}$ is nonempty by surjectivity of $\pi$; by the [Well-Ordering Principle](/theorems/???) on $\mathbb{N}$, the set $\pi^{-1}(\{y_j\})$ has a least element
\begin{align*}
n_{y_j} &:= \min \pi^{-1}(\{y_j\}) \in \mathbb{N}.
\end{align*}
Since the $y_j$ are pairwise distinct, the integers $n_{y_1}, \dots, n_{y_k}$ are pairwise distinct (they lie in disjoint preimages). List them in increasing order as $n_{(1)} < n_{(2)} < \dots < n_{(k)}$ and define
\begin{align*}
w &:= (\pi(n_{(1)}), \pi(n_{(2)}), \dots, \pi(n_{(k)})) \in X^\star.
\end{align*}
Then the letters of $w$ are precisely the elements $y_1, \dots, y_k$ in some order, so
\begin{align*}
f(w) &= \{\pi(n_{(1)}), \dots, \pi(n_{(k)})\} = \{y_1, \dots, y_k\} = F.
\end{align*}
Hence $f$ is surjective.
[guided]
The construction picks a canonical "witness string" for each finite set $F$. The issue is that $F$ is an unordered set while $X^\star$ consists of ordered strings, so we need a rule for choosing an order. The surjection $\pi: \mathbb{N} \to X$ gives one: for each $y \in F$, pick the smallest natural number $n_y$ that $\pi$ sends to $y$, and then order the $y$'s according to the size of $n_y$. This produces a well-defined string $w$ whose set of letters equals $F$, which is exactly what $f$ collapses $w$ down to. Well-ordering of $\mathbb{N}$ is what lets us pick the "smallest" preimage without appealing to the axiom of choice.
[/guided]
[/step]
[step:Compose to obtain a surjection $\mathbb{N} \to \operatorname{Fin}(X)$]
Define
\begin{align*}
f \circ \sigma: \mathbb{N} &\to \operatorname{Fin}(X) \\
k &\mapsto f(\sigma(k)).
\end{align*}
The composition of surjections is a surjection: given $F \in \operatorname{Fin}(X)$, by surjectivity of $f$ there exists $w \in X^\star$ with $f(w) = F$, and by surjectivity of $\sigma$ there exists $k \in \mathbb{N}$ with $\sigma(k) = w$, whence $(f \circ \sigma)(k) = f(w) = F$. The existence of a surjection $\mathbb{N} \to \operatorname{Fin}(X)$ is the definition of countability, so $\operatorname{Fin}(X)$ is countable.
[/step]
