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 = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }
2 1 relopabi ⊢ Rel SucMap