![]() |
Metamath
Proof Explorer Theorem List (p. 388 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfeldisj4 38701* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢) | ||
Theorem | dfeldisj5 38702* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅)) | ||
Theorem | eldisjs 38703 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs2 38704 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs3 38705* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs4 38706* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs5 38707* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels ))) | ||
Theorem | eldisjsdisj 38708 | 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 38709 | Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs )) | ||
Theorem | eleldisjseldisj 38710 | 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 38711 | Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.) |
⊢ ( Disj 𝑅 → Rel 𝑅) | ||
Theorem | disjss 38712 | Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjssi 38713 | Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( Disj 𝐵 → Disj 𝐴) | ||
Theorem | disjssd 38714 | Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjeq 38715 | Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjeqi 38716 | Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( Disj 𝐴 ↔ Disj 𝐵) | ||
Theorem | disjeqd 38717 | Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjdmqseqeq1 38718 | Lemma for the equality theorem for partition parteq1 38755. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴))) | ||
Theorem | eldisjss 38719 | Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjssi 38720 | Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( ElDisj 𝐵 → ElDisj 𝐴) | ||
Theorem | eldisjssd 38721 | Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjeq 38722 | Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | eldisjeqi 38723 | Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵) | ||
Theorem | eldisjeqd 38724 | Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | disjres 38725* | Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023.) |
⊢ (Rel 𝑅 → ( Disj (𝑅 ↾ 𝐴) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅))) | ||
Theorem | eldisjn0elb 38726 | 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 38727 | 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 38728* | Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023.) |
⊢ ( Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ 𝑆) ∩ [𝑣](𝑅 ⋉ 𝑆)) = ∅)) | ||
Theorem | disjorimxrn 38729 | 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 38730 | Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆)) | ||
Theorem | disjimres 38731 | Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴)) | ||
Theorem | disjimin 38732 | Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆)) | ||
Theorem | disjiminres 38733 | Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴))) | ||
Theorem | disjimxrnres 38734 | Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴))) | ||
Theorem | disjALTV0 38735 | The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ Disj ∅ | ||
Theorem | disjALTVid 38736 | The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.) |
⊢ Disj I | ||
Theorem | disjALTVidres 38737 | 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 38738 | The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴)) | ||
Theorem | disjALTVxrnidres 38739 | 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 38740* | Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023.) |
⊢ (𝐴 ∈ 𝑉 → ( Disj (𝑅 ⋉ (◡ E ↾ suc 𝐴)) ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))) | ||
Definition | df-antisymrel 38741 | Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.) |
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅)) | ||
Theorem | dfantisymrel4 38742 | Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.) |
⊢ ( AntisymRel 𝑅 ↔ ((𝑅 ∩ ◡𝑅) ⊆ I ∧ Rel 𝑅)) | ||
Theorem | dfantisymrel5 38743* | Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.) |
⊢ ( AntisymRel 𝑅 ↔ (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
Theorem | antisymrelres 38744* | (Contributed by Peter Mazsa, 25-Jun-2024.) |
⊢ ( AntisymRel (𝑅 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) | ||
Theorem | antisymrelressn 38745 | (Contributed by Peter Mazsa, 29-Jun-2024.) |
⊢ AntisymRel (𝑅 ↾ {𝐴}) | ||
Definition | df-parts 38746 |
Define the class of all partitions, cf. the comment of df-disjs 38685.
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 38685) is what we call membership partition here, cf. dfmembpart2 38751. The binary partitions relation and the partition predicate are the same, that is, (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴) if 𝐴 and 𝑅 are sets, cf. brpartspart 38754. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ Parts = ( DomainQss ↾ Disjs ) | ||
Definition | df-part 38747 | Define the partition predicate (read: 𝐴 is a partition by 𝑅). Alternative definition is dfpart2 38750. The binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets, cf. brpartspart 38754. (Contributed by Peter Mazsa, 12-Aug-2021.) |
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴)) | ||
Definition | df-membparts 38748 | Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎} | ||
Definition | df-membpart 38749 |
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 38751.
Member partition is the conventional meaning of partition (see the notes of df-parts 38746 and dfmembpart2 38751), we generalize the concept in df-parts 38746 and df-part 38747. Member partition and comember equivalence are the same by mpet 38820. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴) | ||
Theorem | dfpart2 38750 | Alternate definition of the partition predicate. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) | ||
Theorem | dfmembpart2 38751 | 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 38752 | Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴))) | ||
Theorem | brparts2 38753 | Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ (dom 𝑅 / 𝑅) = 𝐴))) | ||
Theorem | brpartspart 38754 | Binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴)) | ||
Theorem | parteq1 38755 | Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝑅 = 𝑆 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)) | ||
Theorem | parteq2 38756 | Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.) |
⊢ (𝐴 = 𝐵 → (𝑅 Part 𝐴 ↔ 𝑅 Part 𝐵)) | ||
Theorem | parteq12 38757 | Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐵)) | ||
Theorem | parteq1i 38758 | Equality theorem for partition, inference version. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴) | ||
Theorem | parteq1d 38759 | Equality theorem for partition, deduction version. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)) | ||
Theorem | partsuc2 38760 | Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024.) |
⊢ (((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) Part ((𝐴 ∪ {𝐴}) ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴) | ||
Theorem | partsuc 38761 | Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024.) |
⊢ (((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) Part (suc 𝐴 ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴) | ||
Theorem | disjim 38762 | The "Divide et Aequivalere" Theorem: every disjoint relation generates equivalent cosets by the relation: generalization of the former prter1 38860, cf. eldisjim 38765. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 17-Sep-2021.) |
⊢ ( Disj 𝑅 → EqvRel ≀ 𝑅) | ||
Theorem | disjimi 38763 | Every disjoint relation generates equivalent cosets by the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.) |
⊢ Disj 𝑅 ⇒ ⊢ EqvRel ≀ 𝑅 | ||
Theorem | detlem 38764 | 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 38765 | If the elements of 𝐴 are disjoint, then it has equivalent coelements (former prter1 38860). Special case of disjim 38762. (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 38766 | Alternate form of eldisjim 38765. (Contributed by Peter Mazsa, 30-Dec-2024.) |
⊢ ( ElDisj 𝐴 → EqvRel ∼ 𝐴) | ||
Theorem | eqvrel0 38767 | The null class is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ EqvRel ∅ | ||
Theorem | det0 38768 | The cosets by the null class are in equivalence relation if and only if the null class is disjoint (which it is, see disjALTV0 38735). (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ( Disj ∅ ↔ EqvRel ≀ ∅) | ||
Theorem | eqvrelcoss0 38769 | The cosets by the null class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.) |
⊢ EqvRel ≀ ∅ | ||
Theorem | eqvrelid 38770 | 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 38771 | The cosets by a restricted identity relation is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ EqvRel ≀ ( I ↾ 𝐴) | ||
Theorem | eqvrel1cossinidres 38772 | 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 38773 | 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 38774 | 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 38775 | The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.) |
⊢ EqvRel ≀ I | ||
Theorem | detidres 38776 | 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 38777 | 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 38778 | 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 38779* | Lemma for disjdmqseq 38786, partim2 38788 and petlem 38793 via disjlem17 38780, (general version of the former prtlem14 38855). (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅) → ((𝐴 ∈ [𝑥]𝑅 ∧ 𝐴 ∈ [𝑦]𝑅) → [𝑥]𝑅 = [𝑦]𝑅))) | ||
Theorem | disjlem17 38780* | Lemma for disjdmqseq 38786, partim2 38788 and petlem 38793 via disjlem18 38781, (general version of the former prtlem17 38857). (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (∃𝑦 ∈ dom 𝑅(𝐴 ∈ [𝑦]𝑅 ∧ 𝐵 ∈ [𝑦]𝑅) → 𝐵 ∈ [𝑥]𝑅))) | ||
Theorem | disjlem18 38781* | Lemma for disjdmqseq 38786, partim2 38788 and petlem 38793 via disjlem19 38782, (general version of the former prtlem18 38858). (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (𝐵 ∈ [𝑥]𝑅 ↔ 𝐴 ≀ 𝑅𝐵)))) | ||
Theorem | disjlem19 38782* | Lemma for disjdmqseq 38786, partim2 38788 and petlem 38793 via disjdmqs 38785, (general version of the former prtlem19 38859). (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → [𝑥]𝑅 = [𝐴] ≀ 𝑅))) | ||
Theorem | disjdmqsss 38783 | Lemma for disjdmqseq 38786 via disjdmqs 38785. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) ⊆ (dom ≀ 𝑅 / ≀ 𝑅)) | ||
Theorem | disjdmqscossss 38784 | Lemma for disjdmqseq 38786 via disjdmqs 38785. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → (dom ≀ 𝑅 / ≀ 𝑅) ⊆ (dom 𝑅 / 𝑅)) | ||
Theorem | disjdmqs 38785 | If a relation is disjoint, its domain quotient is equal to the domain quotient of the cosets by it. Lemma for partim2 38788 and petlem 38793 via disjdmqseq 38786. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅)) | ||
Theorem | disjdmqseq 38786 | 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 38787 (which is the closest theorem to the former prter2 38862). Lemma for partim2 38788 and petlem 38793. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
Theorem | eldisjn0el 38787 | Special case of disjdmqseq 38786 (perhaps this is the closest theorem to the former prter2 38862). (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ ( ElDisj 𝐴 → (¬ ∅ ∈ 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | partim2 38788 | Disjoint relation on its natural domain implies an equivalence relation on the cosets of the relation, on its natural domain, cf. partim 38789. Lemma for petlem 38793. (Contributed by Peter Mazsa, 17-Sep-2021.) |
⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
Theorem | partim 38789 | Partition implies equivalence relation by the cosets of the relation on its natural domain, cf. partim2 38788. (Contributed by Peter Mazsa, 17-Sep-2021.) |
⊢ (𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴) | ||
Theorem | partimeq 38790 | Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq 38660. (Contributed by Peter Mazsa, 25-Dec-2024.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅)) | ||
Theorem | eldisjlem19 38791* | Special case of disjlem19 38782 (together with membpartlem19 38792, this is former prtlem19 38859). (Contributed by Peter Mazsa, 21-Oct-2021.) |
⊢ (𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ((𝑢 ∈ dom (◡ E ↾ 𝐴) ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴))) | ||
Theorem | membpartlem19 38792* | Together with disjlem19 38782, this is former prtlem19 38859. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 21-Oct-2021.) |
⊢ (𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ((𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴))) | ||
Theorem | petlem 38793 | If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 38814), or converse function (cf. dfdisjALTV 38694), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 38831. (Contributed by Peter Mazsa, 18-Sep-2021.) |
⊢ (( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴) → Disj 𝑅) ⇒ ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
Theorem | petlemi 38794 | If you can prove disjointness (e.g. disjALTV0 38735, disjALTVid 38736, disjALTVidres 38737, disjALTVxrnidres 38739, search for theorems containing the ' |- Disj ' string), or the same with converse function (cf. dfdisjALTV 38694), 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 38795 | 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 38796 | 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 38797 | 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 38798 | 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 38799 | 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 38800 | 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 38771. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ (( I ↾ 𝐴) Part 𝐴 ↔ ≀ ( I ↾ 𝐴) ErALTV 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |