Definition df-sucmap

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 and dfsucmap3 vs. df-succf and dfsuccf2 ). For maximum mappy shape, see dfsucmap4 .

We also treat the successor relation as the default shift relation for grading/tower arguments (cf. df-shiftstable ). 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 ) and sends each successor to its (unique) predecessor when it exists. (Contributed by Peter Mazsa, 25-Jan-2026)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csucmap	⊢ SucMap
1		vm	⊢ 𝑚
2		vn	⊢ 𝑛
3	1	cv	⊢ 𝑚
4	3	csuc	⊢ suc 𝑚
5	2	cv	⊢ 𝑛
6	4 5	wceq	⊢ suc 𝑚 = 𝑛
7	6 1 2	copab	⊢ { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }
8	0 7	wceq	⊢ SucMap = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }