Metamath Proof Explorer

Theorem relsucmap

Description: The successor map is a relation. (Contributed by Peter Mazsa, 7-Jan-2026)

Ref Expression
Assertion relsucmap 
|- Rel SucMap

Proof

Step Hyp Ref Expression
1 df-sucmap 
 |-  SucMap = { <. m , n >. | suc m = n }
2 1 relopabi 
 |-  Rel SucMap