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 | |- ( R AdjLiftMap A ) = ( m e. dom ( ( R u. `' _E ) |` A ) |-> [ m ] ( ( R u. `' _E ) |` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cR | |- R |
|
| 1 | cA | |- A |
|
| 2 | 1 0 | cadjliftmap | |- ( R AdjLiftMap A ) |
| 3 | vm | |- m |
|
| 4 | cep | |- _E |
|
| 5 | 4 | ccnv | |- `' _E |
| 6 | 0 5 | cun | |- ( R u. `' _E ) |
| 7 | 6 1 | cres | |- ( ( R u. `' _E ) |` A ) |
| 8 | 7 | cdm | |- dom ( ( R u. `' _E ) |` A ) |
| 9 | 3 | cv | |- m |
| 10 | 9 7 | cec | |- [ m ] ( ( R u. `' _E ) |` A ) |
| 11 | 3 8 10 | cmpt | |- ( m e. dom ( ( R u. `' _E ) |` A ) |-> [ m ] ( ( R u. `' _E ) |` A ) ) |
| 12 | 2 11 | wceq | |- ( R AdjLiftMap A ) = ( m e. dom ( ( R u. `' _E ) |` A ) |-> [ m ] ( ( R u. `' _E ) |` A ) ) |