P. 391 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39001-39100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	brabidga 39001	The law of concretion for a binary relation. Special case of brabga 5520. Usage of this theorem is discouraged because it depends on ax-13 2404, see brabidgaw 39000 for a weaker version that does not require it. (Contributed by Peter Mazsa, 24-Nov-2018.) (New usage is discouraged.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝑥𝑅𝑦 ↔ 𝜑)
Theorem	inxp2 39002*	Intersection with a Cartesian product. (Contributed by Peter Mazsa, 18-Jul-2019.)
⊢ (𝑅 ∩ (𝐴 × 𝐵)) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥𝑅𝑦)}
Theorem	opabf 39003	A class abstraction of a collection of ordered pairs with a negated wff is the empty set. (Contributed by Peter Mazsa, 21-Oct-2019.) (Proof shortened by Thierry Arnoux, 18-Feb-2022.)
⊢ ¬ 𝜑    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = ∅
Theorem	ec0 39004	The empty-coset of a class is the empty set. (Contributed by Peter Mazsa, 19-May-2019.)
⊢ [𝐴]∅ = ∅
Theorem	brcnvin 39005	Intersection with a converse, binary relation. (Contributed by Peter Mazsa, 24-Mar-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ ◡𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑆𝐴)))
Theorem	ssdmral 39006*	Subclass of a domain. (Contributed by Peter Mazsa, 15-Sep-2018.)
⊢ (𝐴 ⊆ dom 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝑅𝑦)
21.26.3  Range Cartesian product
Definition	df-xrn 39007	Define the range Cartesian product of two classes. Definition from [Holmes] p. 40. Membership in this class is characterized by xrnss3v 39008 and brxrn 39010. This is Scott Fenton's df-txp 36322 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 36322. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⋉ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵))
Theorem	xrnss3v 39008	A range Cartesian product is a subset of the class of ordered triples. This is Scott Fenton's txpss3v 36346 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 36346. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⋉ 𝐵) ⊆ (V × (V × V))
Theorem	xrnrel 39009	A range Cartesian product is a relation. This is Scott Fenton's txprel 36347 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 36347. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel (𝐴 ⋉ 𝐵)
Theorem	brxrn 39010	Characterize a ternary relation over a range Cartesian product. Together with xrnss3v 39008, this characterizes elementhood in a range cross. (Contributed by Peter Mazsa, 27-Jun-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐶⟩ ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐶)))
Theorem	brxrn2 39011*	A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)))
Theorem	dfxrn2 39012*	Alternate definition of the range Cartesian product. (Contributed by Peter Mazsa, 20-Feb-2022.)
⊢ (𝑅 ⋉ 𝑆) = ◡{⟨⟨𝑥, 𝑦⟩, 𝑢⟩ ∣ (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	brxrncnvep 39013	The range product with converse epsilon relation. (Contributed by Peter Mazsa, 22-Jun-2020.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ ◡ E )⟨𝐵, 𝐶⟩ ↔ (𝐶 ∈ 𝐴 ∧ 𝐴𝑅𝐵)))
Theorem	dmxrn 39014	Domain of the range product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ dom (𝑅 ⋉ 𝑆) = (dom 𝑅 ∩ dom 𝑆)
Theorem	dmcnvep 39015	Domain of converse epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.) (Revised by Peter Mazsa, 23-Nov-2025.)
⊢ dom ◡ E = (V ∖ {∅})
Theorem	dmxrncnvep 39016	Domain of the range product with converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ dom (𝑅 ⋉ ◡ E ) = (dom 𝑅 ∖ {∅})
Theorem	dmcnvepres 39017	Domain of the restricted converse epsilon relation. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom (◡ E ↾ 𝐴) = (𝐴 ∖ {∅})
Theorem	dmuncnvepres 39018	Domain of the union with the converse epsilon, restricted. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) = (𝐴 ∩ (dom 𝑅 ∪ (V ∖ {∅})))
Theorem	dmxrnuncnvepres 39019	Domain of the combined relation of two special relations, see blockadjliftmap 39085. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom (((𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴) = (𝐴 ∖ {∅})
Theorem	ecun 39020	The union coset of 𝐴. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ∪ 𝑆) = ([𝐴]𝑅 ∪ [𝐴]𝑆))
Theorem	ecunres 39021	The restricted union coset of 𝐵. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐵 ∈ 𝑉 → [𝐵]((𝑅 ∪ 𝑆) ↾ 𝐴) = ([𝐵](𝑅 ↾ 𝐴) ∪ [𝐵](𝑆 ↾ 𝐴)))
Theorem	ecuncnvepres 39022	The restricted union with converse epsilon relation coset of 𝐵. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐵 ∈ 𝐴 → [𝐵]((𝑅 ∪ ◡ E ) ↾ 𝐴) = (𝐵 ∪ [𝐵]𝑅))
Theorem	xrneq1 39023	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ (𝐴 = 𝐵 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶))
Theorem	xrneq1i 39024	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶)
Theorem	xrneq1d 39025	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶))
Theorem	xrneq2 39026	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ (𝐴 = 𝐵 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵))
Theorem	xrneq2i 39027	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)
Theorem	xrneq2d 39028	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵))
Theorem	xrneq12 39029	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	xrneq12i 39030	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)
Theorem	xrneq12d 39031	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 18-Dec-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	elecxrn 39032*	Elementhood in the (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴](𝑅 ⋉ 𝑆) ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)))
Theorem	ecxrn 39033*	The (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = {⟨𝑦, 𝑧⟩ ∣ (𝐴𝑅𝑦 ∧ 𝐴𝑆𝑧)})
Theorem	relecxrn 39034	The (𝑅 ⋉ 𝑆)-coset of a set is a relation. (Contributed by Peter Mazsa, 15-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → Rel [𝐴](𝑅 ⋉ 𝑆))
Theorem	ecxrn2 39035	The (𝑅 ⋉ 𝑆)-coset of a set is the Cartesian product of its 𝑅-coset and 𝑆-coset. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = ([𝐴]𝑅 × [𝐴]𝑆))
Theorem	ecxrncnvep 39036*	The (𝑅 ⋉ ◡ E )-coset of a set. (Contributed by Peter Mazsa, 22-May-2021.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ ◡ E ) = {⟨𝑦, 𝑧⟩ ∣ (𝑧 ∈ 𝐴 ∧ 𝐴𝑅𝑦)})
Theorem	ecxrncnvep2 39037	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 39038*	Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
Theorem	disjecxrn 39039	Two ways of saying that (𝑅 ⋉ 𝑆)-cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020.) (Revised by Peter Mazsa, 21-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = ∅ ↔ (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ ([𝐴]𝑆 ∩ [𝐵]𝑆) = ∅)))
Theorem	disjecxrncnvep 39040	Two ways of saying that cosets are disjoint, special case of disjecxrn 39039. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 25-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ ◡ E ) ∩ [𝐵](𝑅 ⋉ ◡ E )) = ∅ ↔ ((𝐴 ∩ 𝐵) = ∅ ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)))
Theorem	disjsuc2 39041*	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 39042*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = ◡{⟨⟨𝑦, 𝑧⟩, 𝑢⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)⟨𝑦, 𝑧⟩))}
Theorem	xrninxp2 39043*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {⟨𝑢, 𝑥⟩ ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))}
Theorem	xrninxpex 39044	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 39045	Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶)))
Theorem	br1cnvxrn2 39046*	The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐴◡(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	elec1cnvxrn2 39047*	Elementhood in the converse range Cartesian product coset of 𝐴. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡(𝑅 ⋉ 𝑆) ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	rnxrn 39048*	Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020.)
⊢ ran (𝑅 ⋉ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrnres 39049*	Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021.)
⊢ ran (𝑅 ⋉ (𝑆 ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrncnvepres 39050*	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 39051*	Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.)
⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)}
Theorem	xrnres 39052	Two ways to express restriction of range Cartesian product, see also xrnres2 39053, xrnres3 39054. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆)
Theorem	xrnres2 39053	Two ways to express restriction of range Cartesian product, see also xrnres 39052, xrnres3 39054. (Contributed by Peter Mazsa, 6-Sep-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres3 39054	Two ways to express restriction of range Cartesian product, see also xrnres 39052, xrnres2 39053. (Contributed by Peter Mazsa, 28-Mar-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres4 39055	Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴))))
Theorem	xrnresex 39056	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 39057	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 39058	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 39059	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (dom (𝑅 ↾ 𝐴) ∖ {∅})
Theorem	dmxrncnvepres2 39060	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (𝐴 ∩ (dom 𝑅 ∖ {∅}))
Theorem	eldmxrncnvepres 39061	Element of the domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eldmxrncnvepres2 39062*	Element of the domain of the range product with restricted converse epsilon relation. This identifies the domain of the pet 39592 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 39063	An (𝑅 ⋉ (◡ E ↾ 𝐴))-coset in its domain quotient. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋) → ([𝐵](𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eceldmqsxrncnvepres2 39064*	An (𝑅 ⋉ (◡ E ↾ 𝐴))-coset in its domain quotient. In the pet 39592 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 39065	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 39066	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 39067	Define the relations class. Proper class relations (like I, see reli 5815) are not elements of it. The element of this class and the relation predicate are the same when 𝑅 is a set (see elrelsrel 39069). 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 39069. 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 39217), 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 39067 (see df-refrels 39218 and the resulting dfrefrels2 39220 and dfrefrels3 39221). 3. Finally, in order to be able to work with proper classes (like iprc 7909) as well, we define the predicate of the relation (see df-refrel 39219) so that it is true for the relevant proper classes (see refrelid 39229), and that the element of the class of the required relations (e.g. elrefrels3 39226) and this predicate are the same in case of sets (see elrefrelsrel 39227). (Contributed by Peter Mazsa, 13-Jun-2018.)
⊢ Rels = 𝒫 (V × V)
Theorem	elrels2 39068	The element of the relations class (df-rels 39067) and the relation predicate (df-rel 5670) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V)))
Theorem	elrelsrel 39069	The element of the relations class (df-rels 39067) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅))
Theorem	elrelsrelim 39070	The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ (𝑅 ∈ Rels → Rel 𝑅)
Theorem	elrels5 39071	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅))
Theorem	elrels6 39072	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 39073*	Define the quotient map (coset map), see also dfqmap2 39074 and dfqmap3 39075. 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 8702, rnqmap 39081). This is crucial for (i) modular "two-layer" characterizations (map layer + carrier layer) such as dfdisjs6 39569 / dfdisjs7 39570, (ii) transport of properties between a relation and its induced quotient-carrier (e.g. "elements are blocks" via rnqmap 39081), 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 39074*	Alternate definition of the quotient map: QMap in image-of-singleton form. (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ QMap 𝑅 = (𝑥 ∈ dom 𝑅 ↦ (𝑅 “ {𝑥}))
Theorem	dfqmap3 39075*	Alternate definition of the quotient map: QMap as ordered-pair class abstraction. Gives the raw set-builder characterization for extensional proofs, Rel proofs (relqmap 39079), and composition/intersection manipulations. (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ QMap 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ dom 𝑅 ∧ 𝑦 = [𝑥]𝑅)}
Theorem	ecqmap 39076	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 39077	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 39078	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 39079	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 39080	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 39081	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 39073 and dfqs2 8702. (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ ran QMap 𝑅 = (dom 𝑅 / 𝑅)
21.26.6  Lifts, shifts, successor, and predecessor
Definition	df-adjliftmap 39082	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 39083. Thus, for 𝑚 in its domain, we have (𝑚 ∪ [𝑚]𝑅), see dfadjliftmap2 39084. 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 39091 and dfsucmap3 39090) are exactly the successor map 𝑚 ↦ suc 𝑚 (cf. dfsucmap4 39092), 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 7415). However, ∪ and ⋉ are introduced in set.mm as class constructors (e.g. df-un 3911), 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 3911, and BlockLiftMap directly using the existing ⋉ constructor dfxrn2 39012, 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 8702, or the equilibrium condition "AdjLiftFix" , in place of {⟨𝑟, 𝑎⟩ ∣ (dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) / ((𝑅 ∪ ◡ E ) ↾ 𝐴)) = 𝑎} (cf. its analog df-blockliftfix 39108). 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 39085) 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 39083*	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 39084*	Alternate definition of the adjoined lift map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝑅 AdjLiftMap 𝐴) = (𝑚 ∈ (𝐴 ∩ (dom 𝑅 ∪ (V ∖ {∅}))) ↦ (𝑚 ∪ [𝑚]𝑅))
Theorem	blockadjliftmap 39085*	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 39086	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 39053). Then map each domain element 𝑚 to its coset [𝑚] under that restricted block relation. For 𝑚 in the domain, which requires (𝑚 ∈ 𝐴 ∧ 𝑚 ≠ ∅ ∧ [𝑚]𝑅 ≠ ∅) (cf. eldmxrncnvepres 39061), the fiber has the product form [𝑚](𝑅 ⋉ ◡ E ) = ([𝑚]𝑅 × 𝑚), so the block relation lifts a block 𝑚 to the rectangular grid "external labels × internal members", see dfblockliftmap2 39088. Contrast: while the adjoined lift, via (𝑅 ∪ ◡ E ), attaches neighbors and members in a single relation (see dfadjliftmap2 39084), 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 39082. For the equilibrium condition, see df-blockliftfix 39108. (Contributed by Peter Mazsa, 24-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)
⊢ (𝑅 BlockLiftMap 𝐴) = QMap (𝑅 ⋉ (◡ E ↾ 𝐴))
Theorem	dfblockliftmap 39087*	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 39088*	Alternate definition of the block lift map. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ (𝑅 BlockLiftMap 𝐴) = (𝑚 ∈ (𝐴 ∩ (dom 𝑅 ∖ {∅})) ↦ ([𝑚]𝑅 × 𝑚))
Definition	df-sucmap 39089*	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 39091 and dfsucmap3 39090 vs. df-succf 36340 and dfsuccf2 36411). For maximum mappy shape, see dfsucmap4 39092. We also treat the successor relation as the default shift relation for grading/tower arguments (cf. df-shiftstable 39109). 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 6139) and sends each successor to its (unique) predecessor when it exists. (Contributed by Peter Mazsa, 25-Jan-2026.)
⊢ SucMap = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
Theorem	dfsucmap3 39090	Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ SucMap = ( I AdjLiftMap V)
Theorem	dfsucmap2 39091	Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ SucMap = ( I AdjLiftMap dom I )
Theorem	dfsucmap4 39092	Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ SucMap = (𝑚 ∈ V ↦ suc 𝑚)
Theorem	brsucmap 39093	Binary relation form of the successor map, general version. (Contributed by Peter Mazsa, 6-Jan-2026.)
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊) → (𝑀 SucMap 𝑁 ↔ suc 𝑀 = 𝑁))
Theorem	relsucmap 39094	The successor map is a relation. (Contributed by Peter Mazsa, 7-Jan-2026.)
⊢ Rel SucMap
Theorem	dmsucmap 39095	The domain of the successor map is the universe. (Contributed by Peter Mazsa, 7-Jan-2026.)
⊢ dom SucMap = V
Definition	df-succl 39096	Define Suc as the class of all successors, i.e. the range of the successor map: 𝑛 ∈ Suc iff ∃𝑚suc 𝑚 = 𝑛 (see dfsuccl2 39097). By injectivity of suc (suc11reg 9589), every 𝑛 ∈ Suc has at most one predecessor, which is exactly what pre 𝑛 (df-pre 39102) names. Cf. dfsuccl3 39100 and dfsuccl4 39101. (Contributed by Peter Mazsa, 25-Jan-2026.)
⊢ Suc = ran SucMap
Theorem	dfsuccl2 39097*	Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ Suc = {𝑛 ∣ ∃𝑚 suc 𝑚 = 𝑛}
Theorem	mopre 39098*	There is at most one predecessor of 𝑁. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ ∃*𝑚 suc 𝑚 = 𝑁
Theorem	exeupre2 39099*	Whenever a predecessor exists, it exists alone. (Contributed by Peter Mazsa, 12-Jan-2026.)
⊢ (∃𝑚 suc 𝑚 = 𝑁 ↔ ∃!𝑚 suc 𝑚 = 𝑁)
Theorem	dfsuccl3 39100*	Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 30-Jan-2026.)
⊢ Suc = {𝑛 ∣ ∃!𝑚 suc 𝑚 = 𝑛}