## Proof of the Lemma on Predecessor$$^{+}$$

We wish to prove the Lemma on Predecessor$$^{+}$$, which asserts:

Lemma on Predecessor$$^{+}$$:
\begin{align*} &Nx\amp \mathit{Precedes}(y,x) \rightarrow \\ &\quad \#[\lambda z \,\mathit{Precedes}^{+}(z,y)] = \#[\lambda z \,\mathit{Precedes}^{+}(z,x)\amp z \neq x] \end{align*}

Now this Lemma can be proved with the help of the following Lemma:

Lemma: No Number Ancestrally Precedes Itself
$$\forall x[Nx\rightarrow\neg\mathit{Precedes}^{*}(x,x)]$$

Now to prove the Lemma on Predecessor$$^{+}\!$$, assume that $$Nn$$ and $$\mathit{Precedes}(m,n)$$. We want to show:

$$\#[\lambda z \, \mathit{Precedes}^{+}(z,m)] = \#[\lambda z \, \mathit{Precedes}^{+}(z,n)\amp z \neq n]$$

By Hume's Principle, it suffices to show:

$$[\lambda z \, \mathit{Precedes}^{+}(z,m)]\approx [\lambda z \, \mathit{Precedes}^{+}(z,n)\amp z \neq n]$$

Now it is a fact about equinumerosity (Fact 1, Facts About Equinumerosity, §3) that if two concepts are materially equivalent, then they are equinumerous. It therefore suffices to show that

$$\forall x([\lambda z \, \mathit{Precedes}^{+}(z,m)]x\equivwide [\lambda z \, \mathit{Precedes}^{+}(z,n)\amp z \neq n]x)$$

And by $$\lambda$$-Conversion, it suffices to show:

$$\forall x[\mathit{Precedes}^{+}(x,m) \equivwide \mathit{Precedes}^{+}(x,n)\amp x \neq n]$$

So let us pick an arbitrary object, say $$a$$, and show:

$$\mathit{Precedes}^{+}(a,m) \equivwide (\mathit{Precedes}^{+}(a,n)\amp a \neq n)$$

$$(\rightarrow)$$ Assume $$\mathit{Precedes}^{+}(a,m)$$. Then from our assumption that $$\mathit{Precedes}(m,n)$$ and a Fact about $$R^{+}$$ (Fact 3, Facts About $$R^{+}\!$$, §4, Weak Ancestral), it follows that $$\mathit{Precedes}^{*}(a,n)$$. A fortiori, then, $$\mathit{Precedes}^{+}(a,n)$$. Now by the Lemma mentioned at the outset of this proof, namely, No Natural Number Ancestrally Precedes Itself, we know that $$\neg \mathit{Precedes}^{*}(n,n)$$. Since $$a$$ ancestrally precedes $$n$$ and $$n$$ does not, it follows that $$a\neq n$$. We have therefore proved what we were after, namely:

$$\mathit{Precedes}^{+}(a,n)\amp a\neq n$$

$$(\leftarrow)$$ Assume $$\mathit{Precedes}^{+}(a,n)$$ and $$a\neq n$$. By definition, the first conjunct tells us that either $$\mathit{Precedes}^{*}(a,n)$$ or $$a = n$$. Since we know by assumption that the latter disjunct is not true, we know $$\mathit{Precedes}^{*}(a,n)$$. But from this fact, the fact that Predecessor is 1-1, and our assumption that $$\mathit{Precedes}(m,n)$$, it follows from a fact about $$R^{+}$$ (Fact 8, Facts About $$R^{+}$$, §4, Weak Ancestral), that $$\mathit{Precedes}^{+}(a,m)$$, which is what we had to show.