Theorem mopre

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

	Ref	Expression
Assertion	mopre	⊢ ∃* 𝑚 suc 𝑚 = 𝑁

Proof

Step	Hyp	Ref	Expression
1		eqtr3	⊢ ( ( suc 𝑚 = 𝑁 ∧ suc 𝑙 = 𝑁 ) → suc 𝑚 = suc 𝑙 )
2		suc11reg	⊢ ( suc 𝑚 = suc 𝑙 ↔ 𝑚 = 𝑙 )
3	1 2	sylib	⊢ ( ( suc 𝑚 = 𝑁 ∧ suc 𝑙 = 𝑁 ) → 𝑚 = 𝑙 )
4	3	gen2	⊢ ∀ 𝑚 ∀ 𝑙 ( ( suc 𝑚 = 𝑁 ∧ suc 𝑙 = 𝑁 ) → 𝑚 = 𝑙 )
5		suceq	⊢ ( 𝑚 = 𝑙 → suc 𝑚 = suc 𝑙 )
6	5	eqeq1d	⊢ ( 𝑚 = 𝑙 → ( suc 𝑚 = 𝑁 ↔ suc 𝑙 = 𝑁 ) )
7	6	mo4	⊢ ( ∃* 𝑚 suc 𝑚 = 𝑁 ↔ ∀ 𝑚 ∀ 𝑙 ( ( suc 𝑚 = 𝑁 ∧ suc 𝑙 = 𝑁 ) → 𝑚 = 𝑙 ) )
8	4 7	mpbir	⊢ ∃* 𝑚 suc 𝑚 = 𝑁