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

Proof

Step	Hyp	Ref	Expression
1		sucmapsuc	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 SucMap suc 𝑀 )
2		relsucmap	⊢ Rel SucMap
3	2	relelrni	⊢ ( 𝑀 SucMap suc 𝑀 → suc 𝑀 ∈ ran SucMap )
4		df-succl	⊢ Suc = ran SucMap
5	3 4	eleqtrrdi	⊢ ( 𝑀 SucMap suc 𝑀 → suc 𝑀 ∈ Suc )
6		sucpre	⊢ ( suc 𝑀 ∈ Suc → suc pre suc 𝑀 = suc 𝑀 )
7	1 5 6	3syl	⊢ ( 𝑀 ∈ 𝑉 → suc pre suc 𝑀 = suc 𝑀 )
8		suc11reg	⊢ ( suc pre suc 𝑀 = suc 𝑀 ↔ pre suc 𝑀 = 𝑀 )
9	7 8	sylib	⊢ ( 𝑀 ∈ 𝑉 → pre suc 𝑀 = 𝑀 )