Metamath Proof Explorer

Theorem mopre

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

Ref Expression
Assertion mopre 
|- E* m suc m = N

Proof

Step Hyp Ref Expression
1 eqtr3 
 |-  ( ( suc m = N /\ suc l = N ) -> suc m = suc l )
2 suc11reg 
 |-  ( suc m = suc l <-> m = l )
3 1 2 sylib 
 |-  ( ( suc m = N /\ suc l = N ) -> m = l )
4 3 gen2 
 |-  A. m A. l ( ( suc m = N /\ suc l = N ) -> m = l )
5 suceq 
 |-  ( m = l -> suc m = suc l )
6 5 eqeq1d 
 |-  ( m = l -> ( suc m = N <-> suc l = N ) )
7 6 mo4 
 |-  ( E* m suc m = N <-> A. m A. l ( ( suc m = N /\ suc l = N ) -> m = l ) )
8 4 7 mpbir 
 |-  E* m suc m = N