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