Let me offer a different perspective, informed by my recent conversion from ZFC to ECTSR, i.e. Lawvere's elementary theory of the category of sets (with replacement). Recall that the two theories are "equivalent" in that each interprets the other, and models naturally correspond; the difference between them is essentially linguistic. In ECTSR, one formalizes the category of all sets. So there is a (meta?)mathematical category of *all* sets $\mathrm{Set}$. I'd like to make the following analogy:

Mathematics probably starts by counting, leading to the integers $0,1,2,\ldots$. This quickly leads one to wonder how far this goes -- is there a "largest integer"? Of course, that's an obviously self-contradictory concept.

Then there was a conceptual leap in mathematics, from mere numbers to the concept of sets. We allowed ourselves to contemplate taking all the integers, forming a new kind of object, a set. Then just like Peano arithmetic formalizes the integers on some inductive idea of the formation of integers, we formalize sets in ZFC based on some inductive idea of the formation of sets. In particular, we can form larger and larger sets. But just like for the integers, it turns out that the idea of "largest set" is self-contradictory.

In the ETCSR point of view, what we do now is to make another conceptual leap in mathematics, from sets to categories. In this conception, we allow ourselves to contemplate the category of all sets, and then also "completed" categories of groups, of rings, etc. So somehow just like for the integers, the correct question was now that of "a largest integer larger than all the others", but that of collecting all the integers into a new kind of object -- a set -- the correct question here is not that of "a largest set containing all the other sets", but that of collecting all the sets in to a new kind of object -- a category.

I realize that this perspective puts me on a (slippery?) slope that would ultimately want to formalize the category of all categories, ..., leading one to $\infty$-categories and homotopy type theory. Maybe that's the way to go, but for now I'd only take one step at a time.