$R$ well-founded relation and $\forall y$, $\{x:xRy\}$ is finite implies $\forall y$, $\{x:xR^t y\}$ is finite (where $R^t$ is the transitive closure)

Question

I am interested in proving the titular claim:

$R$ well-founded relation and $\forall y$, $\{x:xRy\}$ is finite implies $\forall y$, $\{x:xR^t y\}$ is finite (where $R^t$ is the transitive closure)

After drawing a couple of pictures/graphs it reminded me of Konig's Lemma: "every tree that contains infinitely many vertices, each having finite degree, has at least one infinite simple path."

Assuming I have no knowledge of graphs and trees, is there a proof of the claim using the definition of well-founded?

This previous question I asked is related/useful: Transitive Closure of a Well-Founded Relation is Well-Founded (without Axiom of Choice)

Answer 1

Assume that for some $y$ the set $\left\{ x\mid xR^{t}y\right\} $ is not finite and set $a_{0}:=y$.

We have $R^{t}=R\cup (R^{t}\circ R)$ and denoting $\hat{y}:=\left\{ x\mid xRy\right\} $we can write $\left\{ x\mid xR^{t}y\right\} =\hat{y}\cup\bigcup_{z\in\hat{y}}\left\{ x\mid xR^{t}z\right\} $.

Set $\hat{y}$ is finite so $\left\{ x\mid xR^{t}z\right\} $ must be infinite for at least one $z\in\hat{y}$.

Pick out such $z$ and name it $a_{1}$.

This can be repeated and a set $A:=\left\{ a_{n}\mid n=0,1,\dots\right\} $ is constructed with $a_{n+1}Ra_{n}$ for $n=0,1,\dots$.

Then $A$ has no $R$-minimal element which contradicts that $R$ is well-founded.