P. 390 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38901-39000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dmcnvepres 38901	Domain of the restricted converse epsilon relation. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom (◡ E ↾ 𝐴) = (𝐴 ∖ {∅})
Theorem	dmuncnvepres 38902	Domain of the union with the converse epsilon, restricted. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) = (𝐴 ∩ (dom 𝑅 ∪ (V ∖ {∅})))
Theorem	dmxrnuncnvepres 38903	Domain of the combined relation of two special relations, see blockadjliftmap 38969. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom (((𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴) = (𝐴 ∖ {∅})
Theorem	ecun 38904	The union coset of 𝐴. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ∪ 𝑆) = ([𝐴]𝑅 ∪ [𝐴]𝑆))
Theorem	ecunres 38905	The restricted union coset of 𝐵. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐵 ∈ 𝑉 → [𝐵]((𝑅 ∪ 𝑆) ↾ 𝐴) = ([𝐵](𝑅 ↾ 𝐴) ∪ [𝐵](𝑆 ↾ 𝐴)))
Theorem	ecuncnvepres 38906	The restricted union with converse epsilon relation coset of 𝐵. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐵 ∈ 𝐴 → [𝐵]((𝑅 ∪ ◡ E ) ↾ 𝐴) = (𝐵 ∪ [𝐵]𝑅))
Theorem	xrneq1 38907	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ (𝐴 = 𝐵 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶))
Theorem	xrneq1i 38908	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶)
Theorem	xrneq1d 38909	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶))
Theorem	xrneq2 38910	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ (𝐴 = 𝐵 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵))
Theorem	xrneq2i 38911	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)
Theorem	xrneq2d 38912	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵))
Theorem	xrneq12 38913	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	xrneq12i 38914	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)
Theorem	xrneq12d 38915	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 18-Dec-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	elecxrn 38916*	Elementhood in the (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴](𝑅 ⋉ 𝑆) ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)))
Theorem	ecxrn 38917*	The (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = {⟨𝑦, 𝑧⟩ ∣ (𝐴𝑅𝑦 ∧ 𝐴𝑆𝑧)})
Theorem	relecxrn 38918	The (𝑅 ⋉ 𝑆)-coset of a set is a relation. (Contributed by Peter Mazsa, 15-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → Rel [𝐴](𝑅 ⋉ 𝑆))
Theorem	ecxrn2 38919	The (𝑅 ⋉ 𝑆)-coset of a set is the Cartesian product of its 𝑅-coset and 𝑆-coset. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = ([𝐴]𝑅 × [𝐴]𝑆))
Theorem	ecxrncnvep 38920*	The (𝑅 ⋉ ◡ E )-coset of a set. (Contributed by Peter Mazsa, 22-May-2021.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ ◡ E ) = {⟨𝑦, 𝑧⟩ ∣ (𝑧 ∈ 𝐴 ∧ 𝐴𝑅𝑦)})
Theorem	ecxrncnvep2 38921	The (𝑅 ⋉ ◡ E )-coset of a set is the Cartesian product of its 𝑅-coset and the set. (Contributed by Peter Mazsa, 25-Jan-2026.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ ◡ E ) = ([𝐴]𝑅 × 𝐴))
Theorem	disjressuc2 38922*	Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
Theorem	disjecxrn 38923	Two ways of saying that (𝑅 ⋉ 𝑆)-cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020.) (Revised by Peter Mazsa, 21-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = ∅ ↔ (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ ([𝐴]𝑆 ∩ [𝐵]𝑆) = ∅)))
Theorem	disjecxrncnvep 38924	Two ways of saying that cosets are disjoint, special case of disjecxrn 38923. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 25-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ ◡ E ) ∩ [𝐵](𝑅 ⋉ ◡ E )) = ∅ ↔ ((𝐴 ∩ 𝐵) = ∅ ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)))
Theorem	disjsuc2 38925*	Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ ◡ E ) ∩ [𝑣](𝑅 ⋉ ◡ E )) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ ◡ E ) ∩ [𝑣](𝑅 ⋉ ◡ E )) = ∅) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
Theorem	xrninxp 38926*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = ◡{⟨⟨𝑦, 𝑧⟩, 𝑢⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)⟨𝑦, 𝑧⟩))}
Theorem	xrninxp2 38927*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {⟨𝑢, 𝑥⟩ ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))}
Theorem	xrninxpex 38928	Sufficient condition for the intersection of a range Cartesian product with a Cartesian product to be a set. (Contributed by Peter Mazsa, 12-Apr-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) ∈ V)
Theorem	inxpxrn 38929	Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶)))
Theorem	br1cnvxrn2 38930*	The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐴◡(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	elec1cnvxrn2 38931*	Elementhood in the converse range Cartesian product coset of 𝐴. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡(𝑅 ⋉ 𝑆) ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	rnxrn 38932*	Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020.)
⊢ ran (𝑅 ⋉ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrnres 38933*	Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021.)
⊢ ran (𝑅 ⋉ (𝑆 ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrncnvepres 38934*	Range of a range Cartesian product with a restriction of the converse epsilon relation. (Contributed by Peter Mazsa, 6-Dec-2021.)
⊢ ran (𝑅 ⋉ (◡ E ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ 𝑢 ∧ 𝑢𝑅𝑥)}
Theorem	rnxrnidres 38935*	Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.)
⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)}
Theorem	xrnres 38936	Two ways to express restriction of range Cartesian product, see also xrnres2 38937, xrnres3 38938. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆)
Theorem	xrnres2 38937	Two ways to express restriction of range Cartesian product, see also xrnres 38936, xrnres3 38938. (Contributed by Peter Mazsa, 6-Sep-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres3 38938	Two ways to express restriction of range Cartesian product, see also xrnres 38936, xrnres2 38937. (Contributed by Peter Mazsa, 28-Mar-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres4 38939	Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴))))
Theorem	xrnresex 38940	Sufficient condition for a restricted range Cartesian product to be a set. (Contributed by Peter Mazsa, 16-Dec-2020.) (Revised by Peter Mazsa, 7-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ (𝑆 ↾ 𝐴) ∈ 𝑋) → (𝑅 ⋉ (𝑆 ↾ 𝐴)) ∈ V)
Theorem	xrnidresex 38941	Sufficient condition for a range Cartesian product with restricted identity to be a set. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ ( I ↾ 𝐴)) ∈ V)
Theorem	xrncnvepresex 38942	Sufficient condition for a range Cartesian product with restricted converse epsilon to be a set. (Contributed by Peter Mazsa, 16-Dec-2020.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V)
Theorem	dmxrncnvepres 38943	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (dom (𝑅 ↾ 𝐴) ∖ {∅})
Theorem	dmxrncnvepres2 38944	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (𝐴 ∩ (dom 𝑅 ∖ {∅}))
Theorem	eldmxrncnvepres 38945	Element of the domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eldmxrncnvepres2 38946*	Element of the domain of the range product with restricted converse epsilon relation. This identifies the domain of the pet 39476 span (𝑅 ⋉ (◡ E ↾ 𝐴)): a 𝐵 belongs to the domain of the span exactly when 𝐵 is in 𝐴 and has at least one 𝑥 ∈ 𝐵 and 𝑦 with 𝐵𝑅𝑦. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝐵 ∧ ∃𝑦 𝐵𝑅𝑦)))
Theorem	eceldmqsxrncnvepres 38947	An (𝑅 ⋉ (◡ E ↾ 𝐴))-coset in its domain quotient. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋) → ([𝐵](𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eceldmqsxrncnvepres2 38948*	An (𝑅 ⋉ (◡ E ↾ 𝐴))-coset in its domain quotient. In the pet 39476 span (𝑅 ⋉ (◡ E ↾ 𝐴)), a block [ B ] lies in the domain quotient exactly when its representative 𝐵 belongs to 𝐴 and actually fires at least one arrow (has some 𝑥 ∈ 𝐵 and some 𝑦 with 𝐵𝑅𝑦). (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋) → ([𝐵](𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝐵 ∧ ∃𝑦 𝐵𝑅𝑦)))
Theorem	brin2 38949	Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐵⟩))
Theorem	brin3 38950	Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021.) (Avoid depending on this detail.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ 𝑆)𝐵 ↔ 𝐴(𝑅 ⋉ 𝑆){{𝐵}}))
21.26.4  Relations
Definition	df-rels 38951	Define the relations class. Proper class relations (like I, see reli 5804) are not elements of it. The element of this class and the relation predicate are the same when 𝑅 is a set (see elrelsrel 38953). The class of relations is a great tool we can use when we define classes of different relations as nullary class constants as required by the 2. point in our Guidelines https://us.metamath.org/mpeuni/mathbox.html 38953. When we want to define a specific class of relations as a nullary class constant, the appropriate method is the following: 1. We define the specific nullary class constant for general sets (see e.g. df-refs 39101), then 2. we get the required class of relations by the intersection of the class of general sets above with the class of relations df-rels 38951 (see df-refrels 39102 and the resulting dfrefrels2 39104 and dfrefrels3 39105). 3. Finally, in order to be able to work with proper classes (like iprc 7896) as well, we define the predicate of the relation (see df-refrel 39103) so that it is true for the relevant proper classes (see refrelid 39113), and that the element of the class of the required relations (e.g. elrefrels3 39110) and this predicate are the same in case of sets (see elrefrelsrel 39111). (Contributed by Peter Mazsa, 13-Jun-2018.)
⊢ Rels = 𝒫 (V × V)
Theorem	elrels2 38952	The element of the relations class (df-rels 38951) and the relation predicate (df-rel 5659) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V)))
Theorem	elrelsrel 38953	The element of the relations class (df-rels 38951) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅))
Theorem	elrelsrelim 38954	The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ (𝑅 ∈ Rels → Rel 𝑅)
Theorem	elrels5 38955	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅))
Theorem	elrels6 38956	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅))
21.26.5  Quotient map (coset map)
Definition	df-qmap 38957*	Define the quotient map (coset map), see also dfqmap2 38958 and dfqmap3 38959. 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 8689, rnqmap 38965). This is crucial for (i) modular "two-layer" characterizations (map layer + carrier layer) such as dfdisjs6 39453 / dfdisjs7 39454, (ii) transport of properties between a relation and its induced quotient-carrier (e.g. "elements are blocks" via rnqmap 38965), 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.)
⊢ QMap 𝑅 = (𝑥 ∈ dom 𝑅 ↦ [𝑥]𝑅)
Theorem	dfqmap2 38958*	Alternate definition of the quotient map: QMap in image-of-singleton form. (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ QMap 𝑅 = (𝑥 ∈ dom 𝑅 ↦ (𝑅 “ {𝑥}))
Theorem	dfqmap3 38959*	Alternate definition of the quotient map: QMap as ordered-pair class abstraction. Gives the raw set-builder characterization for extensional proofs, Rel proofs (relqmap 38963), and composition/intersection manipulations. (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ QMap 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ dom 𝑅 ∧ 𝑦 = [𝑥]𝑅)}
Theorem	ecqmap 38960	QMap fibers are singletons of blocks. Makes QMap behave like a "block constructor function" on dom 𝑅. (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ (𝐴 ∈ dom 𝑅 → [𝐴] QMap 𝑅 = {[𝐴]𝑅})
Theorem	ecqmap2 38961	Fiber of QMap equals singleton quotient: a conceptual bridge between "map fibers" and quotients. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ (𝐴 ∈ dom 𝑅 → [𝐴] QMap 𝑅 = ({𝐴} / 𝑅))
Theorem	qmapex 38962	Quotient map exists if 𝑅 exists. Type-safety: ensures QMap is a set under the standard "relation sethood" hypothesis. (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → QMap 𝑅 ∈ V)
Theorem	relqmap 38963	Quotient map is a relation. Guarantees that QMap can be composed, restricted, and used in other relation infrastructure (e.g., membership in Disjs, Rels-based typing). (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ Rel QMap 𝑅
Theorem	dmqmap 38964	QMap preserves the domain. Confirms that QMap is defined exactly on the points where cosets [𝑥]𝑅 make sense (those in dom 𝑅). (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → dom QMap 𝑅 = dom 𝑅)
Theorem	rnqmap 38965	The range of the quotient map is the quotient carrier. It lets us replace quotient-carrier reasoning by map/range reasoning (and conversely) via df-qmap 38957 and dfqs2 8689. (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ ran QMap 𝑅 = (dom 𝑅 / 𝑅)
21.26.6  Lifts, shifts, successor, and predecessor
Definition	df-adjliftmap 38966	Define the adjoined lift map. Given a relation 𝑅 and a carrier/set 𝐴, we form the adjoined relation (𝑅 ∪ ◡ E ) (i.e., "follow 𝑅 or follow elements"), restricted to 𝐴, and map each domain element 𝑚 to its coset [𝑚] under that restricted adjoined relation, see its expanded version dfadjliftmap 38967. Thus, for 𝑚 in its domain, we have (𝑚 ∪ [𝑚]𝑅), see dfadjliftmap2 38968. Its key special case is successor: for 𝑅 = I and 𝐴 = dom I, or 𝐴 = V, the adjoined relation is ( I ∪ ◡ E ), and the coset becomes [𝑚]( I ∪ ◡ E ) = (𝑚 ∪ {𝑚}). So ( I AdjLiftMap dom I ) or ( I AdjLiftMap V) (see dfsucmap2 38975 and dfsucmap3 38974) are exactly the successor map 𝑚 ↦ suc 𝑚 (cf. dfsucmap4 38976), which is a prerequisite for accepting the adjoining lift as the right generalization of successor. A maximally generic form would be "( R F LiftMap A )" defined as (𝑚 ∈ dom ((𝑅𝐹◡ E ) ↾ 𝐴) ↦ [𝑚]((𝑅𝐹◡ E ) ↾ 𝐴)) where 𝐹 is an object-level binary operator on relations (used via df-ov 7403). However, ∪ and ⋉ are introduced in set.mm as class constructors (e.g. df-un 3912), not as an object-level binary function symbol 𝐹 that can be passed as a parameter. To make the generic 𝐹-pattern literally usable, we would need to reify union and ⋉ as function-objects, which is additional infrastructure. To avoid introducing operator-as-function objects solely to support 𝐹, we define: AdjLiftMap directly using df-un 3912, and BlockLiftMap directly using the existing ⋉ constructor dfxrn2 38896, so we treat any "generic 𝐹-LiftMap" as optional future generalization, not a dependency. We prefer to avoid defining too many concepts. For this reason, we will not introduce a named "adjoining relation", a named carrier "adjoining lift" "( R AdjLift A )", in place of ran (𝑅 AdjLiftMap 𝐴), which is (dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) / ((𝑅 ∪ ◡ E ) ↾ 𝐴)), cf. dfqs2 8689, or the equilibrium condition "AdjLiftFix" , in place of {⟨𝑟, 𝑎⟩ ∣ (dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) / ((𝑅 ∪ ◡ E ) ↾ 𝐴)) = 𝑎} (cf. its analog df-blockliftfix 38992). These are definable by simple expansions and/or domain-quotient theorems when needed. A "two-stage" construction is obtained by first forming the block relation (𝑅 ⋉ ◡ E ) and then adjoining elements as "BlockAdj" . Combined, it uses the relation ((𝑅 ⋉ ◡ E ) ∪ ◡ E ), which for 𝑚 in its domain (𝐴 ∖ {∅}) gives (𝑚 ∪ [𝑚](𝑅 ⋉ ◡ E )), yielding "BlockAdjLiftMap" (cf. blockadjliftmap 38969) and "BlockAdjLiftFix". We only introduce these if a downstream theorem actually requires them. (Contributed by Peter Mazsa, 24-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)
⊢ (𝑅 AdjLiftMap 𝐴) = QMap ((𝑅 ∪ ◡ E ) ↾ 𝐴)
Theorem	dfadjliftmap 38967*	Alternate (expanded) definition of the adjoined lift map. (Contributed by Peter Mazsa, 28-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)
⊢ (𝑅 AdjLiftMap 𝐴) = (𝑚 ∈ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) ↦ [𝑚]((𝑅 ∪ ◡ E ) ↾ 𝐴))
Theorem	dfadjliftmap2 38968*	Alternate definition of the adjoined lift map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝑅 AdjLiftMap 𝐴) = (𝑚 ∈ (𝐴 ∩ (dom 𝑅 ∪ (V ∖ {∅}))) ↦ (𝑚 ∪ [𝑚]𝑅))
Theorem	blockadjliftmap 38969*	A "two-stage" construction is obtained by first forming the block relation (𝑅 ⋉ ◡ E ) and then adjoining elements as "BlockAdj". Combined, it uses the relation ((𝑅 ⋉ ◡ E ) ∪ ◡ E ). (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ ((𝑅 ⋉ ◡ E ) AdjLiftMap 𝐴) = {⟨𝑚, 𝑛⟩ ∣ (𝑚 ∈ (𝐴 ∖ {∅}) ∧ 𝑛 = (𝑚 ∪ ([𝑚]𝑅 × 𝑚)))}
Definition	df-blockliftmap 38970	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 38937). Then map each domain element 𝑚 to its coset [𝑚] under that restricted block relation. For 𝑚 in the domain, which requires (𝑚 ∈ 𝐴 ∧ 𝑚 ≠ ∅ ∧ [𝑚]𝑅 ≠ ∅) (cf. eldmxrncnvepres 38945), the fiber has the product form [𝑚](𝑅 ⋉ ◡ E ) = ([𝑚]𝑅 × 𝑚), so the block relation lifts a block 𝑚 to the rectangular grid "external labels × internal members", see dfblockliftmap2 38972. Contrast: while the adjoined lift, via (𝑅 ∪ ◡ E ), attaches neighbors and members in a single relation (see dfadjliftmap2 38968), 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 38966. For the equilibrium condition, see df-blockliftfix 38992. (Contributed by Peter Mazsa, 24-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)
⊢ (𝑅 BlockLiftMap 𝐴) = QMap (𝑅 ⋉ (◡ E ↾ 𝐴))
Theorem	dfblockliftmap 38971*	Alternate definition of the block lift map. (Contributed by Peter Mazsa, 29-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)
⊢ (𝑅 BlockLiftMap 𝐴) = (𝑚 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↦ [𝑚](𝑅 ⋉ (◡ E ↾ 𝐴)))
Theorem	dfblockliftmap2 38972*	Alternate definition of the block lift map. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ (𝑅 BlockLiftMap 𝐴) = (𝑚 ∈ (𝐴 ∩ (dom 𝑅 ∖ {∅})) ↦ ([𝑚]𝑅 × 𝑚))
Definition	df-sucmap 38973*	Define the successor map, directly as the graph of the successor operation, using only elementary set theory (ordered-pair class abstraction). This avoids committing to any particular construction of the successor function/class from other operators (e.g. a union/composition presentation), while remaining provably equivalent to those presentations (cf. dfsucmap2 38975 and dfsucmap3 38974 vs. df-succf 36233 and dfsuccf2 36304). For maximum mappy shape, see dfsucmap4 38976. We also treat the successor relation as the default shift relation for grading/tower arguments (cf. df-shiftstable 38993). Because it is used pervasively in shift-lift infrastructure, we adopt the short name SucMap rather than the fully systematic "SucAdjLiftMap". You may also define the predecessor relation as the converse graph "PreMap" as ◡ SucMap, which reverses successor edges ( cf. cnvopab 6128) and sends each successor to its (unique) predecessor when it exists. (Contributed by Peter Mazsa, 25-Jan-2026.)
⊢ SucMap = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
Theorem	dfsucmap3 38974	Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ SucMap = ( I AdjLiftMap V)
Theorem	dfsucmap2 38975	Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ SucMap = ( I AdjLiftMap dom I )
Theorem	dfsucmap4 38976	Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ SucMap = (𝑚 ∈ V ↦ suc 𝑚)
Theorem	brsucmap 38977	Binary relation form of the successor map, general version. (Contributed by Peter Mazsa, 6-Jan-2026.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝑀 SucMap 𝑁 ↔ suc 𝑀 = 𝑁))
Theorem	relsucmap 38978	The successor map is a relation. (Contributed by Peter Mazsa, 7-Jan-2026.)
⊢ Rel SucMap
Theorem	dmsucmap 38979	The domain of the successor map is the universe. (Contributed by Peter Mazsa, 7-Jan-2026.)
⊢ dom SucMap = V
Definition	df-succl 38980	Define Suc as the class of all successors, i.e. the range of the successor map: 𝑛 ∈ Suc iff ∃𝑚suc 𝑚 = 𝑛 (see dfsuccl2 38981). By injectivity of suc (suc11reg 9576), every 𝑛 ∈ Suc has at most one predecessor, which is exactly what pre 𝑛 (df-pre 38986) names. Cf. dfsuccl3 38984 and dfsuccl4 38985. (Contributed by Peter Mazsa, 25-Jan-2026.)
⊢ Suc = ran SucMap
Theorem	dfsuccl2 38981*	Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ Suc = {𝑛 ∣ ∃𝑚 suc 𝑚 = 𝑛}
Theorem	mopre 38982*	There is at most one predecessor of 𝑁. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ ∃*𝑚 suc 𝑚 = 𝑁
Theorem	exeupre2 38983*	Whenever a predecessor exists, it exists alone. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (∃𝑚 suc 𝑚 = 𝑁 ↔ ∃!𝑚 suc 𝑚 = 𝑁)
Theorem	dfsuccl3 38984*	Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 30-Jan-2026.)
⊢ Suc = {𝑛 ∣ ∃!𝑚 suc 𝑚 = 𝑛}
Theorem	dfsuccl4 38985*	Alternate definition that incorporates the most desirable properties of the successor class. (Contributed by Peter Mazsa, 30-Jan-2026.)
⊢ Suc = {𝑛 ∣ ∃!𝑚 ∈ 𝑛 (𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛)}
Definition	df-pre 38986*	Define the term-level successor-predecessor. It is the unique 𝑚 with suc 𝑚 = 𝑁 when such an 𝑚 exists; otherwise pre 𝑁 is the arbitrary default chosen by ℩. See its alternate definitions dfpre 38987, dfpre2 38988, dfpre3 38989 and dfpre4 38991. Our definition is a special case of the widely recognised general 𝑅 -predecessor class df-pred 6292 (the class of all elements 𝑚 of 𝐴 such that 𝑚𝑅𝑁, dfpred3g 6304, cf. also df-bnj14 34995) in several respects. Its most abstract property as a specialisation is that it has a unique existing value by default. This is in contrast to the general version. The uniqueness (conditional on existence) is implied by the property of this specific instance of the general case involving the successor map df-sucmap 38973 in place of 𝑅, so that 𝑚 SucMap 𝑁, cf. sucmapleftuniq 39001, which originates from suc11reg 9576. Existence ∃𝑚𝑚 SucMap 𝑁 holds exactly on 𝑁 ∈ ran SucMap, cf. elrng 5872. Note that dom SucMap = V (see dmsucmap 38979), so the equivalent definition dfpre 38987 uses (℩𝑚𝑚 ∈ Pred( SucMap , V, 𝑁)). (Contributed by Peter Mazsa, 27-Jan-2026.)
⊢ pre 𝑁 = (℩𝑚𝑚 ∈ Pred( SucMap , dom SucMap , 𝑁))
Theorem	dfpre 38987*	Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 27-Jan-2026.)
⊢ pre 𝑁 = (℩𝑚𝑚 ∈ Pred( SucMap , V, 𝑁))
Theorem	dfpre2 38988*	Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → pre 𝑁 = (℩𝑚𝑚 SucMap 𝑁))
Theorem	dfpre3 38989*	Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → pre 𝑁 = (℩𝑚 suc 𝑚 = 𝑁))
Theorem	dfpred4 38990	Alternate definition of the predecessor class when 𝑁 is a set. (Contributed by Peter Mazsa, 26-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑁) = [𝑁]◡(𝑅 ↾ 𝐴))
Theorem	dfpre4 38991*	Alternate definition of the predecessor of the 𝑁 set. The ◡ SucMap is just the "PreMap"; we did not define it because we do not expect to use it extensively in future (cf. the comments of df-sucmap 38973). (Contributed by Peter Mazsa, 26-Jan-2026.)
⊢ (𝑁 ∈ 𝑉 → pre 𝑁 = (℩𝑚𝑚 ∈ [𝑁]◡ SucMap ))
Definition	df-blockliftfix 38992*	Define the equilibrium / fixed-point condition for "block carriers". Start with a candidate block-family 𝑎 (a set whose elements you intend to treat as blocks). Combine it with a relation 𝑟 by forming the block-lift span 𝑇 = (𝑟 ⋉ (◡ E ↾ 𝑎)). For a block 𝑢 ∈ 𝑎, the fiber [𝑢]𝑇 is the set of all outputs produced from "external targets" of 𝑟 together with "internal members" of 𝑢; in other words, 𝑇 is the mechanism that generates new blocks from old ones. Now apply the standard quotient construction (dom 𝑇 / 𝑇). This produces the family of all T-blocks (the cosets [𝑥]𝑇 of witnesses 𝑥 in the domain of 𝑇). In general, this operation can change your carrier: starting from 𝑎, it may generate a different block-family (dom 𝑇 / 𝑇). The equation (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎 says exactly: if you generate blocks from 𝑎 using the lift determined by 𝑟 (cf. df-blockliftmap 38970), you get back the same 𝑎. So 𝑎 is stable under the block-generation operator induced by 𝑟. This is why it is a genuine fixpoint/equilibrium condition: one application of the "make-the-blocks" operator causes no carrier drift, i.e. no hidden refinement/coarsening of what counts as a block. Here, the quotient (dom 𝑇 / 𝑇) is the standard carrier of 𝑇 -blocks; see dfqs2 8689 for the quotient-as-range viewpoint. This is an untyped equilibrium predicate on pairs ⟨𝑟, 𝑎⟩. No hypothesis 𝑟 ∈ Rels is built into the definition, because the fixpoint equation depends only on those ordered pairs ⟨𝑥, 𝑦⟩ that belong to 𝑟 and hence can witness an atomic instance 𝑥𝑟𝑦; extra non-ordered-pair "junk" elements in 𝑟 are ignored automatically by the relational membership predicate. When later work needs 𝑟 to be relation-typed (e.g. to intersect with ( Rels × V)-style typedness modules, or to apply Rels-based infrastructure uniformly), the additional typing constraint 𝑟 ∈ Rels should be imposed locally as a separate conjunct (rather than being baked into this equilibrium module). (Contributed by Peter Mazsa, 25-Jan-2026.) (Revised by Peter Mazsa, 20-Feb-2026.)
⊢ BlockLiftFix = {⟨𝑟, 𝑎⟩ ∣ (dom (𝑟 ⋉ (◡ E ↾ 𝑎)) / (𝑟 ⋉ (◡ E ↾ 𝑎))) = 𝑎}
Definition	df-shiftstable 38993	Define shift-stability, a general "procedure" pattern for "the one-step backward shift/transport of 𝐹 along 𝑆", and then ∩ 𝐹 enforces "and it already holds here". Let 𝐹 be a relation encoding a property that depends on a "level" coordinate (for example, a feasibility condition indexed by a carrier, a grade, or a stage in a construction). Let 𝑆 be a shift relation between levels (for example, the successor map SucMap, or any other grading step). The composed relation (𝑆 ∘ 𝐹) transports 𝐹 one step along the shift: 𝑟(𝑆 ∘ 𝐹)𝑛 means there exists a predecessor level 𝑚 such that 𝑟𝐹𝑚 and 𝑚𝑆𝑛 (e.g., 𝑚 SucMap 𝑛). We do not introduce a separate notation for "Shift" because it is simply the standard relational composition df-co 5661. The intersection ((𝑆 ∘ 𝐹) ∩ 𝐹) is the locally shift-stable fragment of 𝐹: it consists exactly of those points where the property holds at some immediate predecessor that shifts to 𝑛 and also holds at level 𝑛. In other words, it isolates the part of 𝐹 that is already compatible with one-step tower coherence. This definition packages a common construction pattern used throughout the development: "constrain by one-step stability under a chosen shift, then additionally constrain by 𝐹". Iterating the operator (𝑋 ↦ ((𝑆 ∘ 𝑋) ∩ 𝑋) corresponds to multi-step/tower coherence; the one-step definition here is the economical kernel from which such "tower" readings can be developed when needed. (Contributed by Peter Mazsa, 25-Jan-2026.)
⊢ (𝑆 ShiftStable 𝐹) = ((𝑆 ∘ 𝐹) ∩ 𝐹)
Theorem	shiftstableeq2 38994	Equality theorem for shift-stability of two classes. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ (𝐹 = 𝐺 → (𝑆 ShiftStable 𝐹) = (𝑆 ShiftStable 𝐺))
Theorem	suceqsneq 38995	One-to-one relationship between the successor operation and the singleton. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 = suc 𝐵 ↔ {𝐴} = {𝐵}))
Theorem	sucdifsn2 38996	Absorption of union with a singleton by difference. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∪ {𝐴}) ∖ {𝐴}) = 𝐴
Theorem	sucdifsn 38997	The difference between the successor and the singleton of a class is the class. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ (suc 𝐴 ∖ {𝐴}) = 𝐴
Theorem	ressucdifsn2 38998	The difference between restrictions to the successor and the singleton of a class is the restriction to the class, see ressucdifsn 38999. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) = (𝑅 ↾ 𝐴)
Theorem	ressucdifsn 38999	The difference between restrictions to the successor and the singleton of a class is the restriction to the class. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ ((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) = (𝑅 ↾ 𝐴)
Theorem	sucmapsuc 39000	A set is succeeded by its successor. (Contributed by Peter Mazsa, 7-Jan-2026.)
⊢ (𝑀 ∈ 𝑉 → 𝑀 SucMap suc 𝑀)