![]() |
Metamath
Proof Explorer Theorem List (p. 373 of 473) | < 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-29858) |
![]() (29859-31381) |
![]() (31382-47224) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | disjorimxrn 37201 | 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 37202 | Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆)) | ||
Theorem | disjimres 37203 | Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴)) | ||
Theorem | disjimin 37204 | Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆)) | ||
Theorem | disjiminres 37205 | Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴))) | ||
Theorem | disjimxrnres 37206 | Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴))) | ||
Theorem | disjALTV0 37207 | The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ Disj ∅ | ||
Theorem | disjALTVid 37208 | The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.) |
⊢ Disj I | ||
Theorem | disjALTVidres 37209 | 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 37210 | The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴)) | ||
Theorem | disjALTVxrnidres 37211 | 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 37212* | Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023.) |
⊢ (𝐴 ∈ 𝑉 → ( Disj (𝑅 ⋉ (◡ E ↾ suc 𝐴)) ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))) | ||
Definition | df-antisymrel 37213 | Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.) |
⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅)) | ||
Theorem | dfantisymrel4 37214 | Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.) |
⊢ ( AntisymRel 𝑅 ↔ ((𝑅 ∩ ◡𝑅) ⊆ I ∧ Rel 𝑅)) | ||
Theorem | dfantisymrel5 37215* | Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.) |
⊢ ( AntisymRel 𝑅 ↔ (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
Theorem | antisymrelres 37216* | (Contributed by Peter Mazsa, 25-Jun-2024.) |
⊢ ( AntisymRel (𝑅 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) | ||
Theorem | antisymrelressn 37217 | (Contributed by Peter Mazsa, 29-Jun-2024.) |
⊢ AntisymRel (𝑅 ↾ {𝐴}) | ||
Definition | df-parts 37218 |
Define the class of all partitions, cf. the comment of df-disjs 37157.
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 37223. The binary partitions relation and the partition predicate are the same, that is, (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴) if 𝐴 and 𝑅 are sets, cf. brpartspart 37226. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ Parts = ( DomainQss ↾ Disjs ) | ||
Definition | df-part 37219 | Define the partition predicate (read: 𝐴 is a partition by 𝑅). Alternative definition is dfpart2 37222. The binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets, cf. brpartspart 37226. (Contributed by Peter Mazsa, 12-Aug-2021.) |
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴)) | ||
Definition | df-membparts 37220 | Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎} | ||
Definition | df-membpart 37221 |
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 37223.
Member partition is the conventional meaning of partition (see the notes of df-parts 37218 and dfmembpart2 37223), we generalize the concept in df-parts 37218 and df-part 37219. Member partition and comember equivalence are the same by mpet 37292. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴) | ||
Theorem | dfpart2 37222 | Alternate definition of the partition predicate. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) | ||
Theorem | dfmembpart2 37223 | 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 37224 | Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴))) | ||
Theorem | brparts2 37225 | Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ (dom 𝑅 / 𝑅) = 𝐴))) | ||
Theorem | brpartspart 37226 | Binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴)) | ||
Theorem | parteq1 37227 | Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝑅 = 𝑆 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)) | ||
Theorem | parteq2 37228 | Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.) |
⊢ (𝐴 = 𝐵 → (𝑅 Part 𝐴 ↔ 𝑅 Part 𝐵)) | ||
Theorem | parteq12 37229 | Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐵)) | ||
Theorem | parteq1i 37230 | Equality theorem for partition, inference version. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴) | ||
Theorem | parteq1d 37231 | Equality theorem for partition, deduction version. (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)) | ||
Theorem | partsuc2 37232 | Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024.) |
⊢ (((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) Part ((𝐴 ∪ {𝐴}) ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴) | ||
Theorem | partsuc 37233 | Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024.) |
⊢ (((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) Part (suc 𝐴 ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴) | ||
Theorem | disjim 37234 | The "Divide et Aequivalere" Theorem: every disjoint relation generates equivalent cosets by the relation: generalization of the former prter1 37332, cf. eldisjim 37237. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 17-Sep-2021.) |
⊢ ( Disj 𝑅 → EqvRel ≀ 𝑅) | ||
Theorem | disjimi 37235 | Every disjoint relation generates equivalent cosets by the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.) |
⊢ Disj 𝑅 ⇒ ⊢ EqvRel ≀ 𝑅 | ||
Theorem | detlem 37236 | 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 37237 | If the elements of 𝐴 are disjoint, then it has equivalent coelements (former prter1 37332). Special case of disjim 37234. (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 37238 | Alternate form of eldisjim 37237. (Contributed by Peter Mazsa, 30-Dec-2024.) |
⊢ ( ElDisj 𝐴 → EqvRel ∼ 𝐴) | ||
Theorem | eqvrel0 37239 | The null class is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ EqvRel ∅ | ||
Theorem | det0 37240 | The cosets by the null class are in equivalence relation if and only if the null class is disjoint (which it is, see disjALTV0 37207). (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ( Disj ∅ ↔ EqvRel ≀ ∅) | ||
Theorem | eqvrelcoss0 37241 | The cosets by the null class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.) |
⊢ EqvRel ≀ ∅ | ||
Theorem | eqvrelid 37242 | 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 37243 | The cosets by a restricted identity relation is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ EqvRel ≀ ( I ↾ 𝐴) | ||
Theorem | eqvrel1cossinidres 37244 | 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 37245 | 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 37246 | 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 37247 | The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.) |
⊢ EqvRel ≀ I | ||
Theorem | detidres 37248 | 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 37249 | 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 37250 | 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 37251* | Lemma for disjdmqseq 37258, partim2 37260 and petlem 37265 via disjlem17 37252, (general version of the former prtlem14 37327). (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅) → ((𝐴 ∈ [𝑥]𝑅 ∧ 𝐴 ∈ [𝑦]𝑅) → [𝑥]𝑅 = [𝑦]𝑅))) | ||
Theorem | disjlem17 37252* | Lemma for disjdmqseq 37258, partim2 37260 and petlem 37265 via disjlem18 37253, (general version of the former prtlem17 37329). (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (∃𝑦 ∈ dom 𝑅(𝐴 ∈ [𝑦]𝑅 ∧ 𝐵 ∈ [𝑦]𝑅) → 𝐵 ∈ [𝑥]𝑅))) | ||
Theorem | disjlem18 37253* | Lemma for disjdmqseq 37258, partim2 37260 and petlem 37265 via disjlem19 37254, (general version of the former prtlem18 37330). (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (𝐵 ∈ [𝑥]𝑅 ↔ 𝐴 ≀ 𝑅𝐵)))) | ||
Theorem | disjlem19 37254* | Lemma for disjdmqseq 37258, partim2 37260 and petlem 37265 via disjdmqs 37257, (general version of the former prtlem19 37331). (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → [𝑥]𝑅 = [𝐴] ≀ 𝑅))) | ||
Theorem | disjdmqsss 37255 | Lemma for disjdmqseq 37258 via disjdmqs 37257. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) ⊆ (dom ≀ 𝑅 / ≀ 𝑅)) | ||
Theorem | disjdmqscossss 37256 | Lemma for disjdmqseq 37258 via disjdmqs 37257. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → (dom ≀ 𝑅 / ≀ 𝑅) ⊆ (dom 𝑅 / 𝑅)) | ||
Theorem | disjdmqs 37257 | If a relation is disjoint, its domain quotient is equal to the domain quotient of the cosets by it. Lemma for partim2 37260 and petlem 37265 via disjdmqseq 37258. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅)) | ||
Theorem | disjdmqseq 37258 | 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 37259 (which is the closest theorem to the former prter2 37334). Lemma for partim2 37260 and petlem 37265. (Contributed by Peter Mazsa, 16-Sep-2021.) |
⊢ ( Disj 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
Theorem | eldisjn0el 37259 | Special case of disjdmqseq 37258 (perhaps this is the closest theorem to the former prter2 37334). (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ ( ElDisj 𝐴 → (¬ ∅ ∈ 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | partim2 37260 | Disjoint relation on its natural domain implies an equivalence relation on the cosets of the relation, on its natural domain, cf. partim 37261. Lemma for petlem 37265. (Contributed by Peter Mazsa, 17-Sep-2021.) |
⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
Theorem | partim 37261 | Partition implies equivalence relation by the cosets of the relation on its natural domain, cf. partim2 37260. (Contributed by Peter Mazsa, 17-Sep-2021.) |
⊢ (𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴) | ||
Theorem | partimeq 37262 | Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq 37132. (Contributed by Peter Mazsa, 25-Dec-2024.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅)) | ||
Theorem | eldisjlem19 37263* | Special case of disjlem19 37254 (together with membpartlem19 37264, this is former prtlem19 37331). (Contributed by Peter Mazsa, 21-Oct-2021.) |
⊢ (𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ((𝑢 ∈ dom (◡ E ↾ 𝐴) ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴))) | ||
Theorem | membpartlem19 37264* | Together with disjlem19 37254, this is former prtlem19 37331. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 21-Oct-2021.) |
⊢ (𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ((𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴))) | ||
Theorem | petlem 37265 | If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 37286), or converse function (cf. dfdisjALTV 37166), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 37303. (Contributed by Peter Mazsa, 18-Sep-2021.) |
⊢ (( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴) → Disj 𝑅) ⇒ ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴)) | ||
Theorem | petlemi 37266 | If you can prove disjointness (e.g. disjALTV0 37207, disjALTVid 37208, disjALTVidres 37209, disjALTVxrnidres 37211, search for theorems containing the ' |- Disj ' string), or the same with converse function (cf. dfdisjALTV 37166), 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 37267 | 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 37268 | 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 37269 | 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 37270 | 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 37271 | 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 37272 | 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 37243. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ (( I ↾ 𝐴) Part 𝐴 ↔ ≀ ( I ↾ 𝐴) ErALTV 𝐴) | ||
Theorem | petinidres2 37273 | 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 37274 | 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 36902, disjALTVinidres 37210 and eqvrel1cossinidres 37244. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ((𝑅 ∩ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ ( I ↾ 𝐴)) ErALTV 𝐴) | ||
Theorem | petxrnidres2 37275 | 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 37276 | 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 36904, disjALTVxrnidres 37211 and eqvrel1cossxrnidres 37245. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ ((𝑅 ⋉ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ErALTV 𝐴) | ||
Theorem | eqvreldisj1 37277* | The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj2 37278, eqvreldisj3 37279). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 3-Dec-2024.) |
⊢ ( EqvRel 𝑅 → ∀𝑥 ∈ (𝐴 / 𝑅)∀𝑦 ∈ (𝐴 / 𝑅)(𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | ||
Theorem | eqvreldisj2 37278 | The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj3 37279). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 19-Sep-2021.) |
⊢ ( EqvRel 𝑅 → ElDisj (𝐴 / 𝑅)) | ||
Theorem | eqvreldisj3 37279 | The elements of the quotient set of an equivalence relation are disjoint (cf. qsdisj2 8733). (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 37280 | 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 37281 | 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 37282 | Implication of eqvreldisj2 37278, lemma for The Main Theorem of Equivalences mainer 37287. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → ElDisj 𝐴) | ||
Theorem | fences3 37283 | Implication of eqvrelqseqdisj2 37282 and n0eldmqseq 37102, see comment of fences 37297. (Contributed by Peter Mazsa, 30-Dec-2024.) |
⊢ (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴)) | ||
Theorem | eqvrelqseqdisj3 37284 | Implication of eqvreldisj3 37279, lemma for the Member Partition Equivalence Theorem mpet3 37289. (Contributed by Peter Mazsa, 27-Oct-2020.) (Revised by Peter Mazsa, 24-Sep-2021.) |
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (◡ E ↾ 𝐴)) | ||
Theorem | eqvrelqseqdisj4 37285 | Lemma for petincnvepres2 37301. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ∩ (◡ E ↾ 𝐴))) | ||
Theorem | eqvrelqseqdisj5 37286 | Lemma for the Partition-Equivalence Theorem pet2 37303. (Contributed by Peter Mazsa, 15-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ⋉ (◡ E ↾ 𝐴))) | ||
Theorem | mainer 37287 | The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ (𝑅 ErALTV 𝐴 → CoMembEr 𝐴) | ||
Theorem | partimcomember 37288 | Partition with general 𝑅 (in addition to the member partition cf. mpet 37292 and mpet2 37293) implies equivalent comembers. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.) |
⊢ (𝑅 Part 𝐴 → CoMembEr 𝐴) | ||
Theorem | mpet3 37289 | Member Partition-Equivalence Theorem. Together with mpet 37292 mpet2 37293, mostly in its conventional cpet 37291 and cpet2 37290 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 37303 with general 𝑅). (Contributed by Peter Mazsa, 4-May-2018.) (Revised by Peter Mazsa, 26-Sep-2021.) |
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | cpet2 37290 | 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 37291. Together with cpet 37291, mpet 37292 mpet2 37293, this is what we used to think of as the partition equivalence theorem (but cf. pet2 37303 with general 𝑅). (Contributed by Peter Mazsa, 30-Dec-2024.) |
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | cpet 37291 | 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 37290. Cf. mpet 37292, mpet2 37293 and mpet3 37289 for unconventional forms of Member Partition-Equivalence Theorem. Cf. pet 37304 and pet2 37303 for Partition-Equivalence Theorem with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.) |
⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | mpet 37292 | Member Partition-Equivalence Theorem in almost its shortest possible form, cf. the 0-ary version mpets 37295. 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 37293, mpet3 37289, and with the conventional cpet 37291 and cpet2 37290, this is what we used to think of as the partition equivalence theorem (but cf. pet2 37303 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.) |
⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴) | ||
Theorem | mpet2 37293 | Member Partition-Equivalence Theorem in a shorter form. Together with mpet 37292 mpet3 37289, mostly in its conventional cpet 37291 and cpet2 37290 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 37303 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.) |
⊢ ((◡ E ↾ 𝐴) Part 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴) | ||
Theorem | mpets2 37294 | Member Partition-Equivalence Theorem with binary relations, cf. mpet2 37293. (Contributed by Peter Mazsa, 24-Sep-2021.) |
⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) Parts 𝐴 ↔ ≀ (◡ E ↾ 𝐴) Ers 𝐴)) | ||
Theorem | mpets 37295 | Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet 37304, the Partition-Equivalence Theorem, with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.) |
⊢ MembParts = CoMembErs | ||
Theorem | mainpart 37296 | 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 37297 | The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet 37292) generate a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ (𝑅 ErALTV 𝐴 → MembPart 𝐴) | ||
Theorem | fences2 37298 | The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet3 37289) generate a partition of the members, it alo means that (𝑅 ErALTV 𝐴 → ElDisj 𝐴) and that (𝑅 ErALTV 𝐴 → ¬ ∅ ∈ 𝐴). (Contributed by Peter Mazsa, 15-Oct-2021.) |
⊢ (𝑅 ErALTV 𝐴 → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴)) | ||
Theorem | mainer2 37299 | The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 15-Oct-2021.) |
⊢ (𝑅 ErALTV 𝐴 → ( CoElEqvRel 𝐴 ∧ ¬ ∅ ∈ 𝐴)) | ||
Theorem | mainerim 37300 | Every equivalence relation implies equivalent coelements. (Contributed by Peter Mazsa, 20-Oct-2021.) |
⊢ (𝑅 ErALTV 𝐴 → CoElEqvRel 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |