Definition df-pre 38842

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 38843, dfpre2 38844, dfpre3 38845 and dfpre4 38847.

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

Note that dom SucMap = V (see dmsucmap 38835), so the equivalent definition dfpre 38843 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 38547	. 2 class pre 𝑁
3		vm	. . . . 5 setvar 𝑚
4	3	cv 1546	. . . 4 class 𝑚
5		csucmap 38545	. . . . . 6 class SucMap
6	5	cdm 5618	. . . . 5 class dom SucMap
7	6, 5, 1	cpred 6251	. . . 4 class Pred( SucMap , dom SucMap , 𝑁)
8	4, 7	wcel 2119	. . 3 wff 𝑚 ∈ Pred( SucMap , dom SucMap , 𝑁)
9	8, 3	cio 6439	. 2 class (℩𝑚𝑚 ∈ Pred( SucMap , dom SucMap , 𝑁))
10	2, 9	wceq 1547	1 wff pre 𝑁 = (℩𝑚𝑚 ∈ Pred( SucMap , dom SucMap , 𝑁))

This definition is referenced by:  dfpre  38843  dfpre4  38847  preex  38859