![]() |
Metamath
Proof Explorer Theorem List (p. 380 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eldisjsdisj 37901 | 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 37902 | Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs )) | ||
Theorem | eleldisjseldisj 37903 | 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 37904 | Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.) |
⊢ ( Disj 𝑅 → Rel 𝑅) | ||
Theorem | disjss 37905 | Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjssi 37906 | Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( Disj 𝐵 → Disj 𝐴) | ||
Theorem | disjssd 37907 | Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjeq 37908 | Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjeqi 37909 | Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( Disj 𝐴 ↔ Disj 𝐵) | ||
Theorem | disjeqd 37910 | Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjdmqseqeq1 37911 | Lemma for the equality theorem for partition parteq1 37948. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴))) | ||
Theorem | eldisjss 37912 | Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjssi 37913 | Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( ElDisj 𝐵 → ElDisj 𝐴) | ||
Theorem | eldisjssd 37914 | Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjeq 37915 | Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | eldisjeqi 37916 | Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵) | ||
Theorem | eldisjeqd 37917 | Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | disjres 37918* | Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023.) |
⊢ (Rel 𝑅 → ( Disj (𝑅 ↾ 𝐴) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅))) | ||
Theorem | eldisjn0elb 37919 | 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 37920 | 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 37921* | Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023.) |
⊢ ( Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ 𝑆) ∩ [𝑣](𝑅 ⋉ 𝑆)) = ∅)) | ||
Theorem | disjorimxrn 37922 | 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 37923 | Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆)) | ||
Theorem | disjimres 37924 | Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴)) | ||
Theorem | disjimin 37925 | Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆)) | ||
Theorem | disjiminres 37926 | Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴))) | ||
Theorem | disjimxrnres 37927 | Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴))) | ||
Theorem | disjALTV0 37928 | The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ Disj ∅ | ||
Theorem | disjALTVid 37929 | The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.) |
⊢ Disj I | ||
Theorem | disjALTVidres 37930 | 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 37931 | The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴)) | ||
Theorem | disjALTVxrnidres 37932 | 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 37933* | Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023.) |
⊢ (𝐴 ∈ 𝑉 → ( Disj (𝑅 ⋉ (◡ E ↾ suc 𝐴)) ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))) | ||
Definition | df-antisymrel 37934 | Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.) |
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅)) | ||
Theorem | dfantisymrel4 37935 | Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.) |
⊢ ( AntisymRel 𝑅 ↔ ((𝑅 ∩ ◡𝑅) ⊆ I ∧ Rel 𝑅)) | ||
Theorem | dfantisymrel5 37936* | Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.) |
⊢ ( AntisymRel 𝑅 ↔ (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
Theorem | antisymrelres 37937* | (Contributed by Peter Mazsa, 25-Jun-2024.) |
⊢ ( AntisymRel (𝑅 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) | ||
Theorem | antisymrelressn 37938 | (Contributed by Peter Mazsa, 29-Jun-2024.) |
⊢ AntisymRel (𝑅 ↾ {𝐴}) | ||
Definition | df-parts 37939 |
Define the class of all partitions, cf. the comment of df-disjs 37878.
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 ) is what we call membership partition here, cf. dfmembpart2 37944. The binary partitions relation and the partition predicate are the same, that is, (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴) if 𝐴 and 𝑅 are sets, cf. brpartspart 37947. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ Parts = ( DomainQss ↾ Disjs ) | ||
Definition | df-part 37940 | Define the partition predicate (read: 𝐴 is a partition by 𝑅). Alternative definition is dfpart2 37943. The binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets, cf. brpartspart 37947. (Contributed by Peter Mazsa, 12-Aug-2021.) |
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴)) | ||
Definition | df-membparts 37941 | Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎} | ||
Definition | df-membpart 37942 |
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 37944.
Member partition is the conventional meaning of partition (see the notes of df-parts 37939 and dfmembpart2 37944), we generalize the concept in df-parts 37939 and df-part 37940. Member partition and comember equivalence are the same by mpet 38013. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴) | ||
Theorem | dfpart2 37943 | Alternate definition of the partition predicate. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) | ||
Theorem | dfmembpart2 37944 | 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 37945 | Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴))) | ||
Theorem | brparts2 37946 | Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ (dom 𝑅 / 𝑅) = 𝐴))) | ||
Theorem | brpartspart 37947 | Binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴)) | ||
Theorem | parteq1 37948 | Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝑅 = 𝑆 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)) | ||
Theorem | parteq2 37949 | Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.) |
⊢ (𝐴 = 𝐵 → (𝑅 Part 𝐴 ↔ 𝑅 Part 𝐵)) | ||
Theorem | parteq12 37950 | Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐵)) | ||
Theorem | parteq1i 37951 | Equality theorem for partition, inference version. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴) | ||
Theorem | parteq1d 37952 | Equality theorem for partition, deduction version. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)) | ||
Theorem | partsuc2 37953 | Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024.) |
⊢ (((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) Part ((𝐴 ∪ {𝐴}) ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴) | ||
Theorem | partsuc 37954 | Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024.) |
⊢ (((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) Part (suc 𝐴 ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴) | ||
Theorem | disjim 37955 | The "Divide et Aequivalere" Theorem: every disjoint relation generates equivalent cosets by the relation: generalization of the former prter1 38053, cf. eldisjim 37958. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 17-Sep-2021.) |
⊢ ( Disj 𝑅 → EqvRel ≀ 𝑅) | ||
Theorem | disjimi 37956 | Every disjoint relation generates equivalent cosets by the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.) |
⊢ Disj 𝑅 ⇒ ⊢ EqvRel ≀ 𝑅 | ||
Theorem | detlem 37957 | 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 37958 | If the elements of 𝐴 are disjoint, then it has equivalent coelements (former prter1 38053). Special case of disjim 37955. (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 37959 | Alternate form of eldisjim 37958. (Contributed by Peter Mazsa, 30-Dec-2024.) |
⊢ ( ElDisj 𝐴 → EqvRel ∼ 𝐴) | ||
Theorem | eqvrel0 37960 | The null class is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ EqvRel ∅ | ||
Theorem | det0 37961 | The cosets by the null class are in equivalence relation if and only if the null class is disjoint (which it is, see disjALTV0 37928). (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ( Disj ∅ ↔ EqvRel ≀ ∅) | ||
Theorem | eqvrelcoss0 37962 | The cosets by the null class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.) |
⊢ EqvRel ≀ ∅ | ||
Theorem | eqvrelid 37963 | 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 37964 | The cosets by a restricted identity relation is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ EqvRel ≀ ( I ↾ 𝐴) | ||
Theorem | eqvrel1cossinidres 37965 | 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 37966 | 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 37967 | 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 37968 | The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.) |
⊢ EqvRel ≀ I | ||
Theorem | detidres 37969 | 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 37970 | 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 37971 | 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 37972* | Lemma for disjdmqseq 37979, partim2 37981 and petlem 37986 via disjlem17 37973, (general version of the former prtlem14 38048). (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅) → ((𝐴 ∈ [𝑥]𝑅 ∧ 𝐴 ∈ [𝑦]𝑅) → [𝑥]𝑅 = [𝑦]𝑅))) | ||
Theorem | disjlem17 37973* | Lemma for disjdmqseq 37979, partim2 37981 and petlem 37986 via disjlem18 37974, (general version of the former prtlem17 38050). (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (∃𝑦 ∈ dom 𝑅(𝐴 ∈ [𝑦]𝑅 ∧ 𝐵 ∈ [𝑦]𝑅) → 𝐵 ∈ [𝑥]𝑅))) | ||
Theorem | disjlem18 37974* | Lemma for disjdmqseq 37979, partim2 37981 and petlem 37986 via disjlem19 37975, (general version of the former prtlem18 38051). (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (𝐵 ∈ [𝑥]𝑅 ↔ 𝐴 ≀ 𝑅𝐵)))) | ||
Theorem | disjlem19 37975* | Lemma for disjdmqseq 37979, partim2 37981 and petlem 37986 via disjdmqs 37978, (general version of the former prtlem19 38052). (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → [𝑥]𝑅 = [𝐴] ≀ 𝑅))) | ||
Theorem | disjdmqsss 37976 | Lemma for disjdmqseq 37979 via disjdmqs 37978. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) ⊆ (dom ≀ 𝑅 / ≀ 𝑅)) | ||
Theorem | disjdmqscossss 37977 | Lemma for disjdmqseq 37979 via disjdmqs 37978. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → (dom ≀ 𝑅 / ≀ 𝑅) ⊆ (dom 𝑅 / 𝑅)) | ||
Theorem | disjdmqs 37978 | If a relation is disjoint, its domain quotient is equal to the domain quotient of the cosets by it. Lemma for partim2 37981 and petlem 37986 via disjdmqseq 37979. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅)) | ||
Theorem | disjdmqseq 37979 | 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 37980 (which is the closest theorem to the former prter2 38055). Lemma for partim2 37981 and petlem 37986. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
Theorem | eldisjn0el 37980 | Special case of disjdmqseq 37979 (perhaps this is the closest theorem to the former prter2 38055). (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ ( ElDisj 𝐴 → (¬ ∅ ∈ 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | partim2 37981 | Disjoint relation on its natural domain implies an equivalence relation on the cosets of the relation, on its natural domain, cf. partim 37982. Lemma for petlem 37986. (Contributed by Peter Mazsa, 17-Sep-2021.) |
⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
Theorem | partim 37982 | Partition implies equivalence relation by the cosets of the relation on its natural domain, cf. partim2 37981. (Contributed by Peter Mazsa, 17-Sep-2021.) |
⊢ (𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴) | ||
Theorem | partimeq 37983 | Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq 37853. (Contributed by Peter Mazsa, 25-Dec-2024.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅)) | ||
Theorem | eldisjlem19 37984* | Special case of disjlem19 37975 (together with membpartlem19 37985, this is former prtlem19 38052). (Contributed by Peter Mazsa, 21-Oct-2021.) |
⊢ (𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ((𝑢 ∈ dom (◡ E ↾ 𝐴) ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴))) | ||
Theorem | membpartlem19 37985* | Together with disjlem19 37975, this is former prtlem19 38052. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 21-Oct-2021.) |
⊢ (𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ((𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴))) | ||
Theorem | petlem 37986 | If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 38007), or converse function (cf. dfdisjALTV 37887), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 38024. (Contributed by Peter Mazsa, 18-Sep-2021.) |
⊢ (( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴) → Disj 𝑅) ⇒ ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
Theorem | petlemi 37987 | If you can prove disjointness (e.g. disjALTV0 37928, disjALTVid 37929, disjALTVidres 37930, disjALTVxrnidres 37932, search for theorems containing the ' |- Disj ' string), or the same with converse function (cf. dfdisjALTV 37887), 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 37988 | 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 37989 | 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 37990 | 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 37991 | 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 37992 | 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 37993 | 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 37964. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ (( I ↾ 𝐴) Part 𝐴 ↔ ≀ ( I ↾ 𝐴) ErALTV 𝐴) | ||
Theorem | petinidres2 37994 | 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 37995 | 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 37623, disjALTVinidres 37931 and eqvrel1cossinidres 37965. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ((𝑅 ∩ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ ( I ↾ 𝐴)) ErALTV 𝐴) | ||
Theorem | petxrnidres2 37996 | 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 37997 | 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 37625, disjALTVxrnidres 37932 and eqvrel1cossxrnidres 37966. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ((𝑅 ⋉ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ErALTV 𝐴) | ||
Theorem | eqvreldisj1 37998* | The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj2 37999, eqvreldisj3 38000). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 3-Dec-2024.) |
⊢ ( EqvRel 𝑅 → ∀𝑥 ∈ (𝐴 / 𝑅)∀𝑦 ∈ (𝐴 / 𝑅)(𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | ||
Theorem | eqvreldisj2 37999 | The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj3 38000). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 19-Sep-2021.) |
⊢ ( EqvRel 𝑅 → ElDisj (𝐴 / 𝑅)) | ||
Theorem | eqvreldisj3 38000 | The elements of the quotient set of an equivalence relation are disjoint (cf. qsdisj2 8792). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 20-Jun-2019.) (Revised by Peter Mazsa, 19-Sep-2021.) |
⊢ ( EqvRel 𝑅 → Disj (◡ E ↾ (𝐴 / 𝑅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |