Definition df-qmap

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

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

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

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	cqmap	⊢ QMap 𝑅
2		vx	⊢ 𝑥
3	0	cdm	⊢ dom 𝑅
4	2	cv	⊢ 𝑥
5	4 0	cec	⊢ [ 𝑥 ] 𝑅
6	2 3 5	cmpt	⊢ ( 𝑥 ∈ dom 𝑅 ↦ [ 𝑥 ] 𝑅 )
7	1 6	wceq	⊢ QMap 𝑅 = ( 𝑥 ∈ dom 𝑅 ↦ [ 𝑥 ] 𝑅 )