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	Could not format assertion : No typesetting found for |- ( M e. V -> pre suc M = M ) with typecode |-

Proof

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