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 . (Contributed by Peter Mazsa, 24-Jan-2026) (Revised by Peter Mazsa, 22-Feb-2026)

	Ref	Expression
Assertion	df-blockliftmap	|- ( R BlockLiftMap A ) = QMap ( R |X. ( `' _E |` A ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1		cA	|- A
2	1 0	cblockliftmap	|- ( R BlockLiftMap A )
3		cep	|- _E
4	3	ccnv	|- `' _E
5	4 1	cres	|- ( `' _E |` A )
6	0 5	cxrn	|- ( R |X. ( `' _E |` A ) )
7	6	cqmap	|- QMap ( R |X. ( `' _E |` A ) )
8	2 7	wceq	|- ( R BlockLiftMap A ) = QMap ( R |X. ( `' _E |` A ) )