How many sets can we prove existence of in $\text{ZFC}$? $\text{ZFC}$ has, in the form I have been taught, 8 axioms (extensionality, nullset, pairs, unions, powerset, infinity, foundation, choice) and 2 axiom schemes (comprehension, replacement). Within this, some axioms are redundant (e.g. replacement supersedes comprehension) and some are a little bit different (e.g. foundation only prohibits the existence of sets), but I don't think the difference in formulation matters for my question.
My question is: how many sets can we prove existence of in any model of $\text{ZFC}$? To me, it looks like countably many, because our axiom schemes allow for countably many formulae and then we have countably many axioms which we can apply countably many times.
Then, as $\mathcal{P}(\omega)$ is uncountable, surely it follows that some $S \in \mathcal{P}(\omega)$ is not a set. But this is patently absurd: a set can only contain sets, not proper classes, right?
So perhaps I am wrong about the number of sets we can create. If the cardinality of sets we can prove true is some cardinal $\kappa$, then something in the set $\{\omega, \mathcal{P}(\omega), \mathcal{P}(\mathcal{P}(\omega)), ...\}$ has larger cardinality and then it contains something which is not a set.
Is this a proof that $\text{ZFC}$ can prove existence of a proper class of sets (because if it was a set of sets then its cardinality would give a contradiction)? And if so, how do I rectify this with the fact that we have countably many axioms?
 A: I disagree with the other answer and I think that the issue is more subtle.
Being definable is not itself definable in $\mathsf{ZFC}$, indeed if $\mathsf{ZFC}$ has any model at all, then it has one in which every object is definable without parameters. To see that the real numbers analogy doesn't work consider the example of ordinals (which I'm sure I learned from a similar question on MSE but I cannot find it right now), surely there are uncountably many ordinals, but we can always consider "the least ordinal which is not definable", so the class of definable ordinals is the whole of the ordinals. Do you see where the issue in this argument is?
Now given any model $M$ of $\mathsf{ZFC}$ we know that internally $M$ proves that there are proper class many sets, because that's a theorem of $\mathsf{ZFC}$. Externally however the whole of $M$ might even be countable! In that case inside of $M$ there is a set that $M$ believes to be $\mathcal P(\omega)$, and that $M$ believes to be uncountable, but externally we can see that there are sets in the "true" $\mathcal P(\omega)$ which are not in $M$, and externally we have a bijection between $\omega$ and $\mathcal P(\omega)^M$, but this is not a contradiction, since this bijection is not in $M$.
A: Think e.g. about real numbers. The reals between 0 and 1 are uncountable. A standard first-order theory of the reals, with a countable number of expressions, can only come up with specifications of a countable number of reals. There are, in particular, only a countable number of specifiable reals between 0 and 1.
Plainly it doesn't follow that there is a something between 0 and 1 which isn't a real. Only that there is something between 0 and 1 which isn't a real specifiable in our theory. And there is nothing at all mysterious about that. Because not all reals are specifiable in our theory.
You've raised what could be read as a parallel issue about sets. But then that is really(!) is no more mysterious! So to get a more serious issue, you need a more careful formulation of the question.
