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	|- pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cN	|- N
1	0	cpre	|- pre N
2		vm	|- m
3	2	cv	|- m
4		csucmap	|- SucMap
5	4	cdm	|- dom SucMap
6	5 4 0	cpred	|- Pred ( SucMap , dom SucMap , N )
7	3 6	wcel	|- m e. Pred ( SucMap , dom SucMap , N )
8	7 2	cio	|- ( iota m m e. Pred ( SucMap , dom SucMap , N ) )
9	1 8	wceq	|- pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) )