Would this be sufficiently "ordinary": That existence of a tree without a branch implies the existence of such a tree with a linear order on each rank?

@MihaHabič The case where inner models are definable is closer to what I want, but for this question I'm simplifying things by making $M$ countable and considering arbitrary inner models. Of course, an answer to the definable case would also be appreciated.

@MonroeEskew You seem to have misread the definition I presented. We aren't taking ground models, we're taking generic extensions. The sequence will alternate between smaller and large models, it's not monotonic.

@MonroeEskew I do, but even if we restrict to set forcing, I don't understand your argument that this collapses.

@MonroeEskew Please explain how that makes the hierarchy collapse.

@JoelDavidHamkins Isn't the well-founded part of a model of ZF-FA a model of ZF-FA+every set is bijective with a well-founded set in of itself?

"If the answer is affirmative, then the assertion that every set is bijective with a well-founded set would be conservative over ZF-FA for assertions about well-founded sets." Don't we immediately have this by restriction to the well-founded part of the universe?

No Matt, arithmetic is carried out in $\omega,$ which exists in $V_{\text{wf}}.$

Peter do you need to mention the roots of the relation in that sentence? Doesn't any non-empty well-founded extensional relation have a unique root?

You might find it interesting that the axiom in your second question requires Foundation in its prove (as well as AC, of course). I believe this axiom is called the injection principle.