But why should there be a definable Vitali set? Of course, some models of set theory have definable Vitali sets, because sometimes there is even a definable well-ordering of the reals, but the question asks for a parameter-free definition that provably works in every model of set theory.

What I meant about Completeness being a foregone conclusion, is that when you start proving Completeness, you periodically need to know various things about the formal system you defined. So, if you are not so interested in having the optimal proof system, then you can simply add them to the system on the fly as the proof proceeds. Of course, this method only works because the theorem is true! But it does mean that you don't have to remember the exact proof system in advance, as long as you remember the essential proof outline.

Yes, that proof was merely about the finite obstacle, which Compactness provides. The situations where one seems to need Completeness over Compactness, as I mentioned in my answer, have to do with the effectivity of the finite obstacle, for example, when if the question concerns the computability of a theory or model, or whether there is a computable procedure for eliminating quantifiers, and so on.

Preserving join implies preserving the order, since a is less than or equal to b iff a v b =b, so this would give f(a) v f(b) = f(b), which means f(a) is less than or equal to f(b).

Yes, that's right. It is exactly the same idea.

Upon reflection, I had to back off my KM claim somewhat, since the argument I had in mind uses some additional assumptions. I've been thinking of writing a short paper on this topic, the extent to which models of set theory have end-extensions, since there are some interesting things happening with it.