Definition df-adjliftmap 38793

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, see its expanded version dfadjliftmap 38794. Thus, for 𝑚 in its domain, we have (𝑚 ∪ [𝑚]𝑅), see dfadjliftmap2 38795.

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 38802 and dfsucmap3 38801) are exactly the successor map 𝑚 ↦ suc 𝑚 (cf. dfsucmap4 38803), 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 7364). However, ∪ and ⋉ are introduced in set.mm as class constructors (e.g. df-un 3895), 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 3895, and

BlockLiftMap directly using the existing ⋉ constructor dfxrn2 38723,

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

or the equilibrium condition "AdjLiftFix" , in place of {⟨𝑟, 𝑎⟩ ∣ (dom ((𝑅 ∪ ^◡ E ) ↾ 𝐴) / ((𝑅 ∪ ^◡ E ) ↾ 𝐴)) = 𝑎} (cf. its analog df-blockliftfix 38819). 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 38796) and "BlockAdjLiftFix". We only introduce these if a downstream theorem actually requires them. (Contributed by Peter Mazsa, 24-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)

Assertion

Ref	Expression
df-adjliftmap	⊢ (𝑅 AdjLiftMap 𝐴) = QMap ((𝑅 ∪ ◡ E ) ↾ 𝐴)

Detailed syntax breakdown of Definition df-adjliftmap

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	cadjliftmap 38514	. 2 class (𝑅 AdjLiftMap 𝐴)
4		cep 5524	. . . . . 6 class E
5	4	ccnv 5624	. . . . 5 class ◡ E
6	2, 5	cun 3888	. . . 4 class (𝑅 ∪ ◡ E )
7	6, 1	cres 5627	. . 3 class ((𝑅 ∪ ◡ E ) ↾ 𝐴)
8	7	cqmap 38513	. 2 class QMap ((𝑅 ∪ ◡ E ) ↾ 𝐴)
9	3, 8	wceq 1542	1 wff (𝑅 AdjLiftMap 𝐴) = QMap ((𝑅 ∪ ◡ E ) ↾ 𝐴)

This definition is referenced by:  dfadjliftmap  38794