P. 388 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38701-38800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eldisjs3 38701*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs4 38702*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs5 38703*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels )))
Theorem	eldisjsdisj 38704	The element of the class of disjoint relations and the disjoint relation predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ Disj 𝑅))
Theorem	eleldisjs 38705	Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs ))
Theorem	eleldisjseldisj 38706	The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set. (Contributed by Peter Mazsa, 23-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴))
Theorem	disjrel 38707	Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.)
⊢ ( Disj 𝑅 → Rel 𝑅)
Theorem	disjss 38708	Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjssi 38709	Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( Disj 𝐵 → Disj 𝐴)
Theorem	disjssd 38710	Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjeq 38711	Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjeqi 38712	Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( Disj 𝐴 ↔ Disj 𝐵)
Theorem	disjeqd 38713	Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjdmqseqeq1 38714	Lemma for the equality theorem for partition parteq1 38751. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴)))
Theorem	eldisjss 38715	Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjssi 38716	Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( ElDisj 𝐵 → ElDisj 𝐴)
Theorem	eldisjssd 38717	Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjeq 38718	Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	eldisjeqi 38719	Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵)
Theorem	eldisjeqd 38720	Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	disjres 38721*	Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ (Rel 𝑅 → ( Disj (𝑅 ↾ 𝐴) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅)))
Theorem	eldisjn0elb 38722	Two forms of disjoint elements when the empty set is not an element of the class. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( Disj (◡ E ↾ 𝐴) ∧ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴))
Theorem	disjxrn 38723	Two ways of saying that a range Cartesian product is disjoint. (Contributed by Peter Mazsa, 17-Jun-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ ( Disj (𝑅 ⋉ 𝑆) ↔ ( ≀ ◡𝑅 ∩ ≀ ◡𝑆) ⊆ I )
Theorem	disjxrnres5 38724*	Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ ( Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ 𝑆) ∩ [𝑣](𝑅 ⋉ 𝑆)) = ∅))
Theorem	disjorimxrn 38725	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (( Disj 𝑅 ∨ Disj 𝑆) → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimxrn 38726	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimres 38727	Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴))
Theorem	disjimin 38728	Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆))
Theorem	disjiminres 38729	Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴)))
Theorem	disjimxrnres 38730	Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)))
Theorem	disjALTV0 38731	The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ∅
Theorem	disjALTVid 38732	The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.)
⊢ Disj I
Theorem	disjALTVidres 38733	The class of identity relations restricted is disjoint. (Contributed by Peter Mazsa, 28-Jun-2020.) (Revised by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ( I ↾ 𝐴)
Theorem	disjALTVinidres 38734	The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴))
Theorem	disjALTVxrnidres 38735	The class of range Cartesian product with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 25-Jun-2020.) (Revised by Peter Mazsa, 27-Sep-2021.)
⊢ Disj (𝑅 ⋉ ( I ↾ 𝐴))
Theorem	disjsuc 38736*	Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → ( Disj (𝑅 ⋉ (◡ E ↾ suc 𝐴)) ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
21.26.18  Antisymmetry
Definition	df-antisymrel 38737	Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅))
Theorem	dfantisymrel4 38738	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ((𝑅 ∩ ◡𝑅) ⊆ I ∧ Rel 𝑅))
Theorem	dfantisymrel5 38739*	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	antisymrelres 38740*	(Contributed by Peter Mazsa, 25-Jun-2024.)
⊢ ( AntisymRel (𝑅 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))
Theorem	antisymrelressn 38741	(Contributed by Peter Mazsa, 29-Jun-2024.)
⊢ AntisymRel (𝑅 ↾ {𝐴})
21.26.19  Partitions: disjoints on domain quotients
Definition	df-parts 38742	Define the class of all partitions, cf. the comment of df-disjs 38681. Partitions are disjoints on domain quotients (or: domain quotients restricted to disjoints). This is a more general meaning of partition than we we are familiar with: the conventional meaning of partition (e.g. partition 𝐴 of 𝑋, [Halmos] p. 28: "A partition of 𝑋 is a disjoint collection 𝐴 of non-empty subsets of 𝑋 whose union is 𝑋", or Definition 35, [Suppes] p. 83., cf. https://oeis.org/A000110 38681) is what we call membership partition here, cf. dfmembpart2 38747. The binary partitions relation and the partition predicate are the same, that is, (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴) if 𝐴 and 𝑅 are sets, cf. brpartspart 38750. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ Parts = ( DomainQss ↾ Disjs )
Definition	df-part 38743	Define the partition predicate (read: 𝐴 is a partition by 𝑅). Alternative definition is dfpart2 38746. The binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets, cf. brpartspart 38750. (Contributed by Peter Mazsa, 12-Aug-2021.)
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴))
Definition	df-membparts 38744	Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}
Definition	df-membpart 38745	Define the member partition predicate, or the disjoint restricted element relation on its domain quotient predicate. (Read: 𝐴 is a member partition.) A alternative definition is dfmembpart2 38747. Member partition is the conventional meaning of partition (see the notes of df-parts 38742 and dfmembpart2 38747), we generalize the concept in df-parts 38742 and df-part 38743. Member partition and comember equivalence are the same by mpet 38816. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴)
Theorem	dfpart2 38746	Alternate definition of the partition predicate. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴))
Theorem	dfmembpart2 38747	Alternate definition of the conventional membership case of partition. Partition 𝐴 of 𝑋, [Halmos] p. 28: "A partition of 𝑋 is a disjoint collection 𝐴 of non-empty subsets of 𝑋 whose union is 𝑋", or Definition 35, [Suppes] p. 83., cf. https://oeis.org/A000110 . (Contributed by Peter Mazsa, 14-Aug-2021.)
⊢ ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	brparts 38748	Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴)))
Theorem	brparts2 38749	Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ (dom 𝑅 / 𝑅) = 𝐴)))
Theorem	brpartspart 38750	Binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴))
Theorem	parteq1 38751	Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴))
Theorem	parteq2 38752	Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.)
⊢ (𝐴 = 𝐵 → (𝑅 Part 𝐴 ↔ 𝑅 Part 𝐵))
Theorem	parteq12 38753	Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐵))
Theorem	parteq1i 38754	Equality theorem for partition, inference version. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)
Theorem	parteq1d 38755	Equality theorem for partition, deduction version. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴))
Theorem	partsuc2 38756	Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ (((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) Part ((𝐴 ∪ {𝐴}) ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴)
Theorem	partsuc 38757	Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ (((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) Part (suc 𝐴 ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴)
21.26.20  Partition-Equivalence Theorems
Theorem	disjim 38758	The "Divide et Aequivalere" Theorem: every disjoint relation generates equivalent cosets by the relation: generalization of the former prter1 38857, cf. eldisjim 38761. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 17-Sep-2021.)
⊢ ( Disj 𝑅 → EqvRel ≀ 𝑅)
Theorem	disjimi 38759	Every disjoint relation generates equivalent cosets by the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.)
⊢ Disj 𝑅    ⇒   ⊢ EqvRel ≀ 𝑅
Theorem	detlem 38760	If a relation is disjoint, then it is equivalent to the equivalent cosets of the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.)
⊢ Disj 𝑅    ⇒   ⊢ ( Disj 𝑅 ↔ EqvRel ≀ 𝑅)
Theorem	eldisjim 38761	If the elements of 𝐴 are disjoint, then it has equivalent coelements (former prter1 38857). Special case of disjim 38758. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 8-Feb-2018.) ( Revised by Peter Mazsa, 23-Sep-2021.)
⊢ ( ElDisj 𝐴 → CoElEqvRel 𝐴)
Theorem	eldisjim2 38762	Alternate form of eldisjim 38761. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ ( ElDisj 𝐴 → EqvRel ∼ 𝐴)
Theorem	eqvrel0 38763	The null class is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ∅
Theorem	det0 38764	The cosets by the null class are in equivalence relation if and only if the null class is disjoint (which it is, see disjALTV0 38731). (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj ∅ ↔ EqvRel ≀ ∅)
Theorem	eqvrelcoss0 38765	The cosets by the null class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ EqvRel ≀ ∅
Theorem	eqvrelid 38766	The identity relation is an equivalence relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel I
Theorem	eqvrel1cossidres 38767	The cosets by a restricted identity relation is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ≀ ( I ↾ 𝐴)
Theorem	eqvrel1cossinidres 38768	The cosets by an intersection with a restricted identity relation are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ≀ (𝑅 ∩ ( I ↾ 𝐴))
Theorem	eqvrel1cossxrnidres 38769	The cosets by a range Cartesian product with a restricted identity relation are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ≀ (𝑅 ⋉ ( I ↾ 𝐴))
Theorem	detid 38770	The cosets by the identity relation are in equivalence relation if and only if the identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj I ↔ EqvRel ≀ I )
Theorem	eqvrelcossid 38771	The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ EqvRel ≀ I
Theorem	detidres 38772	The cosets by the restricted identity relation are in equivalence relation if and only if the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj ( I ↾ 𝐴) ↔ EqvRel ≀ ( I ↾ 𝐴))
Theorem	detinidres 38773	The cosets by the intersection with the restricted identity relation are in equivalence relation if and only if the intersection with the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj (𝑅 ∩ ( I ↾ 𝐴)) ↔ EqvRel ≀ (𝑅 ∩ ( I ↾ 𝐴)))
Theorem	detxrnidres 38774	The cosets by the range Cartesian product with the restricted identity relation are in equivalence relation if and only if the range Cartesian product with the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj (𝑅 ⋉ ( I ↾ 𝐴)) ↔ EqvRel ≀ (𝑅 ⋉ ( I ↾ 𝐴)))
Theorem	disjlem14 38775*	Lemma for disjdmqseq 38782, partim2 38784 and petlem 38789 via disjlem17 38776, (general version of the former prtlem14 38852). (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅) → ((𝐴 ∈ [𝑥]𝑅 ∧ 𝐴 ∈ [𝑦]𝑅) → [𝑥]𝑅 = [𝑦]𝑅)))
Theorem	disjlem17 38776*	Lemma for disjdmqseq 38782, partim2 38784 and petlem 38789 via disjlem18 38777, (general version of the former prtlem17 38854). (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (∃𝑦 ∈ dom 𝑅(𝐴 ∈ [𝑦]𝑅 ∧ 𝐵 ∈ [𝑦]𝑅) → 𝐵 ∈ [𝑥]𝑅)))
Theorem	disjlem18 38777*	Lemma for disjdmqseq 38782, partim2 38784 and petlem 38789 via disjlem19 38778, (general version of the former prtlem18 38855). (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (𝐵 ∈ [𝑥]𝑅 ↔ 𝐴 ≀ 𝑅𝐵))))
Theorem	disjlem19 38778*	Lemma for disjdmqseq 38782, partim2 38784 and petlem 38789 via disjdmqs 38781, (general version of the former prtlem19 38856). (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → [𝑥]𝑅 = [𝐴] ≀ 𝑅)))
Theorem	disjdmqsss 38779	Lemma for disjdmqseq 38782 via disjdmqs 38781. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) ⊆ (dom ≀ 𝑅 / ≀ 𝑅))
Theorem	disjdmqscossss 38780	Lemma for disjdmqseq 38782 via disjdmqs 38781. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom ≀ 𝑅 / ≀ 𝑅) ⊆ (dom 𝑅 / 𝑅))
Theorem	disjdmqs 38781	If a relation is disjoint, its domain quotient is equal to the domain quotient of the cosets by it. Lemma for partim2 38784 and petlem 38789 via disjdmqseq 38782. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅))
Theorem	disjdmqseq 38782	If a relation is disjoint, its domain quotient is equal to a class if and only if the domain quotient of the cosets by it is equal to the class. General version of eldisjn0el 38783 (which is the closest theorem to the former prter2 38859). Lemma for partim2 38784 and petlem 38789. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	eldisjn0el 38783	Special case of disjdmqseq 38782 (perhaps this is the closest theorem to the former prter2 38859). (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ ( ElDisj 𝐴 → (¬ ∅ ∈ 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	partim2 38784	Disjoint relation on its natural domain implies an equivalence relation on the cosets of the relation, on its natural domain, cf. partim 38785. Lemma for petlem 38789. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	partim 38785	Partition implies equivalence relation by the cosets of the relation on its natural domain, cf. partim2 38784. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ (𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴)
Theorem	partimeq 38786	Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq 38656. (Contributed by Peter Mazsa, 25-Dec-2024.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅))
Theorem	eldisjlem19 38787*	Special case of disjlem19 38778 (together with membpartlem19 38788, this is former prtlem19 38856). (Contributed by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ((𝑢 ∈ dom (◡ E ↾ 𝐴) ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴)))
Theorem	membpartlem19 38788*	Together with disjlem19 38778, this is former prtlem19 38856. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ((𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴)))
Theorem	petlem 38789	If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 38810), or converse function (cf. dfdisjALTV 38690), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 38827. (Contributed by Peter Mazsa, 18-Sep-2021.)
⊢ (( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴) → Disj 𝑅)    ⇒   ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	petlemi 38790	If you can prove disjointness (e.g. disjALTV0 38731, disjALTVid 38732, disjALTVidres 38733, disjALTVxrnidres 38735, search for theorems containing the ' |- Disj ' string), or the same with converse function (cf. dfdisjALTV 38690), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. (Contributed by Peter Mazsa, 18-Sep-2021.)
⊢ Disj 𝑅    ⇒   ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	pet02 38791	Class 𝐴 is a partition by the null class if and only if the cosets by the null class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( Disj ∅ ∧ (dom ∅ / ∅) = 𝐴) ↔ ( EqvRel ≀ ∅ ∧ (dom ≀ ∅ / ≀ ∅) = 𝐴))
Theorem	pet0 38792	Class 𝐴 is a partition by the null class if and only if the cosets by the null class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (∅ Part 𝐴 ↔ ≀ ∅ ErALTV 𝐴)
Theorem	petid2 38793	Class 𝐴 is a partition by the identity class if and only if the cosets by the identity class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( Disj I ∧ (dom I / I ) = 𝐴) ↔ ( EqvRel ≀ I ∧ (dom ≀ I / ≀ I ) = 𝐴))
Theorem	petid 38794	A class is a partition by the identity class if and only if the cosets by the identity class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( I Part 𝐴 ↔ ≀ I ErALTV 𝐴)
Theorem	petidres2 38795	Class 𝐴 is a partition by the identity class restricted to it if and only if the cosets by the restricted identity class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( Disj ( I ↾ 𝐴) ∧ (dom ( I ↾ 𝐴) / ( I ↾ 𝐴)) = 𝐴) ↔ ( EqvRel ≀ ( I ↾ 𝐴) ∧ (dom ≀ ( I ↾ 𝐴) / ≀ ( I ↾ 𝐴)) = 𝐴))
Theorem	petidres 38796	A class is a partition by identity class restricted to it if and only if the cosets by the restricted identity class are in equivalence relation on it, cf. eqvrel1cossidres 38767. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( I ↾ 𝐴) Part 𝐴 ↔ ≀ ( I ↾ 𝐴) ErALTV 𝐴)
Theorem	petinidres2 38797	Class 𝐴 is a partition by an intersection with the identity class restricted to it if and only if the cosets by the intersection are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( Disj (𝑅 ∩ ( I ↾ 𝐴)) ∧ (dom (𝑅 ∩ ( I ↾ 𝐴)) / (𝑅 ∩ ( I ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ∩ ( I ↾ 𝐴)) ∧ (dom ≀ (𝑅 ∩ ( I ↾ 𝐴)) / ≀ (𝑅 ∩ ( I ↾ 𝐴))) = 𝐴))
Theorem	petinidres 38798	A class is a partition by an intersection with the identity class restricted to it if and only if the cosets by the intersection are in equivalence relation on it. Cf. br1cossinidres 38425, disjALTVinidres 38734 and eqvrel1cossinidres 38768. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ∩ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ ( I ↾ 𝐴)) ErALTV 𝐴)
Theorem	petxrnidres2 38799	Class 𝐴 is a partition by a range Cartesian product with the identity class restricted to it if and only if the cosets by the range Cartesian product are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( Disj (𝑅 ⋉ ( I ↾ 𝐴)) ∧ (dom (𝑅 ⋉ ( I ↾ 𝐴)) / (𝑅 ⋉ ( I ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ ( I ↾ 𝐴)) / ≀ (𝑅 ⋉ ( I ↾ 𝐴))) = 𝐴))
Theorem	petxrnidres 38800	A class is a partition by a range Cartesian product with the identity class restricted to it if and only if the cosets by the range Cartesian product are in equivalence relation on it. Cf. br1cossxrnidres 38427, disjALTVxrnidres 38735 and eqvrel1cossxrnidres 38769. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ⋉ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ErALTV 𝐴)