Definition df-blockliftmap

Description: Define the block lift map. Given a relation R and a carrier/set A , we form the block relation ( R |X.`'E ) (i.e., "follow both R and element"), restricted to A (or, equivalently, "follow both R and elements-of-A", cf. xrnres2 ). Then map each domain element m to its coset [ m ] under that restricted block relation.

For m in the domain, which requires ( m e. A /\ m =/= (/) /\ [ m ] R =/= (/) ) (cf. eldmxrncnvepres ), the fiber has the product form [ m ] ( R |X. ``' E ) = ( [ m ] R X. m ) , so the block relation lifts a block m to the rectangular grid "external labels X. ` internal members", see dfblockliftmap2 . Contrast: while the adjoined lift, via ( R u.`' _E ) ` , attaches neighbors and members in a single relation (see dfadjliftmap2 ), the block lift labels each internal member by each external neighbor.

For the general case and a two-stage construction (first block lift, then adjoin membership), see the comments to df-adjliftmap . For the equilibrium condition, see df-blockliftfix and dfblockliftfix2 . (Contributed by Peter Mazsa, 24-Jan-2026)

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

Detailed syntax breakdown

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