Definition df-adjliftmap 38480

Description: Define the adjoined lift map. Given a relation 𝑅 and a carrier/set 𝐴, we form the adjoined relation (𝑅 ∪ ^◡ E ) (i.e., "follow 𝑅 or follow elements"), restricted to 𝐴, and map each domain element 𝑚 to its coset [𝑚] under that restricted adjoined relation. Thus, for 𝑚 in its domain, we have (𝑚 ∪ [𝑚]𝑅), see dfadjliftmap2 38481.

Its key special case is successor: for 𝑅 = I and 𝐴 = dom I, or 𝐴 = V, the adjoined relation is ( I ∪ ^◡ E ), and the coset becomes [𝑚]( I ∪ ^◡ E ) = (𝑚 ∪ {𝑚}). So ( I AdjLiftMap dom I ) or ( I AdjLiftMap V) (see dfsucmap2 38487 and dfsucmap3 38486) are exactly the successor map 𝑚 ↦ suc 𝑚 (cf. dfsucmap4 38488), which is a prerequisite for accepting the adjoining lift as the right generalization of successor.

A maximally generic form would be "( R F LiftMap A )" defined as (𝑚 ∈ dom ((𝑅𝐹^◡ E ) ↾ 𝐴) ↦ [𝑚]((𝑅𝐹^◡ E ) ↾ 𝐴)) where 𝐹 is an object-level binary operator on relations (used via df-ov 7349). However, ∪ and ⋉ are introduced in set.mm as class constructors (e.g. df-un 3902), not as an object-level binary function symbol 𝐹 that can be passed as a parameter. To make the generic 𝐹-pattern literally usable, we would need to reify union and ⋉ as function-objects, which is additional infrastructure. To avoid introducing operator-as-function objects solely to support 𝐹, we define:

AdjLiftMap directly using df-un 3902, and

BlockLiftMap directly using the existing ⋉ constructor dfxrn2 38419,

so we treat any "generic 𝐹-LiftMap" as optional future generalization, not a dependency.

We prefer to avoid defining too many concepts. For this reason, we will not introduce

a named "adjoining relation",

a named carrier "adjoining lift" "( R AdjLift A )", in place of ran (𝑅 AdjLiftMap 𝐴), which is (dom ((𝑅 ∪ ^◡ E ) ↾ 𝐴) / ((𝑅 ∪ ^◡ E ) ↾ 𝐴)), cf. dfqs2 42340,

or the equilibrium condition "AdjLiftFix" , in place of {⟨𝑟, 𝑎⟩ ∣ (dom ((𝑅 ∪ ^◡ E ) ↾ 𝐴) / ((𝑅 ∪ ^◡ E ) ↾ 𝐴)) = 𝑎} (cf. its analog df-blockliftfix 38504 and dfblockliftfix2 38746). These are definable by simple expansions and/or domain-quotient theorems when needed.

A "two-stage" construction is obtained by first forming the block relation (𝑅 ⋉ ^◡ E ) and then adjoining elements as "BlockAdj" . Combined, it uses the relation ((𝑅 ⋉ ^◡ E ) ∪ ^◡ E ), which for 𝑚 in its domain (𝐴 ∖ {∅}) gives (𝑚 ∪ [𝑚](𝑅 ⋉ ^◡ E )), yielding "BlockAdjLiftMap" (cf. blockadjliftmap 38482) and "BlockAdjLiftFix". We only introduce these if a downstream theorem actually requires them. (Contributed by Peter Mazsa, 24-Jan-2026.)

Assertion

Ref	Expression
df-adjliftmap	⊢ (𝑅 AdjLiftMap 𝐴) = (𝑚 ∈ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) ↦ [𝑚]((𝑅 ∪ ◡ E ) ↾ 𝐴))

Distinct variable groups:   𝐴,𝑚   𝑅,𝑚

Detailed syntax breakdown of Definition df-adjliftmap

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	cadjliftmap 38225	. 2 class (𝑅 AdjLiftMap 𝐴)
4		vm	. . 3 setvar 𝑚
5		cep 5513	. . . . . . 7 class E
6	5	ccnv 5613	. . . . . 6 class ◡ E
7	2, 6	cun 3895	. . . . 5 class (𝑅 ∪ ◡ E )
8	7, 1	cres 5616	. . . 4 class ((𝑅 ∪ ◡ E ) ↾ 𝐴)
9	8	cdm 5614	. . 3 class dom ((𝑅 ∪ ◡ E ) ↾ 𝐴)
10	4	cv 1540	. . . 4 class 𝑚
11	10, 8	cec 8620	. . 3 class [𝑚]((𝑅 ∪ ◡ E ) ↾ 𝐴)
12	4, 9, 11	cmpt 5170	. 2 class (𝑚 ∈ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) ↦ [𝑚]((𝑅 ∪ ◡ E ) ↾ 𝐴))
13	3, 12	wceq 1541	1 wff (𝑅 AdjLiftMap 𝐴) = (𝑚 ∈ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) ↦ [𝑚]((𝑅 ∪ ◡ E ) ↾ 𝐴))

This definition is referenced by:  dfadjliftmap2  38481  blockadjliftmap  38482  dfsucmap3  38486  dfsucmap2  38487