# How is Zorn's lemma proven in ZF(C), actually?

I want to prove some results like that every vector space has a base without the use of Zorn's lemma becuase I want to practice set theory and become confident with things like ordinals. I have some basic understanding of ordinals that I could find online and, if I didn't miss anything, online sources don't seem to go into much detail. So, if you can, please provide me with sources from which you got the knowledge for posible answers to my question. Also, forgive me for not specifying my sources, they are basically random websites and blogs.

My understanding of that every vector space has a base as an example:

So basically we can start picking vectors that are not a linear combination of vectors we already picked until we can not do it anymore. Okay, formally, we will define a mapping from the class of ordinals to vectors using transfinite recursion. Two confusions here: for transfinite recursion, they say, we need the axiom schema of replacement and what bothers me more: how do we know that there is enough ordinals to drain the whole vector space? We can't even mention classes as they don't exist in ZF and that's why (I think) we need the axiom schema of replacement to work with collection of formulas. Now to answer the other question we can introduce the axiom of choice (which we needed for this picking the next vector anyway) and remember that every set is well-orderable. With well-order on the set of vectors we can apply transfinite recursion directly on the set of vectors and avoid the use of ordinals completely. Then we would still need this axiom schema of replacement (I think), but no ordinals. But wait, when I search for the proof that every set can be well-ordered, they use ordinals to "pick the next element". Basically the same proof I am trying to use it for.

So, how exactly can we define ordinals in ZF and, using AC, how do we derive necessary properties of them for proving results like Zorn's lemma or that every set is well-orderable?