Proof of Hume's Principle from Basic Law V — Grundgesetze-Style

[Note: We use εF to denote the extension of the concept F.]

Let P,Q be arbitrarily chosen concepts. We want to show:

#P = #Q ≡ P ≈ Q

(→) Assume #P = #Q (to show: P ≈ Q). Note that since P ≈ P (this is Fact 2 in the subsection on Equinumerosity), we know by the previous Lemma that εP ∈ #P. But then, by identity substitution, εP ∈ #Q. So, by our previous Lemma, P ≈ Q.

(←) Assume P ≈ Q (to show: #P = #Q). By definition of #, we have to show εP^≈ = εQ^≈. So, by Basic Law V, we have to show ∀x(P^≈x ≡ Q^≈x). We pick an arbitrary object b (to show: P^≈b ≡ Q^≈b).

(→) Assume P^≈b. Then, by definition of P^≈ and λ-Conversion, ∃H(b = εH & H ≈ P). Let R be an arbitrary such concept; so b = εR & R ≈ P. From the second conjunct and our initial hypothesis, it follows (by the transitivity of equinumerosity) that R ≈ Q. So, reassembling what we know, it follows that b = εR & R ≈ Q. By existential generalization, it follows that ∃H(b = εH & H ≈ Q). So by λ-Conversion,

[λx ∃H(x = εH & H ≈ Q)]b

It follows from this, by definition, that Q^≈b.

(←) (Exercise)