Solution
= Solution
We work in the ambient theory <ZFC> for this question. Write $t(x)=\operatorname{TC}(\{x\})$, using the <transitive closure> convention that $t(x)$ contains $x$ and all its membership descendants.
\b[First construct a set containing exactly the intended objects.] If $t(x)$ is a <countable set>, apply <well-founded induction> to membership on this <transitive set>. If all members $z$ of $y\in t(x)$ have <countable> <set-theoretic rank>, then
$$
\operatorname{rank}(y)=\sup_{z\in y}\bigl(\operatorname{rank}(z)+1\bigr)<\omega_1.
$$
Indeed $y\subseteq t(x)$ is <countable>, and a <countable union of countable sets> is <countable> in <ZFC>. The induction therefore gives $\operatorname{rank}(x)<\omega_1$. The collection
$$
C=\{x\in V_{\omega_1}:t(x)\text{ is countable}\}
$$
is now a genuine <set> by the <axiom schema of separation> inside the <cumulative hierarchy> level $V_{\omega_1}$, and it contains every <hereditarily countable set>. It is a <transitive set>, since $y\in x$ implies $t(y)\subseteq t(x)$.
If $a$ is a <countable> subset of $C$, then
$$
t(a)\subseteq\{a\}\cup\bigcup_{x\in a}t(x).
$$
The right side is <countable>, so $a\in C$. Thus $C$ has <countable-subset closure>. This proves existence of a set with the required closure before taking any intersection.
To make the least-set argument precise, form the nonempty set
$$
\mathcal F=\{B\subseteq C:\text{every countable subset of }B\text{ belongs to }B\}.
$$
It is a subset of $\mathcal P(C)$ and contains $C$. Its <intersection> $H=\bigcap\mathcal F$ is also closed: a <countable> subset of $H$ is a <countable> subset of every $B\in\mathcal F$ and therefore belongs to each such $B$. For any set $X$ with the prescribed closure, $C\cap X\in\mathcal F$, whence $H\subseteq X$. This is leastness among all such sets, not just among subsets of $C$.
Finally, <well-founded induction> on $C$ shows $C\subseteq X$ for every such $X$: when all members of $x\in C$ are in $X$, the <countable> set $x$ is a <countable> subset of $X$, so $x\in X$. Hence $H=C$, proving that the definition gives precisely
$$
\boxed{HC=\{x:\operatorname{TC}(\{x\})\text{ is countable}\}.}
$$
\b[For the cardinal bound, code the entire <countable> membership ancestry.] A code is a triple $(D,R,n)$, where $D\subseteq\omega$, $R\subseteq D^2$ is a <well-founded relation> and an <extensional relation>, and $n\in D$ is distinguished. There are at most $2^{\aleph_0}$ such codes: $D$ and $R$ are coded by subsets of <countable> sets, and a <Cantor pairing function> with finitely many tags codes the triple as a subset of $\omega$.
The <well-founded recursion>
$$
c_R(k)=\{c_R(l):lRk\}
$$
defines its collapse, as in the <Mostowski collapse theorem>. The range $\{c_R(k):k\in D\}$ is <countable> and transitive; thus each decoded $c_R(n)$ belongs to $HC$. Conversely, for $x\in HC$, choose a <bijection> $e:D\to t(x)$ and the point $n$ with $e(n)=x$. Set $lRk$ exactly when $e(l)\in e(k)$. Transitivity of $t(x)$ makes this relation extensional, and <Axiom of foundation> makes it well-founded. The recursion then gives $c_R(k)=e(k)$, so this code decodes to $x$.
We have a <surjection> from a set of at most continuum many codes onto $HC$. Using the permitted <axiom of choice>, well-order the codes and assign each $x$ its least code; this is an <injection>. In fact every subset of $\omega$ is hereditarily <countable>, giving the reverse bound as well:
$$
\boxed{|HC|=2^{\aleph_0},\quad\text{in particular }|HC|\le 2^{\aleph_0}.}
$$
Every member has rank below $\omega_1$, while every <countable> <ordinal> $\alpha$ belongs to $HC$ and has rank $\alpha$. Consequently
$$
\boxed{\operatorname{rank}(HC)=\omega_1.}
$$
\b[The axioms hold except Power Set.] <axiom of extensionality> and <Axiom of foundation> are inherited by this transitive structure. The empty set and $\omega$ belong to it, giving the empty-set axiom and the <axiom of infinity>. The <axiom of pairing> follows from <countable>-subset closure. For $a\in HC$, $\bigcup a$ is a <countable> subset of $HC$, giving the <Axiom of union>. Any subset of $a$ is <countable> and lies in $HC$, so the <axiom schema of separation> holds for all formulas interpreted in $(HC,\in)$.
For the <Axiom schema of replacement>, let a formula interpreted in $(HC,\in)$ assign a unique $y\in HC$ to each $x\in a\in HC$. Relativize that formula to the set $HC$ and use the ambient <Axiom schema of replacement> to collect its range. The range is <countable> and consists of members of $HC$, hence belongs to $HC$. The same argument, selecting one witness for each member of the <countable> domain, proves <axiom schema of collection>. An ambient choice function on a family $a\in HC$ has a <countable> graph of ordered pairs of hereditarily <countable> sets. Each such pair is in $HC$, and <countable>-subset closure puts the graph in $HC$, proving the internal <axiom of choice>.
However, all external subsets of $\omega$ are elements of $HC$. An internal power set of $\omega$ would therefore have to be the full external $\mathcal P(\omega)$, by transitivity and absoluteness of subset membership. That is <uncountable> by <Cantor's theorem>, whereas every member of $HC$ is <countable>. Thus the <axioms satisfied by hereditarily countable sets> are
$$
\boxed{HC\models\mathrm{ZFC}\text{ with Power Set deleted},\qquad
HC\not\models\mathrm{Power\ Set}.}
$$
Here the asserted axiom list includes both <Axiom schema of replacement> and <axiom schema of collection>; no equivalence relying on Power Set is being silently invoked.