Theorem relsucmap

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

	Ref	Expression
Assertion	relsucmap	Could not format assertion : No typesetting found for |- Rel SucMap with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-sucmap	Could not format SucMap = { <. m , n >. | suc m = n } : No typesetting found for |- SucMap = { <. m , n >. | suc m = n } with typecode |-
2	1	relopabi	Could not format Rel SucMap : No typesetting found for |- Rel SucMap with typecode |-