This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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