## Proof of the Lemma on Predecessor+

We wish to prove the Lemma on Predecessor+, which asserts:

Lemma on Predecessor+:
Nx & Precedes(y,x) →
#[λz Precedes+(z,y)] = #[λz Precedes+(z,x) & zx]

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

Lemma: No Number Ancestrally Precedes Itself
x[Nx → ¬Precedes*(x,x)]

Now to prove the Lemma on Predecessor+, assume that Nn and Precedes(m,n). We want to show:

#[λz Precedes+(z,m)] = #[λz Precedes+(z,n) & zn]

By Hume's Principle, it suffices to show:

z Precedes+(z,m)] ≈ [λz Precedes+(z,n) & zn]

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

x([λz Precedes+(z,m)]x ≡ [λz Precedes+(z,n) & zn]x)

And by λ-Conversion, it suffices to show:

x[Precedes+(x,m)  ≡  Precedes+(x,n) & xn]

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

Precedes+(a,m)  ≡  (Precedes+(a,n) & an)

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

Precedes+(a,n) & an

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