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