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	⊢ ( 𝑁 ∈ Suc → suc pre 𝑁 = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		presucmap	⊢ ( 𝑁 ∈ ran SucMap → pre 𝑁 SucMap 𝑁 )
2		preex	⊢ pre 𝑁 ∈ V
3		brsucmap	⊢ ( ( pre 𝑁 ∈ V ∧ 𝑁 ∈ ran SucMap ) → ( pre 𝑁 SucMap 𝑁 ↔ suc pre 𝑁 = 𝑁 ) )
4	2 3	mpan	⊢ ( 𝑁 ∈ ran SucMap → ( pre 𝑁 SucMap 𝑁 ↔ suc pre 𝑁 = 𝑁 ) )
5	1 4	mpbid	⊢ ( 𝑁 ∈ ran SucMap → suc pre 𝑁 = 𝑁 )
6		df-succl	⊢ Suc = ran SucMap
7	5 6	eleq2s	⊢ ( 𝑁 ∈ Suc → suc pre 𝑁 = 𝑁 )