Definition df-adjliftmap 38570

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 38571.

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 38577 and dfsucmap3 38576) are exactly the successor map 𝑚 ↦ suc 𝑚 (cf. dfsucmap4 38578), 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 7359). However, ∪ and ⋉ are introduced in set.mm as class constructors (e.g. df-un 3904), 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 3904, and

BlockLiftMap directly using the existing ⋉ constructor dfxrn2 38509,

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 42435,

or the equilibrium condition "AdjLiftFix" , in place of {⟨𝑟, 𝑎⟩ ∣ (dom ((𝑅 ∪ ^◡ E ) ↾ 𝐴) / ((𝑅 ∪ ^◡ E ) ↾ 𝐴)) = 𝑎} (cf. its analog df-blockliftfix 38594 and dfblockliftfix2 38836). 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 38572) 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 38315	. 2 class (𝑅 AdjLiftMap 𝐴)
4		vm	. . 3 setvar 𝑚
5		cep 5521	. . . . . . 7 class E
6	5	ccnv 5621	. . . . . 6 class ◡ E
7	2, 6	cun 3897	. . . . 5 class (𝑅 ∪ ◡ E )
8	7, 1	cres 5624	. . . 4 class ((𝑅 ∪ ◡ E ) ↾ 𝐴)
9	8	cdm 5622	. . 3 class dom ((𝑅 ∪ ◡ E ) ↾ 𝐴)
10	4	cv 1540	. . . 4 class 𝑚
11	10, 8	cec 8631	. . 3 class [𝑚]((𝑅 ∪ ◡ E ) ↾ 𝐴)
12	4, 9, 11	cmpt 5177	. 2 class (𝑚 ∈ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) ↦ [𝑚]((𝑅 ∪ ◡ E ) ↾ 𝐴))
13	3, 12	wceq 1541	1 wff (𝑅 AdjLiftMap 𝐴) = (𝑚 ∈ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) ↦ [𝑚]((𝑅 ∪ ◡ E ) ↾ 𝐴))

This definition is referenced by:  dfadjliftmap2  38571  blockadjliftmap  38572  dfsucmap3  38576  dfsucmap2  38577