Metamath Proof Explorer

Theorem presuc

Description: pre is a left-inverse of suc . This theorem gives a clean rewrite rule that eliminates pre on explicit successors. (Contributed by Peter Mazsa, 12-Jan-2026)

Ref Expression
Assertion presuc 
|- ( M e. V -> pre suc M = M )

Proof

Step Hyp Ref Expression
1 sucmapsuc 
 |-  ( M e. V -> M SucMap suc M )
2 relsucmap 
 |-  Rel SucMap
3 2 relelrni 
 |-  ( M SucMap suc M -> suc M e. ran SucMap )
4 df-succl 
 |-  Suc = ran SucMap
5 3 4 eleqtrrdi 
 |-  ( M SucMap suc M -> suc M e. Suc )
6 sucpre 
 |-  ( suc M e. Suc -> suc pre suc M = suc M )
7 1 5 6 3syl 
 |-  ( M e. V -> suc pre suc M = suc M )
8 suc11reg 
 |-  ( suc pre suc M = suc M <-> pre suc M = M )
9 7 8 sylib 
 |-  ( M e. V -> pre suc M = M )