P. 387 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38601-38700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	inecmo2 38601*	Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 29-May-2018.) (Revised by Peter Mazsa, 2-Sep-2021.)
⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅) ↔ (∀𝑥∃*𝑢 ∈ 𝐴 𝑢𝑅𝑥 ∧ Rel 𝑅))
Theorem	ineccnvmo 38602*	Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 2-Sep-2021.)
⊢ (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦 = 𝑧 ∨ ([𝑦]◡𝐹 ∩ [𝑧]◡𝐹) = ∅) ↔ ∀𝑥∃*𝑦 ∈ 𝐵 𝑥𝐹𝑦)
Theorem	alrmomorn 38603	Equivalence of an "at most one" and an "at most one" restricted to the range inside a universal quantification. (Contributed by Peter Mazsa, 3-Sep-2021.)
⊢ (∀𝑥∃*𝑦 ∈ ran 𝑅 𝑥𝑅𝑦 ↔ ∀𝑥∃*𝑦 𝑥𝑅𝑦)
Theorem	alrmomodm 38604*	Equivalence of an "at most one" and an "at most one" restricted to the domain inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (Rel 𝑅 → (∀𝑥∃*𝑢 ∈ dom 𝑅 𝑢𝑅𝑥 ↔ ∀𝑥∃*𝑢 𝑢𝑅𝑥))
Theorem	ralmo 38605*	"At most one" can be restricted to the range. (Contributed by Peter Mazsa, 2-Feb-2026.)
⊢ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ↔ ∀𝑥 ∈ ran 𝑅∃*𝑢 𝑢𝑅𝑥)
Theorem	ralrnmo 38606*	On the range, "at most one" becomes "exactly one". (Contributed by Peter Mazsa, 27-Sep-2018.) (Revised by Peter Mazsa, 2-Feb-2026.)
⊢ (∀𝑥 ∈ ran 𝑅∃*𝑢 𝑢𝑅𝑥 ↔ ∀𝑥 ∈ ran 𝑅∃!𝑢 𝑢𝑅𝑥)
Theorem	dmqsex 38607	Sethood of the domain quotient under sethood of 𝑅. (Contributed by Peter Mazsa, 2-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 / 𝑅) ∈ V)
Theorem	raldmqsmo 38608*	On the quotient carrier, "at most one" and "exactly one" coincide for coset witnesses. (Contributed by Peter Mazsa, 6-Feb-2026.)
⊢ (∀𝑢 ∈ (dom 𝑅 / 𝑅)∃*𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅 ↔ ∀𝑢 ∈ (dom 𝑅 / 𝑅)∃!𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅)
Theorem	ralrmo3 38609*	Pull a restricted universal quantifier into the body (for ∃*). (Contributed by Peter Mazsa, 9-May-2019.)
⊢ (∀𝑦 ∈ 𝐵 ∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑))
Theorem	raldmqseu 38610*	Equivalence between "exactly one" on the quotient carrier and "at most one" globally. Provides a type-safe way to talk about unique representatives either as ∃! on the intended carrier or as a global ∃* statement. (Contributed by Peter Mazsa, 6-Feb-2026.)
⊢ (𝑅 ∈ 𝑉 → (∀𝑢 ∈ (dom 𝑅 / 𝑅)∃!𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅 ↔ ∀𝑢∃*𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅))
Theorem	rsp3 38611*	From a restricted universal statement over 𝐴, specialize to an arbitrary element 𝑦 ∈ 𝐴, cf. rsp 3226. (Contributed by Peter Mazsa, 9-Feb-2026.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑦 ∈ 𝐴 → 𝜓))
Theorem	rsp3eq 38612*	From a restricted universal statement over 𝐴, specialize to an arbitrary element class, cf. rsp3 38611. (Contributed by Peter Mazsa, 9-Feb-2026.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ((𝑦 = 𝐵 ∧ 𝐵 ∈ 𝐴) → 𝜓))
Theorem	ineccnvmo2 38613*	Equivalence of a double universal quantification restricted to the range and an "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 4-Sep-2021.)
⊢ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ↔ ∀𝑢∃*𝑥 𝑢𝐹𝑥)
Theorem	inecmo3 38614*	Equivalence of a double universal quantification restricted to the domain and an "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ((∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅) ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅))
Theorem	moeu2 38615	Uniqueness is equivalent to non-existence or unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by Peter Mazsa, 19-Nov-2024.)
⊢ (∃*𝑥𝜑 ↔ (¬ ∃𝑥𝜑 ∨ ∃!𝑥𝜑))
Theorem	mopickr 38616	"At most one" picks a variable value, eliminating an existential quantifier. The proof begins with references *2.21 (pm2.21 123) and *14.26 (eupickbi 2637) from [WhiteheadRussell] p. 104 and p. 183. (Contributed by Peter Mazsa, 18-Nov-2024.) (Proof modification is discouraged.)
⊢ ((∃*𝑥𝜓 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜓 → 𝜑))
Theorem	moantr 38617	Sufficient condition for transitivity of conjunctions inside existential quantifiers. (Contributed by Peter Mazsa, 2-Oct-2018.)
⊢ (∃*𝑥𝜓 → ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃𝑥(𝜓 ∧ 𝜒)) → ∃𝑥(𝜑 ∧ 𝜒)))
Theorem	brabidgaw 38618*	The law of concretion for a binary relation. Special case of brabga 5490. Version of brabidga 38619 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Peter Mazsa, 24-Nov-2018.) (Revised by GG, 2-Apr-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝑥𝑅𝑦 ↔ 𝜑)
Theorem	brabidga 38619	The law of concretion for a binary relation. Special case of brabga 5490. Usage of this theorem is discouraged because it depends on ax-13 2377, see brabidgaw 38618 for a weaker version that does not require it. (Contributed by Peter Mazsa, 24-Nov-2018.) (New usage is discouraged.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝑥𝑅𝑦 ↔ 𝜑)
Theorem	inxp2 38620*	Intersection with a Cartesian product. (Contributed by Peter Mazsa, 18-Jul-2019.)
⊢ (𝑅 ∩ (𝐴 × 𝐵)) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥𝑅𝑦)}
Theorem	opabf 38621	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 38622	The empty-coset of a class is the empty set. (Contributed by Peter Mazsa, 19-May-2019.)
⊢ [𝐴]∅ = ∅
Theorem	brcnvin 38623	Intersection with a converse, binary relation. (Contributed by Peter Mazsa, 24-Mar-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝑅 ∩ ◡𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑆𝐴)))
Theorem	ssdmral 38624*	Subclass of a domain. (Contributed by Peter Mazsa, 15-Sep-2018.)
⊢ (𝐴 ⊆ dom 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝑅𝑦)
21.26.3  Range Cartesian product
Definition	df-xrn 38625	Define the range Cartesian product of two classes. Definition from [Holmes] p. 40. Membership in this class is characterized by xrnss3v 38626 and brxrn 38628. This is Scott Fenton's df-txp 36065 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 36065. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⋉ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵))
Theorem	xrnss3v 38626	A range Cartesian product is a subset of the class of ordered triples. This is Scott Fenton's txpss3v 36089 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 36089. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⋉ 𝐵) ⊆ (V × (V × V))
Theorem	xrnrel 38627	A range Cartesian product is a relation. This is Scott Fenton's txprel 36090 with a different symbol, see https://github.com/metamath/set.mm/issues/2469 36090. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel (𝐴 ⋉ 𝐵)
Theorem	brxrn 38628	Characterize a ternary relation over a range Cartesian product. Together with xrnss3v 38626, this characterizes elementhood in a range cross. (Contributed by Peter Mazsa, 27-Jun-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐶⟩ ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐶)))
Theorem	brxrn2 38629*	A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)))
Theorem	dfxrn2 38630*	Alternate definition of the range Cartesian product. (Contributed by Peter Mazsa, 20-Feb-2022.)
⊢ (𝑅 ⋉ 𝑆) = ◡{⟨⟨𝑥, 𝑦⟩, 𝑢⟩ ∣ (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	brxrncnvep 38631	The range product with converse epsilon relation. (Contributed by Peter Mazsa, 22-Jun-2020.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ ◡ E )⟨𝐵, 𝐶⟩ ↔ (𝐶 ∈ 𝐴 ∧ 𝐴𝑅𝐵)))
Theorem	dmxrn 38632	Domain of the range product. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ dom (𝑅 ⋉ 𝑆) = (dom 𝑅 ∩ dom 𝑆)
Theorem	dmcnvep 38633	Domain of converse epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.) (Revised by Peter Mazsa, 23-Nov-2025.)
⊢ dom ◡ E = (V ∖ {∅})
Theorem	dmxrncnvep 38634	Domain of the range product with converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ dom (𝑅 ⋉ ◡ E ) = (dom 𝑅 ∖ {∅})
Theorem	dmcnvepres 38635	Domain of the restricted converse epsilon relation. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom (◡ E ↾ 𝐴) = (𝐴 ∖ {∅})
Theorem	dmuncnvepres 38636	Domain of the union with the converse epsilon, restricted. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) = (𝐴 ∩ (dom 𝑅 ∪ (V ∖ {∅})))
Theorem	dmxrnuncnvepres 38637	Domain of the combined relation of two special relations, see blockadjliftmap 38703. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ dom (((𝑅 ⋉ ◡ E ) ∪ ◡ E ) ↾ 𝐴) = (𝐴 ∖ {∅})
Theorem	ecun 38638	The union coset of 𝐴. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ∪ 𝑆) = ([𝐴]𝑅 ∪ [𝐴]𝑆))
Theorem	ecunres 38639	The restricted union coset of 𝐵. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐵 ∈ 𝑉 → [𝐵]((𝑅 ∪ 𝑆) ↾ 𝐴) = ([𝐵](𝑅 ↾ 𝐴) ∪ [𝐵](𝑆 ↾ 𝐴)))
Theorem	ecuncnvepres 38640	The restricted union with converse epsilon relation coset of 𝐵. (Contributed by Peter Mazsa, 28-Jan-2026.)
⊢ (𝐵 ∈ 𝐴 → [𝐵]((𝑅 ∪ ◡ E ) ↾ 𝐴) = (𝐵 ∪ [𝐵]𝑅))
Theorem	xrneq1 38641	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ (𝐴 = 𝐵 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶))
Theorem	xrneq1i 38642	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶)
Theorem	xrneq1d 38643	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐶))
Theorem	xrneq2 38644	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ (𝐴 = 𝐵 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵))
Theorem	xrneq2i 38645	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵)
Theorem	xrneq2d 38646	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 7-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 ⋉ 𝐴) = (𝐶 ⋉ 𝐵))
Theorem	xrneq12 38647	Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	xrneq12i 38648	Equality theorem for the range Cartesian product, inference form. (Contributed by Peter Mazsa, 16-Dec-2020.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷)
Theorem	xrneq12d 38649	Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 18-Dec-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 ⋉ 𝐶) = (𝐵 ⋉ 𝐷))
Theorem	elecxrn 38650*	Elementhood in the (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴](𝑅 ⋉ 𝑆) ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)))
Theorem	ecxrn 38651*	The (𝑅 ⋉ 𝑆)-coset of 𝐴. (Contributed by Peter Mazsa, 18-Apr-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = {⟨𝑦, 𝑧⟩ ∣ (𝐴𝑅𝑦 ∧ 𝐴𝑆𝑧)})
Theorem	relecxrn 38652	The (𝑅 ⋉ 𝑆)-coset of a set is a relation. (Contributed by Peter Mazsa, 15-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → Rel [𝐴](𝑅 ⋉ 𝑆))
Theorem	ecxrn2 38653	The (𝑅 ⋉ 𝑆)-coset of a set is the Cartesian product of its 𝑅-coset and 𝑆-coset. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ 𝑆) = ([𝐴]𝑅 × [𝐴]𝑆))
Theorem	ecxrncnvep 38654*	The (𝑅 ⋉ ◡ E )-coset of a set. (Contributed by Peter Mazsa, 22-May-2021.)
⊢ (𝐴 ∈ 𝑉 → [𝐴](𝑅 ⋉ ◡ E ) = {⟨𝑦, 𝑧⟩ ∣ (𝑧 ∈ 𝐴 ∧ 𝐴𝑅𝑦)})
Theorem	ecxrncnvep2 38655	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 38656*	Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
Theorem	disjecxrn 38657	Two ways of saying that (𝑅 ⋉ 𝑆)-cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020.) (Revised by Peter Mazsa, 21-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ 𝑆) ∩ [𝐵](𝑅 ⋉ 𝑆)) = ∅ ↔ (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ ([𝐴]𝑆 ∩ [𝐵]𝑆) = ∅)))
Theorem	disjecxrncnvep 38658	Two ways of saying that cosets are disjoint, special case of disjecxrn 38657. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 25-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴](𝑅 ⋉ ◡ E ) ∩ [𝐵](𝑅 ⋉ ◡ E )) = ∅ ↔ ((𝐴 ∩ 𝐵) = ∅ ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)))
Theorem	disjsuc2 38659*	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 38660*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = ◡{⟨⟨𝑦, 𝑧⟩, 𝑢⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)⟨𝑦, 𝑧⟩))}
Theorem	xrninxp2 38661*	Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020.)
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {⟨𝑢, 𝑥⟩ ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))}
Theorem	xrninxpex 38662	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 38663	Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020.)
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶)))
Theorem	br1cnvxrn2 38664*	The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐴◡(𝑅 ⋉ 𝑆)𝐵 ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	elec1cnvxrn2 38665*	Elementhood in the converse range Cartesian product coset of 𝐴. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡(𝑅 ⋉ 𝑆) ↔ ∃𝑦∃𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝐵𝑅𝑦 ∧ 𝐵𝑆𝑧)))
Theorem	rnxrn 38666*	Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020.)
⊢ ran (𝑅 ⋉ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrnres 38667*	Range of a range Cartesian product with a restricted relation. (Contributed by Peter Mazsa, 5-Dec-2021.)
⊢ ran (𝑅 ⋉ (𝑆 ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝑥 ∧ 𝑢𝑆𝑦)}
Theorem	rnxrncnvepres 38668*	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 38669*	Range of a range Cartesian product with a restriction of the identity relation. (Contributed by Peter Mazsa, 6-Dec-2021.)
⊢ ran (𝑅 ⋉ ( I ↾ 𝐴)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑢 = 𝑦 ∧ 𝑢𝑅𝑥)}
Theorem	xrnres 38670	Two ways to express restriction of range Cartesian product, see also xrnres2 38671, xrnres3 38672. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ 𝑆)
Theorem	xrnres2 38671	Two ways to express restriction of range Cartesian product, see also xrnres 38670, xrnres3 38672. (Contributed by Peter Mazsa, 6-Sep-2021.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = (𝑅 ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres3 38672	Two ways to express restriction of range Cartesian product, see also xrnres 38670, xrnres2 38671. (Contributed by Peter Mazsa, 28-Mar-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ↾ 𝐴) ⋉ (𝑆 ↾ 𝐴))
Theorem	xrnres4 38673	Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020.)
⊢ ((𝑅 ⋉ 𝑆) ↾ 𝐴) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (ran (𝑅 ↾ 𝐴) × ran (𝑆 ↾ 𝐴))))
Theorem	xrnresex 38674	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 38675	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 38676	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 38677	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (dom (𝑅 ↾ 𝐴) ∖ {∅})
Theorem	dmxrncnvepres2 38678	Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 29-Jan-2026.)
⊢ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) = (𝐴 ∩ (dom 𝑅 ∖ {∅}))
Theorem	eldmxrncnvepres 38679	Element of the domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴)) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eldmxrncnvepres2 38680*	Element of the domain of the range product with restricted converse epsilon relation. This identifies the domain of the pet 39210 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 38681	An (𝑅 ⋉ (◡ E ↾ 𝐴))-coset in its domain quotient. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋) → ([𝐵](𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [𝐵]𝑅 ≠ ∅)))
Theorem	eceldmqsxrncnvepres2 38682*	An (𝑅 ⋉ (◡ E ↾ 𝐴))-coset in its domain quotient. In the pet 39210 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 38683	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 38684	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 38685	Define the relations class. Proper class relations (like I, see reli 5783) are not elements of it. The element of this class and the relation predicate are the same when 𝑅 is a set (see elrelsrel 38687). 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 38687. 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 38835), 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 38685 (see df-refrels 38836 and the resulting dfrefrels2 38838 and dfrefrels3 38839). 3. Finally, in order to be able to work with proper classes (like iprc 7863) as well, we define the predicate of the relation (see df-refrel 38837) so that it is true for the relevant proper classes (see refrelid 38847), and that the element of the class of the required relations (e.g. elrefrels3 38844) and this predicate are the same in case of sets (see elrefrelsrel 38845). (Contributed by Peter Mazsa, 13-Jun-2018.)
⊢ Rels = 𝒫 (V × V)
Theorem	elrels2 38686	The element of the relations class (df-rels 38685) and the relation predicate (df-rel 5639) are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 14-Jun-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ 𝑅 ⊆ (V × V)))
Theorem	elrelsrel 38687	The element of the relations class (df-rels 38685) and the relation predicate are the same when 𝑅 is a set. (Contributed by Peter Mazsa, 24-Nov-2018.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ Rel 𝑅))
Theorem	elrelsrelim 38688	The element of the relations class is a relation. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ (𝑅 ∈ Rels → Rel 𝑅)
Theorem	elrels5 38689	Equivalent expressions for an element of the relations class. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Rels ↔ (𝑅 ↾ dom 𝑅) = 𝑅))
Theorem	elrels6 38690	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 38691*	Define the quotient map (coset map), see also dfqmap2 38692 and dfqmap3 38693. 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 8652, rnqmap 38699). This is crucial for (i) modular "two-layer" characterizations (map layer + carrier layer) such as dfdisjs6 39187 / dfdisjs7 39188, (ii) transport of properties between a relation and its induced quotient-carrier (e.g. "elements are blocks" via rnqmap 38699), 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 38692*	Alternate definition of the quotient map: QMap in image-of-singleton form. (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ QMap 𝑅 = (𝑥 ∈ dom 𝑅 ↦ (𝑅 “ {𝑥}))
Theorem	dfqmap3 38693*	Alternate definition of the quotient map: QMap as ordered-pair class abstraction. Gives the raw set-builder characterization for extensional proofs, Rel proofs (relqmap 38697), and composition/intersection manipulations. (Contributed by Peter Mazsa, 14-Feb-2026.)
⊢ QMap 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ dom 𝑅 ∧ 𝑦 = [𝑥]𝑅)}
Theorem	ecqmap 38694	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 38695	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 38696	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 38697	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 38698	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 38699	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 38691 and dfqs2 8652. (Contributed by Peter Mazsa, 12-Feb-2026.)
⊢ ran QMap 𝑅 = (dom 𝑅 / 𝑅)
21.26.6  Lifts, shifts, successor, and predecessor
Definition	df-adjliftmap 38700	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 38701. Thus, for 𝑚 in its domain, we have (𝑚 ∪ [𝑚]𝑅), see dfadjliftmap2 38702. 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 38709 and dfsucmap3 38708) are exactly the successor map 𝑚 ↦ suc 𝑚 (cf. dfsucmap4 38710), 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 7371). However, ∪ and ⋉ are introduced in set.mm as class constructors (e.g. df-un 3908), 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 3908, and BlockLiftMap directly using the existing ⋉ constructor dfxrn2 38630, 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 8652, or the equilibrium condition "AdjLiftFix" , in place of {⟨𝑟, 𝑎⟩ ∣ (dom ((𝑅 ∪ ◡ E ) ↾ 𝐴) / ((𝑅 ∪ ◡ E ) ↾ 𝐴)) = 𝑎} (cf. its analog df-blockliftfix 38726). 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 38703) 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 ) ↾ 𝐴)