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

Metamath Proof Explorer

Theorem sucpre

Description: suc is a right-inverse of pre on Suc . This theorem states the partial inverse relation in the direction we most often need. (Contributed by Peter Mazsa, 27-Jan-2026)

Ref Expression
Assertion sucpre Could not format assertion : No typesetting found for |- ( N e. Suc -> suc pre N = N ) with typecode |-

Proof

Step Hyp Ref Expression
1 presucmap Could not format ( N e. ran SucMap -> pre N SucMap N ) : No typesetting found for |- ( N e. ran SucMap -> pre N SucMap N ) with typecode |-
2 preex Could not format pre N e. _V : No typesetting found for |- pre N e. _V with typecode |-
3 brsucmap Could not format ( ( pre N e. _V /\ N e. ran SucMap ) -> ( pre N SucMap N <-> suc pre N = N ) ) : No typesetting found for |- ( ( pre N e. _V /\ N e. ran SucMap ) -> ( pre N SucMap N <-> suc pre N = N ) ) with typecode |-
4 2 3 mpan Could not format ( N e. ran SucMap -> ( pre N SucMap N <-> suc pre N = N ) ) : No typesetting found for |- ( N e. ran SucMap -> ( pre N SucMap N <-> suc pre N = N ) ) with typecode |-
5 1 4 mpbid Could not format ( N e. ran SucMap -> suc pre N = N ) : No typesetting found for |- ( N e. ran SucMap -> suc pre N = N ) with typecode |-
6 df-succl Could not format Suc = ran SucMap : No typesetting found for |- Suc = ran SucMap with typecode |-
7 5 6 eleq2s Could not format ( N e. Suc -> suc pre N = N ) : No typesetting found for |- ( N e. Suc -> suc pre N = N ) with typecode |-