I am interested in proving the titular claim:
Transitive Closure of a Well-Founded Relation is Well-Founded (without Axiom of Choice)
My approach:
Let $R$ be a well-founded relation. We construct the transitive closure $R^t$ as the union of the range of $F:\mathbb{N}\to \mathrm{fld}(R)\times\mathrm{fld}(R)$ defined (inductively) by $$ F(0)=R\qquad\text{and}\qquad F(n+1)=F(n)\circ R $$ for every $n\in\mathbb{N}$. That is to say, $R^t\overset{\mathrm{def}}{=}\bigcup\mathrm{ran}(F)=\bigcup_{i=0}^\infty F(i)$...
My thought process:
I can show that for each natural number $n$, $\bigcup_{i=0}^nF(i)$ is well-founded given that $R$ is well-founded (by induction on $n$), but that doesn't imply that $R^t$ is well-founded. It seems I need some sort of "transfinite induction" argument where if all the "finite" predecessors $\bigcup_{i=0}^nF(i)$ are well-founded, then $\bigcup_{i=0}^\infty F(i)$ is well-founded (but I don't think we necessarily have a well-ordered set to make such an argument).
Any hints/advice is much appreciated!
(The reason I want to work in ZF is because Enderton's Elements of Set Theory pg 244 gives a proof using AC, but remarks as an exercise to give a proof without it)
Suppose that $R$ is well-founded, and let $A$ be any nonempty subset of its field. We wish to show that $A$ contains an $R^t$-minimal element.
Let $B$ consist of all elements of $A$, plus every element of every finite $R$-sequence that connects two elements of $A$.
Because $R$ is well-founded, $B$ contains an $R$-minimal element $b$. The elements that were added to $B$ as intermediate elements of $R$-sequences cannot, by construction, be $R$-minimal, so we must have $b\in A$.
I claim that $b$ is $R^t$-minimal in $A$ -- because it it were not, it would sit at the top of an $R$-sequence that witnesses $\langle a,b\rangle\in R^t$, and the penultimate element of that sequence would be a predecessor of $b$ in $B$, contradicting $b$ being $R$-minimal in $B$.
Thus, $R^t$ is well founded.