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 
|- ( N e. Suc -> suc pre N = N )

Proof

Step Hyp Ref Expression
1 presucmap 
 |-  ( N e. ran SucMap -> pre N SucMap N )
2 preex 
 |-  pre N e. _V
3 brsucmap 
 |-  ( ( pre N e. _V /\ N e. ran SucMap ) -> ( pre N SucMap N <-> suc pre N = N ) )
4 2 3 mpan 
 |-  ( N e. ran SucMap -> ( pre N SucMap N <-> suc pre N = N ) )
5 1 4 mpbid 
 |-  ( N e. ran SucMap -> suc pre N = N )
6 df-succl 
 |-  Suc = ran SucMap
7 5 6 eleq2s 
 |-  ( N e. Suc -> suc pre N = N )