This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 |-