I proved the following claim (source image), can you tell me if my proof is correct? Thanks:
Claim 4: Let $R$ be a binary relation on a set $X$, and suppose $\langle Y, \prec \rangle$ is a strict w.o. If there exists a function $rk : X \to Y$ such that $$ \forall x, y \in X (x \neq y \land \langle x, y \rangle \in R \to rk(x) \prec rk(y)), \tag{*}$$ then the relation $R$ is wellfounded.
where we use the following definition of wellfounded:
$\newcommand{\pair}[2]{\langle#1,#2\rangle}$
Definition 3: Let $R$ be a binary relation on a set $X$. We say that $R$ is wellfounded, if for every nonempty subset $Y \subseteq X$ there exists a $z \in Y$ such that $\pair yz \notin R$ for all $y \in Y\setminus \{z\}$. A relation $R$ is strictly wellfounded if it is wellfounded and irreflexive.
Proof:
Assume $R$ is not well-founded. Then there exists an infinite $R$-descending sequence $(x_n)$ such that $(x_{n+1}, x_n) \in R$, $n \in \mathbb N$, so that $S = \{x_n \mid n \in \mathbb N\}$ does not have an $R$-minimal element. Then $f(S)$ is a subset of $Y$ containing an infinite $R$-descending sequence $(f(x_{n+1}), f(x_n)) \in \prec$ which is a contradiction to $(Y,\prec)$ being well-founded.
First, a notational error: $(x_{n+1},x_n)\in R$ does not describe a describe a sequence. What you mean is that there is a sequence $\langle x_n:n\in\Bbb N\rangle$ in $X$ such that $\langle x_{n+1},x_n\rangle\in R$ for each $n\in\Bbb N$. There’s no need for the scare quotes; just call it an $R$-descending sequence, or a descending sequence with respect to $R$. Similarly, there’s no good reason for the scare quotes on minimal: just say $R$-minimal.
Thus substance of the argument is correct, but it’s unnecessarily complicated. Let $A$ be any non-empty subset of $X$. Then $rk[A]$ is a non-empty subset of $Y$, so it has a $\prec$-least element $y$. Let $a\in A$ be such that $rk(a)=y$. If $\langle x,a\rangle\in R$ for some $x\in X$, then $rk(x)<y$, and therefore $x\notin A$. Thus, $a$ is an $R$-minimal element of $A$, and $R$ is well-founded.