"Too large" is an informal description of what goes wrong, and is not entirely on point for understanding how ZFC doesn't allow you to do this.
It would be more honest to describe the problem as
There is simply no axiom in ZFC that will let you conclude that the notation $\{ x \cup \{y\} \mid x\in a, y\notin x\}$ describes any set that exists.
Remember that ZFC doesn't support free-wheeling use of the set builder noation which assumes that $\{y\mid \phi(y) \}$ (where $\phi$ is some logical formula) always describes a set. Instead you have only separation which tells you that expressions of the form $\{y\in A\mid \phi(y)\}$ describe sets, and replacement which tells you that expressions of the form $\{F(y)\mid y\in A\}$ -- where $F$ is some function that you can define by a logical formula -- are sets.
However, $\{ x \cup \{y\} \mid x\in a, y\notin x\}$ doesn't have this form -- instead it would fit the scheme $\{ F(y) \mid \phi(y) \}$, and neither Separation nor Replacement promises to work for that situation.
(If you haven't seen the axioms of ZFC written down, it would probably help your understanding to seek out an explanation of them. In particular, what I describe as, for example, "$\{y\in A\mid \phi(y)\}$ exists" is formally described by saying that for any formula $\phi(y)$ that doesn't contain $x$, the formula
$$ \exists x.\forall y.(y\in x \iff y\in A \land \phi(y)) $$
is an axiom).
The "too large to be a set" is at most a hint at an answer to a different question, namely
- Why can't we just have some more axioms that say we can do this?
The answer to this is that we can actually prove that $\{x\cup \{y\}\mid x\in A, y\notin x\}$ does not exist (which is different from not being able to prove that it does) -- so if we had an axiom that claimed that it did exist, the system would become inconsistent.
In more detail, the proof might go: Suppose that for some set $A$,
$$\sigma(A) = \{x\cup \{y\}\mid x\in A, y\notin x\}$$
exists. Then $\bigcup A \cup \bigcup\sigma(A)$ -- which must exist due to ZFCs explicit Axiom of Unions -- would be a set that contains all elements of $A$, as well as all elements of elements of $A$, as well as every set that is in neither of these groups. In other words, this would be a set of all sets, and then Russell's paradox would lead us to a contradiction.
Presenting only this second argument, without explaining (or stressing) the first one, is a common failing of semi-popular descriptions of set theory. It can easily give a reader the impression that something must be allowed unless we can see it leads to a paradox, which is most definitely not how axiomatic set theory works. Axiomatic set theory works by saying from the beginning, "these are the things that are allowed" and then hoping no combination of those things lead to a paradox.
The only real value of the "if you could do this, it would lead to a paradox" argument is that once you see it you can stop trying to figure out a way that it is allowed.
The cardinality function is well-defined, but it is what known as a class function. Since every set has a cardinality, the domain of the function $A\mapsto |A|$ has to be the class of all sets, so this is indeed a proper class. And since every set has a strictly large cardinal, the class of cardinals is not a set either.
Using the axioms of set theory, we can canonically determine an object, in the set theoretic universe, which will represent the cardinal $|A|$. So the function $A\mapsto|A|$ is indeed definable.
It should be pointed, perhaps, that this class function is also amenable. Namely, restricting it to any set of sets will result in a function which is itself a set. Namely, a set of sets can only have a set of distinct cardinals. This is a direct consequence of the Replacement axiom.
There is some inherent difficulty at first when talking about existence of proper classes, and whether or not they are well-defined objects. In the case of $\sf ZFC$ and related theories, existence means "a set", but when we say that a class exists and it is well-defined, we mean to say that there is a definition which is provably giving us the function that we want. This is the case in your question.
But one can also work in class theories like $\sf KM$ (Kelley–Morse) or $\sf NBG$ (von Neumann–Godel–Bernays), and there the function assigning every set its cardinality is still a class function and not a set, but now it exists in "an internal way" as an object of the universe.
Best Answer
Basically, yes. The problem is that the collection of all equivalent sets is a proper class (except in the case of the empty set). Thus to work with the notion of cardinality in set theory, it is convenient to define some representative of the class that is a set.
The most common solution is to use the axiom of choice and define the cardinality as the smallest ordinal in the class. In the absence of choice, one can instead appeal to foundation and define it as the subset consisting of the sets of lowest rank.