# Very large axiom of choice

let me say that I am not a set theorist, but I have to settle up some things in category theory and I need your help.

What I'd like to do is, in some way, use axiom of choice for proper classes. I say that axiom of choice holds for a set $$X$$ if there exist a function $$f:X \to \bigcup X$$ such that $$f(x) \in x$$.

My attempt is the following:

Assume the Tarski Grothendieck axiom, i.e. every set is contained in a Grothendieck Universe.

Fix a Universe $$U$$ and an enlarged universe $$U^+$$ that contains $$U$$. Now note that every subset of $$U$$, i.e. a $$U$$ proper class, is contained in $$U^+$$ by the subset axiom. Now I read from wikipedia that "axiom of choice holds" in Tarski Grothendieck framework. My question is:

Does the axiom of choice holds in TG for every element of some universe?

This would mean that for every subset of $$U$$, axiom of choice holds, being an element of $$U^+$$. To be honest, I would be ok with the following:

Does the axiom of choice holds for a Universe? Can you provide a reference?

If you have ZFC in the ambient theory, including the axiom of choice, then indeed the axiom of choice holds in every Grothendieck-Zermelo universe (also sometimes known as Grothendieck universes). A Grothendieck-Zermelo universe is a rank-initial segment $$V_\kappa$$ of the cumulative hierarchy, where $$\kappa$$ is an inaccessible cardinal. And every set in $$V_\kappa$$ has a well-ordering in $$V$$, by the axiom of choice in the ambient theory, and this order must also be in $$V_\kappa$$, since $$V_\kappa$$ is closed under subsets of its elements.
• Wow! Thank you very much. Another question: now let's suppose I just need choice for the class of finite sets, and the class $\{X: |X| = k\}$, where $k$ is some fixed cardinal (the cardinality of $\mathbb{R}$ is ok for me). Which axioms would you suggest me to assume? I suspect that TG is not necessary, even if it solves the issue. On the other side, it seems to me that there are " a lot" of finite sets, in the sense that the function $\{\}: U \to Finite Sets$ that send $X$ to $\{X\}$ is injective. So... what to do? – Andrea Marino Dec 10 '19 at 15:25