Definition df-succl 39494

Description: Define Suc as the class of all successors, i.e. the range of the successor map: 𝑛 ∈ Suc iff ∃𝑚suc 𝑚 = 𝑛 (see dfsuccl2 39495). By injectivity of suc (suc11reg 9623), every 𝑛 ∈ Suc has at most one predecessor, which is exactly what pre 𝑛 (df-pre 39500) names. Cf. dfsuccl3 39498 and dfsuccl4 39499. (Contributed by Peter Mazsa, 25-Jan-2026.)

Assertion

Ref	Expression
df-succl	⊢ Suc = ran SucMap

Detailed syntax breakdown of Definition df-succl

Step	Hyp	Ref	Expression
1		csuccl 39204	. 2 class Suc
2		csucmap 39203	. . 3 class SucMap
3	2	crn 5651	. 2 class ran SucMap
4	1, 3	wceq 1569	1 wff Suc = ran SucMap

This definition is used by:  dfsuccl2  39495  eupre  39519  sucpre  39522  presuc  39523