Definition df-blockliftmap 39391

Description: Define the block lift map. Given a relation 𝑅 and a carrier/set 𝐴, we form the block relation (𝑅 ⋉ ^◡ E ) (i.e., "follow both 𝑅 and element"), restricted to 𝐴 (or, equivalently, "follow both 𝑅 and elements-of-A", cf. xrnres2 39358). Then map each domain element 𝑚 to its coset [𝑚] under that restricted block relation.

For 𝑚 in the domain, which requires (𝑚 ∈ 𝐴 ∧ 𝑚 ≠ ∅ ∧ [𝑚]𝑅 ≠ ∅) (cf. eldmxrncnvepres 39366), the fiber has the product form [𝑚](𝑅 ⋉ ^◡ E ) = ([𝑚]𝑅 × 𝑚), so the block relation lifts a block 𝑚 to the rectangular grid "external labels × internal members", see dfblockliftmap2 39393. Contrast: while the adjoined lift, via (𝑅 ∪ ^◡ E ), attaches neighbors and members in a single relation (see dfadjliftmap2 39389), 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 39387. For the equilibrium condition, see df-blockliftfix 39413. (Contributed by Peter Mazsa, 24-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)

Assertion

Ref	Expression
df-blockliftmap	⊢ (𝑅 BlockLiftMap 𝐴) = QMap (𝑅 ⋉ (◡ E ↾ 𝐴))

Detailed syntax breakdown of Definition df-blockliftmap

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	cblockliftmap 39109	. 2 class (𝑅 BlockLiftMap 𝐴)
4		cep 5550	. . . . . 6 class E
5	4	ccnv 5650	. . . . 5 class ◡ E
6	5, 1	cres 5653	. . . 4 class (◡ E ↾ 𝐴)
7	2, 6	cxrn 39106	. . 3 class (𝑅 ⋉ (◡ E ↾ 𝐴))
8	7	cqmap 39107	. 2 class QMap (𝑅 ⋉ (◡ E ↾ 𝐴))
9	3, 8	wceq 1570	1 wff (𝑅 BlockLiftMap 𝐴) = QMap (𝑅 ⋉ (◡ E ↾ 𝐴))

This definition is used by:  dfblockliftmap  39392