Definition df-pre 39184

Description: Define the term-level successor-predecessor. It is the unique 𝑚 with suc 𝑚 = 𝑁 when such an 𝑚 exists; otherwise pre 𝑁 is the arbitrary default chosen by ℩. See its alternate definitions dfpre 39185, dfpre2 39186, dfpre3 39187 and dfpre4 39189.

Our definition is a special case of the widely recognised general 𝑅 -predecessor class df-pred 6306 (the class of all elements 𝑚 of 𝐴 such that 𝑚𝑅𝑁, dfpred3g 6318, cf. also df-bnj14 35145) 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 39171 in place of 𝑅, so that 𝑚 SucMap 𝑁, cf. sucmapleftuniq 39199, which originates from suc11reg 9595. Existence ∃𝑚𝑚 SucMap 𝑁 holds exactly on 𝑁 ∈ ran SucMap, cf. elrng 5883.

Note that dom SucMap = V (see dmsucmap 39177), so the equivalent definition dfpre 39185 uses (℩𝑚𝑚 ∈ Pred( SucMap , V, 𝑁)). (Contributed by Peter Mazsa, 27-Jan-2026.)

Assertion

Ref	Expression
df-pre	⊢ pre 𝑁 = (℩𝑚𝑚 ∈ Pred( SucMap , dom SucMap , 𝑁))

Distinct variable group:   𝑚,𝑁

Detailed syntax breakdown of Definition df-pre

Step	Hyp	Ref	Expression
1		cN	. . 3 class 𝑁
2	1	cpre 38889	. 2 class pre 𝑁
3		vm	. . . . 5 setvar 𝑚
4	3	cv 1569	. . . 4 class 𝑚
5		csucmap 38887	. . . . . 6 class SucMap
6	5	cdm 5663	. . . . 5 class dom SucMap
7	6, 5, 1	cpred 6305	. . . 4 class Pred( SucMap , dom SucMap , 𝑁)
8	4, 7	wcel 2146	. . 3 wff 𝑚 ∈ Pred( SucMap , dom SucMap , 𝑁)
9	8, 3	cio 6494	. 2 class (℩𝑚𝑚 ∈ Pred( SucMap , dom SucMap , 𝑁))
10	2, 9	wceq 1570	1 wff pre 𝑁 = (℩𝑚𝑚 ∈ Pred( SucMap , dom SucMap , 𝑁))

This definition is used by:  dfpre  39185  dfpre4  39189  preex  39201