Definition df-pre

Description: Define the term-level successor-predecessor. It is the unique m with suc m = N when such an m exists; otherwise pre N is the arbitrary default chosen by iota . See its alternate definitions dfpre , dfpre2 , dfpre3 and dfpre4 .

Our definition is a special case of the widely recognised general R -predecessor class df-pred (the class of all elements m of A such that m R N , dfpred3g , cf. also df-bnj14 ) in several respects. Its most abstract property as a specialisation is that it has a unique existing value by default. This is in contrast to the general version. The uniqueness (conditional on existence) is implied by the property of this specific instance of the general case involving the successor map df-sucmap in place of R , so that m SucMap N , cf. sucmapleftuniq , which originates from suc11reg . Existence E. m m SucMap N holds exactly on N e. ran SucMap , cf. elrng .

Note that dom SucMap =V (see dmsucmap ), so the equivalent definition dfpre uses ( iota m m e. Pred ( SucMap , V , N ) ) . (Contributed by Peter Mazsa, 27-Jan-2026)

	Ref	Expression
Assertion	df-pre	Could not format assertion : No typesetting found for |- pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cN	$$classN$$
1	0	cpre	Could not format pre N : No typesetting found for class pre N with typecode class
2		vm	$$setvarm$$
3	2	cv	$$setvarm$$
4		csucmap	Could not format SucMap : No typesetting found for class SucMap with typecode class
5	4	cdm	Could not format dom SucMap : No typesetting found for class dom SucMap with typecode class
6	5 4 0	cpred	Could not format Pred ( SucMap , dom SucMap , N ) : No typesetting found for class Pred ( SucMap , dom SucMap , N ) with typecode class
7	3 6	wcel	Could not format m e. Pred ( SucMap , dom SucMap , N ) : No typesetting found for wff m e. Pred ( SucMap , dom SucMap , N ) with typecode wff
8	7 2	cio	Could not format ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) : No typesetting found for class ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) with typecode class
9	1 8	wceq	Could not format pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) : No typesetting found for wff pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) with typecode wff