| Metamath
Proof Explorer Theorem List (p. 388 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | funALTVeq 38701 | Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
| ⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
| Theorem | funALTVeqi 38702 | Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵) | ||
| Theorem | funALTVeqd 38703 | Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
| Definition | df-disjss 38704 | Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 38705). It is used only by df-disjs 38705. (Contributed by Peter Mazsa, 17-Jul-2021.) |
| ⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } | ||
| Definition | df-disjs 38705 |
Define the disjoint relations class, i.e., the class of disjoints. We
need Disjs for the definition of Parts and Part
for the
Partition-Equivalence Theorems: this need for Parts as disjoint relations
on their domain quotients is the reason why we must define Disjs
instead of simply using converse functions (cf. dfdisjALTV 38714).
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 38728. Alternate definitions are dfdisjs 38709, ... , dfdisjs5 38713. (Contributed by Peter Mazsa, 17-Jul-2021.) |
| ⊢ Disjs = ( Disjss ∩ Rels ) | ||
| Definition | df-disjALTV 38706 |
Define the disjoint relation predicate, i.e., the disjoint predicate. A
disjoint relation is a converse function of the relation by dfdisjALTV 38714,
see the comment of df-disjs 38705 why we need disjoint relations instead of
converse functions anyway.
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 38728. Alternate definitions are dfdisjALTV 38714, ... , dfdisjALTV5 38718. (Contributed by Peter Mazsa, 17-Jul-2021.) |
| ⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅)) | ||
| Definition | df-eldisjs 38707 | Define the disjoint element relations class, i.e., the disjoint elements class. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set, see eleldisjseldisj 38730. (Contributed by Peter Mazsa, 28-Nov-2022.) |
| ⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs } | ||
| Definition | df-eldisj 38708 |
Define the disjoint element relation predicate, i.e., the disjoint
elementhood predicate. Read: the elements of 𝐴 are disjoint. The
element of the disjoint elements class and the disjoint elementhood
predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when
𝐴 is a set, see eleldisjseldisj 38730.
As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 38873 with dfeldisj5 38722. See also the comments of dfmembpart2 38771 and of df-parts 38766. (Contributed by Peter Mazsa, 17-Jul-2021.) |
| ⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴)) | ||
| Theorem | dfdisjs 38709 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.) |
| ⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels } | ||
| Theorem | dfdisjs2 38710 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I } | ||
| Theorem | dfdisjs3 38711* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)} | ||
| Theorem | dfdisjs4 38712* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥} | ||
| Theorem | dfdisjs5 38713* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)} | ||
| Theorem | dfdisjALTV 38714 | Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 38705 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.) |
| ⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅)) | ||
| Theorem | dfdisjALTV2 38715 | Alternate definition of the disjoint relation predicate, cf. dffunALTV2 38689. (Contributed by Peter Mazsa, 27-Jul-2021.) |
| ⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅)) | ||
| Theorem | dfdisjALTV3 38716* | Alternate definition of the disjoint relation predicate, cf. dffunALTV3 38690. (Contributed by Peter Mazsa, 28-Jul-2021.) |
| ⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅)) | ||
| Theorem | dfdisjALTV4 38717* | Alternate definition of the disjoint relation predicate, cf. dffunALTV4 38691. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ ( Disj 𝑅 ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅)) | ||
| Theorem | dfdisjALTV5 38718* | Alternate definition of the disjoint relation predicate, cf. dffunALTV5 38692. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅)) | ||
| Theorem | dfeldisj2 38719 | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
| ⊢ ( ElDisj 𝐴 ↔ ≀ ◡(◡ E ↾ 𝐴) ⊆ I ) | ||
| Theorem | dfeldisj3 38720* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
| ⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣) | ||
| Theorem | dfeldisj4 38721* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
| ⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢) | ||
| Theorem | dfeldisj5 38722* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
| ⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅)) | ||
| Theorem | eldisjs 38723 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.) |
| ⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels )) | ||
| Theorem | eldisjs2 38724 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels )) | ||
| Theorem | eldisjs3 38725* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels )) | ||
| Theorem | eldisjs4 38726* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels )) | ||
| Theorem | eldisjs5 38727* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels ))) | ||
| Theorem | eldisjsdisj 38728 | 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 38729 | Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs )) | ||
| Theorem | eleldisjseldisj 38730 | 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 38731 | Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.) |
| ⊢ ( Disj 𝑅 → Rel 𝑅) | ||
| Theorem | disjss 38732 | Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
| ⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴)) | ||
| Theorem | disjssi 38733 | Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
| ⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( Disj 𝐵 → Disj 𝐴) | ||
| Theorem | disjssd 38734 | Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴)) | ||
| Theorem | disjeq 38735 | Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.) |
| ⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
| Theorem | disjeqi 38736 | Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ( Disj 𝐴 ↔ Disj 𝐵) | ||
| Theorem | disjeqd 38737 | Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
| Theorem | disjdmqseqeq1 38738 | Lemma for the equality theorem for partition parteq1 38775. (Contributed by Peter Mazsa, 5-Oct-2021.) |
| ⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴))) | ||
| Theorem | eldisjss 38739 | Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
| Theorem | eldisjssi 38740 | Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
| ⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( ElDisj 𝐵 → ElDisj 𝐴) | ||
| Theorem | eldisjssd 38741 | Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
| Theorem | eldisjeq 38742 | Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
| Theorem | eldisjeqi 38743 | Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵) | ||
| Theorem | eldisjeqd 38744 | Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
| Theorem | disjres 38745* | Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023.) |
| ⊢ (Rel 𝑅 → ( Disj (𝑅 ↾ 𝐴) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅))) | ||
| Theorem | eldisjn0elb 38746 | 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 38747 | 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 38748* | Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023.) |
| ⊢ ( Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)) ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢](𝑅 ⋉ 𝑆) ∩ [𝑣](𝑅 ⋉ 𝑆)) = ∅)) | ||
| Theorem | disjorimxrn 38749 | 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 38750 | Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
| ⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆)) | ||
| Theorem | disjimres 38751 | Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
| ⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴)) | ||
| Theorem | disjimin 38752 | Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.) |
| ⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆)) | ||
| Theorem | disjiminres 38753 | Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
| ⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴))) | ||
| Theorem | disjimxrnres 38754 | Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
| ⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴))) | ||
| Theorem | disjALTV0 38755 | The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.) |
| ⊢ Disj ∅ | ||
| Theorem | disjALTVid 38756 | The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.) |
| ⊢ Disj I | ||
| Theorem | disjALTVidres 38757 | 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 38758 | The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ Disj (𝑅 ∩ ( I ↾ 𝐴)) | ||
| Theorem | disjALTVxrnidres 38759 | 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 38760* | Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → ( Disj (𝑅 ⋉ (◡ E ↾ suc 𝐴)) ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ ∀𝑢 ∈ 𝐴 ((𝑢 ∩ 𝐴) = ∅ ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))) | ||
| Definition | df-antisymrel 38761 | Define the antisymmetric relation predicate. (Read: 𝑅 is an antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.) |
| ⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel (𝑅 ∩ ◡𝑅) ∧ Rel 𝑅)) | ||
| Theorem | dfantisymrel4 38762 | Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.) |
| ⊢ ( AntisymRel 𝑅 ↔ ((𝑅 ∩ ◡𝑅) ⊆ I ∧ Rel 𝑅)) | ||
| Theorem | dfantisymrel5 38763* | Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024.) |
| ⊢ ( AntisymRel 𝑅 ↔ (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ Rel 𝑅)) | ||
| Theorem | antisymrelres 38764* | (Contributed by Peter Mazsa, 25-Jun-2024.) |
| ⊢ ( AntisymRel (𝑅 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) | ||
| Theorem | antisymrelressn 38765 | (Contributed by Peter Mazsa, 29-Jun-2024.) |
| ⊢ AntisymRel (𝑅 ↾ {𝐴}) | ||
| Definition | df-parts 38766 |
Define the class of all partitions, cf. the comment of df-disjs 38705.
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 38705) is what we call membership partition here, cf. dfmembpart2 38771. The binary partitions relation and the partition predicate are the same, that is, (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴) if 𝐴 and 𝑅 are sets, cf. brpartspart 38774. (Contributed by Peter Mazsa, 26-Jun-2021.) |
| ⊢ Parts = ( DomainQss ↾ Disjs ) | ||
| Definition | df-part 38767 | Define the partition predicate (read: 𝐴 is a partition by 𝑅). Alternative definition is dfpart2 38770. The binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets, cf. brpartspart 38774. (Contributed by Peter Mazsa, 12-Aug-2021.) |
| ⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ 𝑅 DomainQs 𝐴)) | ||
| Definition | df-membparts 38768 | Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021.) |
| ⊢ MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎} | ||
| Definition | df-membpart 38769 |
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 38771.
Member partition is the conventional meaning of partition (see the notes of df-parts 38766 and dfmembpart2 38771), we generalize the concept in df-parts 38766 and df-part 38767. Member partition and comember equivalence are the same by mpet 38840. (Contributed by Peter Mazsa, 26-Jun-2021.) |
| ⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴) | ||
| Theorem | dfpart2 38770 | Alternate definition of the partition predicate. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ (𝑅 Part 𝐴 ↔ ( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) | ||
| Theorem | dfmembpart2 38771 | 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 38772 | Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ 𝑅 DomainQss 𝐴))) | ||
| Theorem | brparts2 38773 | Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ (𝑅 ∈ Disjs ∧ (dom 𝑅 / 𝑅) = 𝐴))) | ||
| Theorem | brpartspart 38774 | Binary partition and the partition predicate are the same if 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴)) | ||
| Theorem | parteq1 38775 | Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021.) |
| ⊢ (𝑅 = 𝑆 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)) | ||
| Theorem | parteq2 38776 | Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.) |
| ⊢ (𝐴 = 𝐵 → (𝑅 Part 𝐴 ↔ 𝑅 Part 𝐵)) | ||
| Theorem | parteq12 38777 | Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐵)) | ||
| Theorem | parteq1i 38778 | Equality theorem for partition, inference version. (Contributed by Peter Mazsa, 5-Oct-2021.) |
| ⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴) | ||
| Theorem | parteq1d 38779 | Equality theorem for partition, deduction version. (Contributed by Peter Mazsa, 5-Oct-2021.) |
| ⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝑅 Part 𝐴 ↔ 𝑆 Part 𝐴)) | ||
| Theorem | partsuc2 38780 | Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024.) |
| ⊢ (((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) Part ((𝐴 ∪ {𝐴}) ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴) | ||
| Theorem | partsuc 38781 | Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024.) |
| ⊢ (((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) Part (suc 𝐴 ∖ {𝐴}) ↔ (𝑅 ↾ 𝐴) Part 𝐴) | ||
| Theorem | disjim 38782 | The "Divide et Aequivalere" Theorem: every disjoint relation generates equivalent cosets by the relation: generalization of the former prter1 38880, cf. eldisjim 38785. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 17-Sep-2021.) |
| ⊢ ( Disj 𝑅 → EqvRel ≀ 𝑅) | ||
| Theorem | disjimi 38783 | Every disjoint relation generates equivalent cosets by the relation, inference version. (Contributed by Peter Mazsa, 30-Sep-2021.) |
| ⊢ Disj 𝑅 ⇒ ⊢ EqvRel ≀ 𝑅 | ||
| Theorem | detlem 38784 | 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 38785 | If the elements of 𝐴 are disjoint, then it has equivalent coelements (former prter1 38880). Special case of disjim 38782. (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 38786 | Alternate form of eldisjim 38785. (Contributed by Peter Mazsa, 30-Dec-2024.) |
| ⊢ ( ElDisj 𝐴 → EqvRel ∼ 𝐴) | ||
| Theorem | eqvrel0 38787 | The null class is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ EqvRel ∅ | ||
| Theorem | det0 38788 | The cosets by the null class are in equivalence relation if and only if the null class is disjoint (which it is, see disjALTV0 38755). (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ ( Disj ∅ ↔ EqvRel ≀ ∅) | ||
| Theorem | eqvrelcoss0 38789 | The cosets by the null class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.) |
| ⊢ EqvRel ≀ ∅ | ||
| Theorem | eqvrelid 38790 | 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 38791 | The cosets by a restricted identity relation is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.) |
| ⊢ EqvRel ≀ ( I ↾ 𝐴) | ||
| Theorem | eqvrel1cossinidres 38792 | 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 38793 | 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 38794 | 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 38795 | The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.) |
| ⊢ EqvRel ≀ I | ||
| Theorem | detidres 38796 | 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 38797 | 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 38798 | 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 38799* | Lemma for disjdmqseq 38806, partim2 38808 and petlem 38813 via disjlem17 38800, (general version of the former prtlem14 38875). (Contributed by Peter Mazsa, 10-Sep-2021.) |
| ⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅) → ((𝐴 ∈ [𝑥]𝑅 ∧ 𝐴 ∈ [𝑦]𝑅) → [𝑥]𝑅 = [𝑦]𝑅))) | ||
| Theorem | disjlem17 38800* | Lemma for disjdmqseq 38806, partim2 38808 and petlem 38813 via disjlem18 38801, (general version of the former prtlem17 38877). (Contributed by Peter Mazsa, 10-Sep-2021.) |
| ⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (∃𝑦 ∈ dom 𝑅(𝐴 ∈ [𝑦]𝑅 ∧ 𝐵 ∈ [𝑦]𝑅) → 𝐵 ∈ [𝑥]𝑅))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |