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	disjxrn 39001	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 39002*	Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ ( Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ 𝑆) ∩ [𝑣](𝑅 ⋉ 𝑆)) = ∅))
Theorem	disjorimxrn 39003	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 39004	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimres 39005	Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴))
Theorem	disjimin 39006	Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆))
Theorem	disjiminres 39007	Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴)))
Theorem	disjimxrnres 39008	Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)))
Theorem	disjALTV0 39009	The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ∅
Theorem	disjALTVid 39010	The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.)
⊢ Disj I
Theorem	disjALTVidres 39011	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 39012	The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴))
Theorem	disjALTVxrnidres 39013	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 39014*	Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → ( Disj (𝑅 ⋉ (◡ E ↾ suc 𝐴)) ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
21.26.19  Antisymmetry
Definition	df-antisymrel 39015	Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅))
Theorem	dfantisymrel4 39016	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ ((𝑅 ∩ ◡𝑅) ⊆ I ∧ Rel 𝑅))
Theorem	dfantisymrel5 39017*	Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.)
⊢ ( AntisymRel 𝑅 ↔ (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	antisymrelres 39018*	(Contributed by Peter Mazsa, 25-Jun-2024.)
⊢ ( AntisymRel (𝑅 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))
Theorem	antisymrelressn 39019	(Contributed by Peter Mazsa, 29-Jun-2024.)
⊢ AntisymRel (𝑅 ↾ {𝐴})
21.26.20  Partitions: disjoints on domain quotients
Definition	df-parts 39020	Define the class of all partitions, cf. the comment of df-disjs 38959. 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 38959) is what we call membership partition here, cf. dfmembpart2 39025. The binary partitions relation and the partition predicate are the same, that is, (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴) if 𝐴 and 𝑅 are sets, cf. brpartspart 39028. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ Parts = ( DomainQss ↾ Disjs )
Definition	df-part 39021	Define the partition predicate (read: 𝐴 is a partition by 𝑅). Alternative definition is dfpart2 39024. The binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets, cf. brpartspart 39028. (Contributed by Peter Mazsa, 12-Aug-2021.)
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴))
Definition	df-membparts 39022	Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}
Definition	df-membpart 39023	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 39025. Member partition is the conventional meaning of partition (see the notes of df-parts 39020 and dfmembpart2 39025), we generalize the concept in df-parts 39020 and df-part 39021. Member partition and comember equivalence are the same by mpet 39094. (Contributed by Peter Mazsa, 26-Jun-2021.)
⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴)
Theorem	dfpart2 39024	Alternate definition of the partition predicate. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴))
Theorem	dfmembpart2 39025	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 39026	Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021.)
⊢ (𝐴 ∈ 𝑉 → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴)))
Theorem	brparts2 39027	Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ (dom 𝑅 / 𝑅) = 𝐴)))
Theorem	brpartspart 39028	Binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴))
Theorem	parteq1 39029	Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴))
Theorem	parteq2 39030	Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.)
⊢ (𝐴 = 𝐵 → (𝑅 Part 𝐴 ↔ 𝑅 Part 𝐵))
Theorem	parteq12 39031	Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐵))
Theorem	parteq1i 39032	Equality theorem for partition, inference version. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)
Theorem	parteq1d 39033	Equality theorem for partition, deduction version. (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴))
Theorem	partsuc2 39034	Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ (((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) Part ((𝐴 ∪ {𝐴}) ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴)
Theorem	partsuc 39035	Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024.)
⊢ (((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) Part (suc 𝐴 ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴)
21.26.21  Partition-Equivalence Theorems
Theorem	disjim 39036	The "Divide et Aequivalere" Theorem: every disjoint relation generates equivalent cosets by the relation: generalization of the former prter1 39135, cf. eldisjim 39039. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 17-Sep-2021.)
⊢ ( Disj 𝑅 → EqvRel ≀ 𝑅)
Theorem	disjimi 39037	Every disjoint relation generates equivalent cosets by the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.)
⊢ Disj 𝑅    ⇒   ⊢ EqvRel ≀ 𝑅
Theorem	detlem 39038	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 39039	If the elements of 𝐴 are disjoint, then it has equivalent coelements (former prter1 39135). Special case of disjim 39036. (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 39040	Alternate form of eldisjim 39039. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ ( ElDisj 𝐴 → EqvRel ∼ 𝐴)
Theorem	eqvrel0 39041	The null class is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ∅
Theorem	det0 39042	The cosets by the null class are in equivalence relation if and only if the null class is disjoint (which it is, see disjALTV0 39009). (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj ∅ ↔ EqvRel ≀ ∅)
Theorem	eqvrelcoss0 39043	The cosets by the null class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ EqvRel ≀ ∅
Theorem	eqvrelid 39044	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 39045	The cosets by a restricted identity relation is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ EqvRel ≀ ( I ↾ 𝐴)
Theorem	eqvrel1cossinidres 39046	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 39047	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 39048	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 39049	The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ EqvRel ≀ I
Theorem	detidres 39050	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 39051	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 39052	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 39053*	Lemma for disjdmqseq 39060, partim2 39062 and petlem 39067 via disjlem17 39054, (general version of the former prtlem14 39130). (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅) → ((𝐴 ∈ [𝑥]𝑅 ∧ 𝐴 ∈ [𝑦]𝑅) → [𝑥]𝑅 = [𝑦]𝑅)))
Theorem	disjlem17 39054*	Lemma for disjdmqseq 39060, partim2 39062 and petlem 39067 via disjlem18 39055, (general version of the former prtlem17 39132). (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (∃𝑦 ∈ dom 𝑅(𝐴 ∈ [𝑦]𝑅 ∧ 𝐵 ∈ [𝑦]𝑅) → 𝐵 ∈ [𝑥]𝑅)))
Theorem	disjlem18 39055*	Lemma for disjdmqseq 39060, partim2 39062 and petlem 39067 via disjlem19 39056, (general version of the former prtlem18 39133). (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (𝐵 ∈ [𝑥]𝑅 ↔ 𝐴 ≀ 𝑅𝐵))))
Theorem	disjlem19 39056*	Lemma for disjdmqseq 39060, partim2 39062 and petlem 39067 via disjdmqs 39059, (general version of the former prtlem19 39134). (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → [𝑥]𝑅 = [𝐴] ≀ 𝑅)))
Theorem	disjdmqsss 39057	Lemma for disjdmqseq 39060 via disjdmqs 39059. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) ⊆ (dom ≀ 𝑅 / ≀ 𝑅))
Theorem	disjdmqscossss 39058	Lemma for disjdmqseq 39060 via disjdmqs 39059. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom ≀ 𝑅 / ≀ 𝑅) ⊆ (dom 𝑅 / 𝑅))
Theorem	disjdmqs 39059	If a relation is disjoint, its domain quotient is equal to the domain quotient of the cosets by it. Lemma for partim2 39062 and petlem 39067 via disjdmqseq 39060. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅))
Theorem	disjdmqseq 39060	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 39061 (which is the closest theorem to the former prter2 39137). Lemma for partim2 39062 and petlem 39067. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	eldisjn0el 39061	Special case of disjdmqseq 39060 (perhaps this is the closest theorem to the former prter2 39137). (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ ( ElDisj 𝐴 → (¬ ∅ ∈ 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	partim2 39062	Disjoint relation on its natural domain implies an equivalence relation on the cosets of the relation, on its natural domain, cf. partim 39063. Lemma for petlem 39067. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	partim 39063	Partition implies equivalence relation by the cosets of the relation on its natural domain, cf. partim2 39062. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ (𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴)
Theorem	partimeq 39064	Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq 38934. (Contributed by Peter Mazsa, 25-Dec-2024.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅))
Theorem	eldisjlem19 39065*	Special case of disjlem19 39056 (together with membpartlem19 39066, this is former prtlem19 39134). (Contributed by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ((𝑢 ∈ dom (◡ E ↾ 𝐴) ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴)))
Theorem	membpartlem19 39066*	Together with disjlem19 39056, this is former prtlem19 39134. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ((𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴)))
Theorem	petlem 39067	If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 39088), or converse function (cf. dfdisjALTV 38968), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 39105. (Contributed by Peter Mazsa, 18-Sep-2021.)
⊢ (( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴) → Disj 𝑅)    ⇒   ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	petlemi 39068	If you can prove disjointness (e.g. disjALTV0 39009, disjALTVid 39010, disjALTVidres 39011, disjALTVxrnidres 39013, search for theorems containing the ' |- Disj ' string), or the same with converse function (cf. dfdisjALTV 38968), 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 39069	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 39070	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 39071	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 39072	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 39073	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 39074	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 39045. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( I ↾ 𝐴) Part 𝐴 ↔ ≀ ( I ↾ 𝐴) ErALTV 𝐴)
Theorem	petinidres2 39075	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 39076	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 38708, disjALTVinidres 39012 and eqvrel1cossinidres 39046. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ∩ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ ( I ↾ 𝐴)) ErALTV 𝐴)
Theorem	petxrnidres2 39077	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 39078	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 38710, disjALTVxrnidres 39013 and eqvrel1cossxrnidres 39047. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ⋉ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ErALTV 𝐴)
Theorem	eqvreldisj1 39079*	The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj2 39080, eqvreldisj3 39081). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 3-Dec-2024.)
⊢ ( EqvRel 𝑅 → ∀𝑥 ∈ (𝐴 / 𝑅)∀𝑦 ∈ (𝐴 / 𝑅)(𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	eqvreldisj2 39080	The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj3 39081). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 19-Sep-2021.)
⊢ ( EqvRel 𝑅 → ElDisj (𝐴 / 𝑅))
Theorem	eqvreldisj3 39081	The elements of the quotient set of an equivalence relation are disjoint (cf. qsdisj2 8732). (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 39082	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 39083	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 39084	Implication of eqvreldisj2 39080, lemma for The Main Theorem of Equivalences mainer 39089. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → ElDisj 𝐴)
Theorem	fences3 39085	Implication of eqvrelqseqdisj2 39084 and n0eldmqseq 38904, see comment of fences 39099. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	eqvrelqseqdisj3 39086	Implication of eqvreldisj3 39081, lemma for the Member Partition Equivalence Theorem mpet3 39091. (Contributed by Peter Mazsa, 27-Oct-2020.) (Revised by Peter Mazsa, 24-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (◡ E ↾ 𝐴))
Theorem	eqvrelqseqdisj4 39087	Lemma for petincnvepres2 39103. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ∩ (◡ E ↾ 𝐴)))
Theorem	eqvrelqseqdisj5 39088	Lemma for the Partition-Equivalence Theorem pet2 39105. (Contributed by Peter Mazsa, 15-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ⋉ (◡ E ↾ 𝐴)))
Theorem	mainer 39089	The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → CoMembEr 𝐴)
Theorem	partimcomember 39090	Partition with general 𝑅 (in addition to the member partition cf. mpet 39094 and mpet2 39095) implies equivalent comembers. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.)
⊢ (𝑅 Part 𝐴 → CoMembEr 𝐴)
Theorem	mpet3 39091	Member Partition-Equivalence Theorem. Together with mpet 39094 mpet2 39095, mostly in its conventional cpet 39093 and cpet2 39092 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 39105 with general 𝑅). (Contributed by Peter Mazsa, 4-May-2018.) (Revised by Peter Mazsa, 26-Sep-2021.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	cpet2 39092	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 39093. Together with cpet 39093, mpet 39094 mpet2 39095, this is what we used to think of as the partition equivalence theorem (but cf. pet2 39105 with general 𝑅). (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	cpet 39093	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 39092. Cf. mpet 39094, mpet2 39095 and mpet3 39091 for unconventional forms of Member Partition-Equivalence Theorem. Cf. pet 39106 and pet2 39105 for Partition-Equivalence Theorem with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	mpet 39094	Member Partition-Equivalence Theorem in almost its shortest possible form, cf. the 0-ary version mpets 39097. 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 39095, mpet3 39091, and with the conventional cpet 39093 and cpet2 39092, this is what we used to think of as the partition equivalence theorem (but cf. pet2 39105 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴)
Theorem	mpet2 39095	Member Partition-Equivalence Theorem in a shorter form. Together with mpet 39094 mpet3 39091, mostly in its conventional cpet 39093 and cpet2 39092 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 39105 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ ((◡ E ↾ 𝐴) Part 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)
Theorem	mpets2 39096	Member Partition-Equivalence Theorem with binary relations, cf. mpet2 39095. (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) Parts 𝐴 ↔ ≀ (◡ E ↾ 𝐴) Ers 𝐴))
Theorem	mpets 39097	Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet 39106, the Partition-Equivalence Theorem, with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ MembParts = CoMembErs
Theorem	mainpart 39098	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 39099	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet 39094) generate a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → MembPart 𝐴)
Theorem	fences2 39100	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet3 39091) generate a partition of the members, it alo means that (𝑅 ErALTV 𝐴 → ElDisj 𝐴) and that (𝑅 ErALTV 𝐴 → ¬ ∅ ∈ 𝐴). (Contributed by Peter Mazsa, 15-Oct-2021.)
⊢ (𝑅 ErALTV 𝐴 → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))