Cumulative hierarchy construction in ZFC, category of sets in ZFC This is probably a dumb question, but

How is the proof that all sets lie inside the cumulative hierarchy carried out in $ZFC$?

In particular, I'd like to understand it in ZFC and not GBC/MK or any other system allowing reference to proper classes. The text I use for a reference is Donald Monk's Introduction to Set Theory (where the system used is MK) -- he constructs the rank function $\rho$ on the universe (p.112) by recursion as $$\rho(x)=\min\{\alpha:\forall y\in x(\rho(y)<\alpha)\}$$ then proceeds to show that rank interacts with powersets etc. in the expected way, defining ${\bf M}_\alpha$ to mean the $\alpha^{th}$ stage of the cumulative hierarchy (all sets of rank less than $\alpha$), showing that $\mathcal{P}({\bf M}_\alpha)={\bf M}_{\alpha+1}$, that ${\bf M}_\alpha=\bigcup_{\beta<\alpha}M_\beta$ for limit $\alpha$, and finally that $V=\bigcup_{\alpha\in O_n}{\bf M}_\alpha$.
This is all done in MK, so statements like '$V=\bigcup_{\alpha\in O_n}{\bf M}_\alpha$' have a well defined meaning, but if we drop down to $ZFC$ this statement isn't well defined since the left and right hand sides aren't sets.

Is there a standard reference for this construction carried out in $ZFC$, or could someone give a quick sketch of how to view the cumulative hierarchy from within $ZFC$ and how to state the fact that all sets appear inside it?

I could see a 'Scott's trick' statement like $\forall x\exists\alpha(x\in{\bf M}_\alpha)$ standing in for $V=\bigcup_{\alpha\in O_n}{\bf M}_\alpha$; is this the standard approach?
On a related note, what is the standard definition of the category of sets in $ZFC$? As far as I'm aware we at least need to be able to define the 'collection of objects' for a category, wether we want to use the one hom-set definition or the many hom-set definition; how is the category of sets usually defined within ZFC?
 A: I think you're over-thinking this. The $\mathsf{MK}$ approach you describe does not use $\mathsf{MK}$, or indeed classes at all, in any essential way. To $\mathsf{ZFC}$ify it, we just replace the specific classes used with their defining formulas. For example, we can whip up a formula $\rho(x,y)$ which intuitively says "$y$ is an ordinal and $x$ has rank $\le y$." The theorem you're asking about just says "$\forall x\exists y(\rho(x,y))$," and there are no subtleties in porting over the proof: basically, using the term "non-cumulative" to refer to a putative counterexample, we show that every non-cumulative set must have a non-cumulative element and then apply regularity (after constructing the transitive closure and applying separation, if you want to avoid using choice).
Or, as in your previous question, we can use sequences to prove a sharper result. First, we prove that for every ordinal $\alpha$ there is exactly one sequence $s_\alpha$ of length $\alpha$ such that $s_\alpha(0)=\emptyset$, $s_\alpha(\beta+1)=\mathcal{P}(s_\alpha(\beta))$ for $\beta+1<\alpha$, and $s_\alpha(\lambda)=\bigcup_{\beta<\lambda}s_\alpha(\beta)$ for $\lambda<\alpha$ a limit. This $s_\alpha$ is just $\langle V_\beta\rangle_{\beta<\alpha}$. We can then prove that every set is an element of $s_{\alpha+1}(\alpha)$ for some $\alpha$, using exactly the same outline above. (And actually this isn't really any different from the previous paragraph, since sequences are already used in this exact way in the construction of $\rho$.)
None of this in any way goes outside $\mathsf{ZFC}$, or even $\mathsf{ZF}$. Replacement is necessary, however; for example, it's consistent with $\mathsf{ZC}$ (= $\mathsf{ZFC}$ minus replacement) that $V_\omega$ doesn't exist, so a fortiori only finite sets are contained in the cumulative hierarchy.

As to the category of sets, just use the formula $x=x$. In $\mathsf{ZFC}$, all things are sets, so the object-class is just the universe itself.
