mopre

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

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

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

Metamath Proof Explorer