Definition df-adjliftmap

Description: Define the adjoined lift map. Given a relation R and a carrier/set A , we form the adjoined relation ( R u.`'E ) (i.e., "follow R or follow elements"), restricted to A , and map each domain element m to its coset [ m ] under that restricted adjoined relation. Thus, for m in its domain, we have ( m u. [ m ] R ) , see dfadjliftmap2 .

Its key special case is successor: for R = I and A = domI , or A = V , the adjoined relation is (I u. ``' E ) , and the coset becomes [ m ] (I u. ``' E ) = ( m u. { m } ) . So (I AdjLiftMap dom I ) or (I AdjLiftMap V ) (see dfsucmap2 and dfsucmap3 ) are exactly the successor map m |-> suc m (cf. dfsucmap4 ), 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 ( m e. dom ( ( R F ``'E ) |`A ) |-> [ m ] ( ( R F`' E ) |`A ) ) where F is an object-level binary operator on relations (used via df-ov ). However, u. and |X. are introduced in set.mm as class constructors (e.g. df-un ), not as an object-level binary function symbol F that can be passed as a parameter. To make the generic F -pattern literally usable, we would need to reify union and |X. as function-objects, which is additional infrastructure. To avoid introducing operator-as-function objects solely to support F , we define:

AdjLiftMap directly using df-un , and

BlockLiftMap directly using the existing |X. constructor dfxrn2 ,

so we treat any "generic F -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 ( R AdjLiftMap A ) , which is ( dom ( ( R u.`'E ) |`A ) /. ( ( R u.`' E ) |`A ) ) , cf. dfqs2 ,

or the equilibrium condition "AdjLiftFix" , in place of { <. r , a >. | ( dom ( ( R u.`'E ) |`A ) /. ( ( R u.`' E ) |`A ) ) = a } (cf. its analog df-blockliftfix and dfblockliftfix2 ). 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 ( R |X.`'E ) and then adjoining elements as "BlockAdj" . Combined, it uses the relation ( ( R |X. ``' E ) u. ``'E ) , which for m in its domain ( A \ { (/) } ) gives ( m u. [ m ] ( R |X. ``' E ) ) ` , yielding "BlockAdjLiftMap" (cf. blockadjliftmap ) and "BlockAdjLiftFix". We only introduce these if a downstream theorem actually requires them. (Contributed by Peter Mazsa, 24-Jan-2026)

	Ref	Expression
Assertion	df-adjliftmap	Could not format assertion : No typesetting found for |- ( R AdjLiftMap A ) = ( m e. dom ( ( R u. `' _E ) |` A ) |-> [ m ] ( ( R u. `' _E ) |` A ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	cadjliftmap	Could not format ( R AdjLiftMap A ) : No typesetting found for class ( R AdjLiftMap A ) with typecode class
3		vm	$$setvarm$$
4		cep	$$class\mathrm{E}$$
5	4	ccnv	$$class{\mathrm{E}}^{-1}$$
6	0 5	cun	$$class\left(R\cup {\mathrm{E}}^{-1}\right)$$
7	6 1	cres	$$class\left({\left(R\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)$$
8	7	cdm	$$class\mathrm{dom}\left({\left(R\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)$$
9	3	cv	$$setvarm$$
10	9 7	cec	$$class\left[m\right]\left({\left(R\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)$$
11	3 8 10	cmpt	$$class\left(m\in \mathrm{dom}\left({\left(R\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)⟼\left[m\right]\left({\left(R\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\right)$$
12	2 11	wceq	Could not format ( R AdjLiftMap A ) = ( m e. dom ( ( R u. `' _E ) |` A ) |-> [ m ] ( ( R u. `' _E ) |` A ) ) : No typesetting found for wff ( R AdjLiftMap A ) = ( m e. dom ( ( R u. `' _E ) |` A ) |-> [ m ] ( ( R u. `' _E ) |` A ) ) with typecode wff