Definition df-sucmap 39394

Description: Define the successor map, directly as the graph of the successor operation, using only elementary set theory (ordered-pair class abstraction). This avoids committing to any particular construction of the successor function/class from other operators (e.g. a union/composition presentation), while remaining provably equivalent to those presentations (cf. dfsucmap2 39396 and dfsucmap3 39395 vs. df-succf 36634 and dfsuccf2 36705). For maximum mappy shape, see dfsucmap4 39397.

We also treat the successor relation as the default shift relation for grading/tower arguments (cf. df-shiftstable 39414). Because it is used pervasively in shift-lift infrastructure, we adopt the short name SucMap rather than the fully systematic "SucAdjLiftMap".

You may also define the predecessor relation as the converse graph "PreMap" as ^◡ SucMap, which reverses successor edges ( cf. cnvopab 6131) and sends each successor to its (unique) predecessor when it exists. (Contributed by Peter Mazsa, 25-Jan-2026.)

Assertion

Ref	Expression
df-sucmap	⊢ SucMap = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}

Distinct variable group:   𝑚,𝑛

Detailed syntax breakdown of Definition df-sucmap

Step	Hyp	Ref	Expression
1		csucmap 39110	. 2 class SucMap
2		vm	. . . . . 6 setvar 𝑚
3	2	cv 1569	. . . . 5 class 𝑚
4	3	csuc 6364	. . . 4 class suc 𝑚
5		vn	. . . . 5 setvar 𝑛
6	5	cv 1569	. . . 4 class 𝑛
7	4, 6	wceq 1570	. . 3 wff suc 𝑚 = 𝑛
8	7, 2, 5	copab 5167	. 2 class {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
9	1, 8	wceq 1570	1 wff SucMap = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}

This definition is used by:  dfsucmap3  39395  dfsucmap4  39397  brsucmap  39398  relsucmap  39399  dfsuccl2  39402