This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-succl

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)

		Ref	Expression
	Assertion	df-succl	Could not format assertion : No typesetting found for \|- Suc = ran SucMap with typecode \|-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csuccl	Could not format Suc : No typesetting found for class Suc with typecode class
1		csucmap	Could not format SucMap : No typesetting found for class SucMap with typecode class
2	1	crn	Could not format ran SucMap : No typesetting found for class ran SucMap with typecode class
3	0 2	wceq	Could not format Suc = ran SucMap : No typesetting found for wff Suc = ran SucMap with typecode wff