Definition df-qmap 39123

Description: Define the quotient map (coset map), see also dfqmap2 39124 and dfqmap3 39125. QMap 𝑅 is the "send a generator / domain element to its 𝑅 -coset" map: it maps each 𝑥 ∈ dom 𝑅 to the block [𝑥]𝑅. Makes the quotient operation / structurally explicit as the range of a canonical map (see dfqs2 8699, rnqmap 39131). This is crucial for

(i) modular "two-layer" characterizations (map layer + carrier layer) such as dfdisjs6 39619 / dfdisjs7 39620,

(ii) transport of properties between a relation and its induced quotient-carrier (e.g. "elements are blocks" via rnqmap 39131), and

(iii) expressing stability/invariance constraints as ordinary conditions on a graph (e.g. ran QMap 𝑟 ∈ ElDisjs, QMap 𝑟 ∈ Disjs). (Contributed by Peter Mazsa, 12-Feb-2026.)

Assertion

Ref	Expression
df-qmap	⊢ QMap 𝑅 = (𝑥 ∈ dom 𝑅 ↦ [𝑥]𝑅)

Distinct variable group:   𝑥,𝑅

Detailed syntax breakdown of Definition df-qmap

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	cqmap 38852	. 2 class QMap 𝑅
3		vx	. . 3 setvar 𝑥
4	1	cdm 5660	. . 3 class dom 𝑅
5	3	cv 1568	. . . 4 class 𝑥
6	5, 1	cec 8690	. . 3 class [𝑥]𝑅
7	3, 4, 6	cmpt 5191	. 2 class (𝑥 ∈ dom 𝑅 ↦ [𝑥]𝑅)
8	2, 7	wceq 1569	1 wff QMap 𝑅 = (𝑥 ∈ dom 𝑅 ↦ [𝑥]𝑅)

This definition is used by:  dfqmap2  39124  dfqmap3  39125  qmapex  39128  relqmap  39129  dmqmap  39130  rnqmap  39131  dfadjliftmap  39133  dfblockliftmap  39137  disjqmap2  39503