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?