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	eldisjn0elb 38701	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 38702	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 38703*	Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ ( Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ 𝑆) ∩ [𝑣](𝑅 ⋉ 𝑆)) = ∅))
Theorem	disjorimxrn 38704	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 38705	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimres 38706	Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴))
Theorem	disjimin 38707	Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆))
Theorem	disjiminres 38708	Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴)))
Theorem	disjimxrnres 38709	Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)))
Theorem	disjALTV0 38710	The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ∅
Theorem	disjALTVid 38711	The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.)
⊢ Disj I
Theorem	disjALTVidres 38712	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 38713	The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴))
Theorem	disjALTVxrnidres 38714	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 38715*	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 38716	Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅))
Theorem	dfantisymrel4 38717	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ((𝑅 ∩ ◡𝑅) ⊆ I ∧ Rel 𝑅))
Theorem	dfantisymrel5 38718*	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	antisymrelres 38719*	(Contributed by Peter Mazsa, 25-Jun-2024.)
⊢ ( AntisymRel (𝑅 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))
Theorem	antisymrelressn 38720	(Contributed by Peter Mazsa, 29-Jun-2024.)
⊢ AntisymRel (𝑅 ↾ {𝐴})
21.26.19  Partitions: disjoints on domain quotients
Definition	df-parts 38721	Define the class of all partitions, cf. the comment of df-disjs 38660. 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 38660) is what we call membership partition here, cf. dfmembpart2 38726. The binary partitions relation and the partition predicate are the same, that is, (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴) if 𝐴 and 𝑅 are sets, cf. brpartspart 38729. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ Parts = ( DomainQss ↾ Disjs )
Definition	df-part 38722	Define the partition predicate (read: 𝐴 is a partition by 𝑅). Alternative definition is dfpart2 38725. The binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets, cf. brpartspart 38729. (Contributed by Peter Mazsa, 12-Aug-2021.)
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴))
Definition	df-membparts 38723	Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}
Definition	df-membpart 38724	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 38726. Member partition is the conventional meaning of partition (see the notes of df-parts 38721 and dfmembpart2 38726), we generalize the concept in df-parts 38721 and df-part 38722. Member partition and comember equivalence are the same by mpet 38795. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴)
Theorem	dfpart2 38725	Alternate definition of the partition predicate. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴))
Theorem	dfmembpart2 38726	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 38727	Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴)))
Theorem	brparts2 38728	Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ (dom 𝑅 / 𝑅) = 𝐴)))
Theorem	brpartspart 38729	Binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴))
Theorem	parteq1 38730	Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴))
Theorem	parteq2 38731	Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.)
⊢ (𝐴 = 𝐵 → (𝑅 Part 𝐴 ↔ 𝑅 Part 𝐵))
Theorem	parteq12 38732	Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐵))
Theorem	parteq1i 38733	Equality theorem for partition, inference version. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)
Theorem	parteq1d 38734	Equality theorem for partition, deduction version. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴))
Theorem	partsuc2 38735	Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ (((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) Part ((𝐴 ∪ {𝐴}) ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴)
Theorem	partsuc 38736	Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ (((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) Part (suc 𝐴 ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴)
21.26.20  Partition-Equivalence Theorems
Theorem	disjim 38737	The "Divide et Aequivalere" Theorem: every disjoint relation generates equivalent cosets by the relation: generalization of the former prter1 38835, cf. eldisjim 38740. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 17-Sep-2021.)
⊢ ( Disj 𝑅 → EqvRel ≀ 𝑅)
Theorem	disjimi 38738	Every disjoint relation generates equivalent cosets by the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.)
⊢ Disj 𝑅    ⇒   ⊢ EqvRel ≀ 𝑅
Theorem	detlem 38739	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 38740	If the elements of 𝐴 are disjoint, then it has equivalent coelements (former prter1 38835). Special case of disjim 38737. (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 38741	Alternate form of eldisjim 38740. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ ( ElDisj 𝐴 → EqvRel ∼ 𝐴)
Theorem	eqvrel0 38742	The null class is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ∅
Theorem	det0 38743	The cosets by the null class are in equivalence relation if and only if the null class is disjoint (which it is, see disjALTV0 38710). (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj ∅ ↔ EqvRel ≀ ∅)
Theorem	eqvrelcoss0 38744	The cosets by the null class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ EqvRel ≀ ∅
Theorem	eqvrelid 38745	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 38746	The cosets by a restricted identity relation is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ≀ ( I ↾ 𝐴)
Theorem	eqvrel1cossinidres 38747	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 38748	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 38749	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 38750	The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ EqvRel ≀ I
Theorem	detidres 38751	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 38752	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 38753	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 38754*	Lemma for disjdmqseq 38761, partim2 38763 and petlem 38768 via disjlem17 38755, (general version of the former prtlem14 38830). (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅) → ((𝐴 ∈ [𝑥]𝑅 ∧ 𝐴 ∈ [𝑦]𝑅) → [𝑥]𝑅 = [𝑦]𝑅)))
Theorem	disjlem17 38755*	Lemma for disjdmqseq 38761, partim2 38763 and petlem 38768 via disjlem18 38756, (general version of the former prtlem17 38832). (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (∃𝑦 ∈ dom 𝑅(𝐴 ∈ [𝑦]𝑅 ∧ 𝐵 ∈ [𝑦]𝑅) → 𝐵 ∈ [𝑥]𝑅)))
Theorem	disjlem18 38756*	Lemma for disjdmqseq 38761, partim2 38763 and petlem 38768 via disjlem19 38757, (general version of the former prtlem18 38833). (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (𝐵 ∈ [𝑥]𝑅 ↔ 𝐴 ≀ 𝑅𝐵))))
Theorem	disjlem19 38757*	Lemma for disjdmqseq 38761, partim2 38763 and petlem 38768 via disjdmqs 38760, (general version of the former prtlem19 38834). (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → [𝑥]𝑅 = [𝐴] ≀ 𝑅)))
Theorem	disjdmqsss 38758	Lemma for disjdmqseq 38761 via disjdmqs 38760. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) ⊆ (dom ≀ 𝑅 / ≀ 𝑅))
Theorem	disjdmqscossss 38759	Lemma for disjdmqseq 38761 via disjdmqs 38760. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom ≀ 𝑅 / ≀ 𝑅) ⊆ (dom 𝑅 / 𝑅))
Theorem	disjdmqs 38760	If a relation is disjoint, its domain quotient is equal to the domain quotient of the cosets by it. Lemma for partim2 38763 and petlem 38768 via disjdmqseq 38761. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅))
Theorem	disjdmqseq 38761	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 38762 (which is the closest theorem to the former prter2 38837). Lemma for partim2 38763 and petlem 38768. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	eldisjn0el 38762	Special case of disjdmqseq 38761 (perhaps this is the closest theorem to the former prter2 38837). (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ ( ElDisj 𝐴 → (¬ ∅ ∈ 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	partim2 38763	Disjoint relation on its natural domain implies an equivalence relation on the cosets of the relation, on its natural domain, cf. partim 38764. Lemma for petlem 38768. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	partim 38764	Partition implies equivalence relation by the cosets of the relation on its natural domain, cf. partim2 38763. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ (𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴)
Theorem	partimeq 38765	Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq 38635. (Contributed by Peter Mazsa, 25-Dec-2024.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅))
Theorem	eldisjlem19 38766*	Special case of disjlem19 38757 (together with membpartlem19 38767, this is former prtlem19 38834). (Contributed by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ((𝑢 ∈ dom (◡ E ↾ 𝐴) ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴)))
Theorem	membpartlem19 38767*	Together with disjlem19 38757, this is former prtlem19 38834. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ((𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴)))
Theorem	petlem 38768	If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 38789), or converse function (cf. dfdisjALTV 38669), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 38806. (Contributed by Peter Mazsa, 18-Sep-2021.)
⊢ (( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴) → Disj 𝑅)    ⇒   ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	petlemi 38769	If you can prove disjointness (e.g. disjALTV0 38710, disjALTVid 38711, disjALTVidres 38712, disjALTVxrnidres 38714, search for theorems containing the ' |- Disj ' string), or the same with converse function (cf. dfdisjALTV 38669), 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 38770	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 38771	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 38772	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 38773	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 38774	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 38775	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 38746. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( I ↾ 𝐴) Part 𝐴 ↔ ≀ ( I ↾ 𝐴) ErALTV 𝐴)
Theorem	petinidres2 38776	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 38777	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 38405, disjALTVinidres 38713 and eqvrel1cossinidres 38747. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ∩ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ ( I ↾ 𝐴)) ErALTV 𝐴)
Theorem	petxrnidres2 38778	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 38779	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 38407, disjALTVxrnidres 38714 and eqvrel1cossxrnidres 38748. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ⋉ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ErALTV 𝐴)
Theorem	eqvreldisj1 38780*	The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj2 38781, eqvreldisj3 38782). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 3-Dec-2024.)
⊢ ( EqvRel 𝑅 → ∀𝑥 ∈ (𝐴 / 𝑅)∀𝑦 ∈ (𝐴 / 𝑅)(𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	eqvreldisj2 38781	The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj3 38782). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 19-Sep-2021.)
⊢ ( EqvRel 𝑅 → ElDisj (𝐴 / 𝑅))
Theorem	eqvreldisj3 38782	The elements of the quotient set of an equivalence relation are disjoint (cf. qsdisj2 8853). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 20-Jun-2019.) (Revised by Peter Mazsa, 19-Sep-2021.)
⊢ ( EqvRel 𝑅 → Disj (◡ E ↾ (𝐴 / 𝑅)))
Theorem	eqvreldisj4 38783	Intersection with the converse epsilon relation restricted to the quotient set of an equivalence relation is disjoint. (Contributed by Peter Mazsa, 30-May-2020.) (Revised by Peter Mazsa, 31-Dec-2021.)
⊢ ( EqvRel 𝑅 → Disj (𝑆 ∩ (◡ E ↾ (𝐵 / 𝑅))))
Theorem	eqvreldisj5 38784	Range Cartesian product with converse epsilon relation restricted to the quotient set of an equivalence relation is disjoint. (Contributed by Peter Mazsa, 30-May-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ ( EqvRel 𝑅 → Disj (𝑆 ⋉ (◡ E ↾ (𝐵 / 𝑅))))
Theorem	eqvrelqseqdisj2 38785	Implication of eqvreldisj2 38781, lemma for The Main Theorem of Equivalences mainer 38790. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → ElDisj 𝐴)
Theorem	fences3 38786	Implication of eqvrelqseqdisj2 38785 and n0eldmqseq 38605, see comment of fences 38800. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	eqvrelqseqdisj3 38787	Implication of eqvreldisj3 38782, lemma for the Member Partition Equivalence Theorem mpet3 38792. (Contributed by Peter Mazsa, 27-Oct-2020.) (Revised by Peter Mazsa, 24-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (◡ E ↾ 𝐴))
Theorem	eqvrelqseqdisj4 38788	Lemma for petincnvepres2 38804. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ∩ (◡ E ↾ 𝐴)))
Theorem	eqvrelqseqdisj5 38789	Lemma for the Partition-Equivalence Theorem pet2 38806. (Contributed by Peter Mazsa, 15-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ⋉ (◡ E ↾ 𝐴)))
Theorem	mainer 38790	The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → CoMembEr 𝐴)
Theorem	partimcomember 38791	Partition with general 𝑅 (in addition to the member partition cf. mpet 38795 and mpet2 38796) implies equivalent comembers. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.)
⊢ (𝑅 Part 𝐴 → CoMembEr 𝐴)
Theorem	mpet3 38792	Member Partition-Equivalence Theorem. Together with mpet 38795 mpet2 38796, mostly in its conventional cpet 38794 and cpet2 38793 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38806 with general 𝑅). (Contributed by Peter Mazsa, 4-May-2018.) (Revised by Peter Mazsa, 26-Sep-2021.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	cpet2 38793	The conventional form of the Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have called disjoint or partition what we call element disjoint or member partition, see also cpet 38794. Together with cpet 38794, mpet 38795 mpet2 38796, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38806 with general 𝑅). (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	cpet 38794	The conventional form of Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have been calling disjoint or partition what we call element disjoint or member partition, see also cpet2 38793. Cf. mpet 38795, mpet2 38796 and mpet3 38792 for unconventional forms of Member Partition-Equivalence Theorem. Cf. pet 38807 and pet2 38806 for Partition-Equivalence Theorem with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	mpet 38795	Member Partition-Equivalence Theorem in almost its shortest possible form, cf. the 0-ary version mpets 38798. Member partition and comember equivalence relation are the same (or: each element of 𝐴 have equivalent comembers if and only if 𝐴 is a member partition). Together with mpet2 38796, mpet3 38792, and with the conventional cpet 38794 and cpet2 38793, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38806 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴)
Theorem	mpet2 38796	Member Partition-Equivalence Theorem in a shorter form. Together with mpet 38795 mpet3 38792, mostly in its conventional cpet 38794 and cpet2 38793 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38806 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ ((◡ E ↾ 𝐴) Part 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)
Theorem	mpets2 38797	Member Partition-Equivalence Theorem with binary relations, cf. mpet2 38796. (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) Parts 𝐴 ↔ ≀ (◡ E ↾ 𝐴) Ers 𝐴))
Theorem	mpets 38798	Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet 38807, the Partition-Equivalence Theorem, with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ MembParts = CoMembErs
Theorem	mainpart 38799	Partition with general 𝑅 also imply member partition. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.)
⊢ (𝑅 Part 𝐴 → MembPart 𝐴)
Theorem	fences 38800	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet 38795) generate a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → MembPart 𝐴)