Theorem mopre

Description: There is at most one predecessor of N . (Contributed by Peter Mazsa, 12-Jan-2026)

	Ref	Expression
Assertion	mopre	$$⊢{\exists }^{*}m\mathrm{suc}m=N$$

Proof

Step	Hyp	Ref	Expression
1		eqtr3	$$⊢\left(\mathrm{suc}m=N\wedge \mathrm{suc}l=N\right)\to \mathrm{suc}m=\mathrm{suc}l$$
2		suc11reg	$$⊢\mathrm{suc}m=\mathrm{suc}l\leftrightarrow m=l$$
3	1 2	sylib	$$⊢\left(\mathrm{suc}m=N\wedge \mathrm{suc}l=N\right)\to m=l$$
4	3	gen2	$$⊢\forall m\forall l\left(\left(\mathrm{suc}m=N\wedge \mathrm{suc}l=N\right)\to m=l\right)$$
5		suceq	$$⊢m=l\to \mathrm{suc}m=\mathrm{suc}l$$
6	5	eqeq1d	$$⊢m=l\to \left(\mathrm{suc}m=N\leftrightarrow \mathrm{suc}l=N\right)$$
7	6	mo4	$$⊢{\exists }^{*}m\mathrm{suc}m=N\leftrightarrow \forall m\forall l\left(\left(\mathrm{suc}m=N\wedge \mathrm{suc}l=N\right)\to m=l\right)$$
8	4 7	mpbir	$$⊢{\exists }^{*}m\mathrm{suc}m=N$$