Definition df-blockliftmap 38483

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 38460). Then map each domain element 𝑚 to its coset [𝑚] under that restricted block relation.

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

Assertion

Ref	Expression
df-blockliftmap	⊢ (𝑅 BlockLiftMap 𝐴) = (𝑚 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↦ [𝑚](𝑅 ⋉ (◡ E ↾ 𝐴)))

Distinct variable groups:   𝐴,𝑚   𝑅,𝑚

Detailed syntax breakdown of Definition df-blockliftmap

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	cblockliftmap 38226	. 2 class (𝑅 BlockLiftMap 𝐴)
4		vm	. . 3 setvar 𝑚
5		cep 5513	. . . . . . 7 class E
6	5	ccnv 5613	. . . . . 6 class ◡ E
7	6, 1	cres 5616	. . . . 5 class (◡ E ↾ 𝐴)
8	2, 7	cxrn 38224	. . . 4 class (𝑅 ⋉ (◡ E ↾ 𝐴))
9	8	cdm 5614	. . 3 class dom (𝑅 ⋉ (◡ E ↾ 𝐴))
10	4	cv 1540	. . . 4 class 𝑚
11	10, 8	cec 8620	. . 3 class [𝑚](𝑅 ⋉ (◡ E ↾ 𝐴))
12	4, 9, 11	cmpt 5170	. 2 class (𝑚 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↦ [𝑚](𝑅 ⋉ (◡ E ↾ 𝐴)))
13	3, 12	wceq 1541	1 wff (𝑅 BlockLiftMap 𝐴) = (𝑚 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↦ [𝑚](𝑅 ⋉ (◡ E ↾ 𝐴)))

This definition is referenced by:  dfblockliftmap2  38484