In both Lang's Algebra and Atiyah, MacDonald, Introduction to Commutative Algebra, the following construction of the algebraic closure is atributed to Artin:
(Atiyah, MacDonald, exercises of Chapter 1.)
I wanted to make a question regarding the step “repeat the construction with $K_1$ in place of $K$, obtaining a field $K_2$, and so on.” Implicitly, the argument here is claiming that we can find a chain of field extensions $$ K=K_0\subset K_1\subset K_2\subset \cdots $$ such that, for all $j\geq 0$, the extension $K_j\subset K_{j+1}$ is algebraic and every polynomial of $K_j[x]$ has a root in $K_{j+1}$. My question is: what is the precise set-theoretic tool that allows one to get such a chain? At the beginning I would have said that it is dependent choice.
But if so, what is the set $X$ that we are applying $\mathsf{DC}$ to? It seems that $X$ must be the collection of all algebraic field extensions of $K$. But the problem is that this collection is a proper class.
(I should say perhaps that I have no background of set theory at all. One day I found out about what $\mathsf{DC}$ is and, after that, I realized that it is actually what one must use in certain things that are sometimes justified by mathematicians “by applying induction.”)