| Metamath
Proof Explorer Theorem List (p. 387 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 | eqvreltrrel 38601 | An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021.) |
| ⊢ ( EqvRel 𝑅 → TrRel 𝑅) | ||
| Theorem | eqvrelim 38602 | Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.) |
| ⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅) | ||
| Theorem | eqvreleq 38603 | Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 23-Sep-2021.) |
| ⊢ (𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆)) | ||
| Theorem | eqvreleqi 38604 | Equality theorem for equivalence relation, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ 𝑅 = 𝑆 ⇒ ⊢ ( EqvRel 𝑅 ↔ EqvRel 𝑆) | ||
| Theorem | eqvreleqd 38605 | Equality theorem for equivalence relation, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| ⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ( EqvRel 𝑅 ↔ EqvRel 𝑆)) | ||
| Theorem | eqvrelsym 38606 | An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.) |
| ⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐴) | ||
| Theorem | eqvrelsymb 38607 | An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised and distinct variable conditions removed by Peter Mazsa, 2-Jun-2019.) |
| ⊢ (𝜑 → EqvRel 𝑅) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
| Theorem | eqvreltr 38608 | An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.) |
| ⊢ (𝜑 → EqvRel 𝑅) ⇒ ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) | ||
| Theorem | eqvreltrd 38609 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
| ⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
| Theorem | eqvreltr4d 38610 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
| ⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
| Theorem | eqvrelref 38611 | An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56. (Contributed by Mario Carneiro, 6-May-2013.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.) |
| ⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑅) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐴) | ||
| Theorem | eqvrelth 38612 | Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) (Revised by Peter Mazsa, 2-Jun-2019.) |
| ⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑅) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅)) | ||
| Theorem | eqvrelcl 38613 | Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.) |
| ⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ dom 𝑅) | ||
| Theorem | eqvrelthi 38614 | Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
| ⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅) | ||
| Theorem | eqvreldisj 38615 | Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83. (Contributed by NM, 15-Jun-2004.) (Revised by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
| ⊢ ( EqvRel 𝑅 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)) | ||
| Theorem | qsdisjALTV 38616 | Elements of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.) (Revised by Peter Mazsa, 3-Jun-2019.) |
| ⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 / 𝑅)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 / 𝑅)) ⇒ ⊢ (𝜑 → (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅)) | ||
| Theorem | eqvrelqsel 38617 | If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 28-Dec-2019.) |
| ⊢ (( EqvRel 𝑅 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅) | ||
| Theorem | eqvrelcoss 38618 | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 20-Dec-2021.) |
| ⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅) | ||
| Theorem | eqvrelcoss3 38619* | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019.) |
| ⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧)) | ||
| Theorem | eqvrelcoss2 38620 | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) |
| ⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅) | ||
| Theorem | eqvrelcoss4 38621* | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 30-Sep-2021.) |
| ⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅)) | ||
| Theorem | dfcoeleqvrels 38622 | Alternate definition of the coelement equivalence relations class. Other alternate definitions should be based on eqvrelcoss2 38620, eqvrelcoss3 38619 and eqvrelcoss4 38621 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.) |
| ⊢ CoElEqvRels = {𝑎 ∣ ∼ 𝑎 ∈ EqvRels } | ||
| Theorem | dfcoeleqvrel 38623 | Alternate definition of the coelement equivalence relation predicate: a coelement equivalence relation is an equivalence relation on coelements. Other alternate definitions should be based on eqvrelcoss2 38620, eqvrelcoss3 38619 and eqvrelcoss4 38621 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.) |
| ⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴) | ||
| Definition | df-redunds 38624* | Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 38627) is equivalent to satisfying the redundancy predicate (df-redund 38625). (Contributed by Peter Mazsa, 23-Oct-2022.) |
| ⊢ Redunds = ◡{〈〈𝑦, 𝑧〉, 𝑥〉 ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} | ||
| Definition | df-redund 38625 | Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 38627) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.) |
| ⊢ (𝐴 Redund 〈𝐵, 𝐶〉 ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))) | ||
| Definition | df-redundp 38626 | Define the redundancy operator for propositions, cf. df-redund 38625. (Contributed by Peter Mazsa, 23-Oct-2022.) |
| ⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)))) | ||
| Theorem | brredunds 38627 | Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds 〈𝐵, 𝐶〉 ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))) | ||
| Theorem | brredundsredund 38628 | For sets, binary relation on the class of all redundant sets (brredunds 38627) is equivalent to satisfying the redundancy predicate (df-redund 38625). (Contributed by Peter Mazsa, 25-Oct-2022.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds 〈𝐵, 𝐶〉 ↔ 𝐴 Redund 〈𝐵, 𝐶〉)) | ||
| Theorem | redundss3 38629 | Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022.) |
| ⊢ 𝐷 ⊆ 𝐶 ⇒ ⊢ (𝐴 Redund 〈𝐵, 𝐶〉 → 𝐴 Redund 〈𝐵, 𝐷〉) | ||
| Theorem | redundeq1 38630 | Equivalence of redundancy predicates. (Contributed by Peter Mazsa, 26-Oct-2022.) |
| ⊢ 𝐴 = 𝐷 ⇒ ⊢ (𝐴 Redund 〈𝐵, 𝐶〉 ↔ 𝐷 Redund 〈𝐵, 𝐶〉) | ||
| Theorem | redundpim3 38631 | Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022.) |
| ⊢ (𝜃 → 𝜒) ⇒ ⊢ ( redund (𝜑, 𝜓, 𝜒) → redund (𝜑, 𝜓, 𝜃)) | ||
| Theorem | redundpbi1 38632 | Equivalence of redundancy of propositions. (Contributed by Peter Mazsa, 25-Oct-2022.) |
| ⊢ (𝜑 ↔ 𝜃) ⇒ ⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ redund (𝜃, 𝜓, 𝜒)) | ||
| Theorem | refrelsredund4 38633 | The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 38514) if the relations are symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.) |
| ⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund 〈 RefRels , ( RefRels ∩ SymRels )〉 | ||
| Theorem | refrelsredund2 38634 | The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 38514) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.) |
| ⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund 〈 RefRels , EqvRels 〉 | ||
| Theorem | refrelsredund3 38635* | The naive version of the class of reflexive relations {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥} is redundant with respect to the class of reflexive relations (see dfrefrels3 38515) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.) |
| ⊢ {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥} Redund 〈 RefRels , EqvRels 〉 | ||
| Theorem | refrelredund4 38636 | The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 38516) if the relation is symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.) |
| ⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, ( RefRel 𝑅 ∧ SymRel 𝑅)) | ||
| Theorem | refrelredund2 38637 | The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 38516) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.) |
| ⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅) | ||
| Theorem | refrelredund3 38638* | The naive version of the definition of reflexive relation (∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 ∧ Rel 𝑅) is redundant with respect to reflexive relation (see dfrefrel3 38517) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.) |
| ⊢ redund ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅) | ||
| Definition | df-dmqss 38639* | Define the class of domain quotients. Domain quotients are pairs of sets, typically a relation and a set, where the quotient (see df-qs 8751) of the relation on its domain is equal to the set. See comments of df-ers 38664 for the motivation for this definition. (Contributed by Peter Mazsa, 16-Apr-2019.) |
| ⊢ DomainQss = {〈𝑥, 𝑦〉 ∣ (dom 𝑥 / 𝑥) = 𝑦} | ||
| Definition | df-dmqs 38640 | Define the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.) If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same, see brdmqssqs 38648. (Contributed by Peter Mazsa, 9-Aug-2021.) |
| ⊢ (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴) | ||
| Theorem | dmqseq 38641 | Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.) |
| ⊢ (𝑅 = 𝑆 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)) | ||
| Theorem | dmqseqi 38642 | Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
| ⊢ 𝑅 = 𝑆 ⇒ ⊢ (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆) | ||
| Theorem | dmqseqd 38643 | Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
| ⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)) | ||
| Theorem | dmqseqeq1 38644 | Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.) |
| ⊢ (𝑅 = 𝑆 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)) | ||
| Theorem | dmqseqeq1i 38645 | Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
| ⊢ 𝑅 = 𝑆 ⇒ ⊢ ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴) | ||
| Theorem | dmqseqeq1d 38646 | Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
| ⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)) | ||
| Theorem | brdmqss 38647 | The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)) | ||
| Theorem | brdmqssqs 38648 | If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same. (Contributed by Peter Mazsa, 14-Aug-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ 𝑅 DomainQs 𝐴)) | ||
| Theorem | n0eldmqs 38649 | The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 2-Mar-2018.) |
| ⊢ ¬ ∅ ∈ (dom 𝑅 / 𝑅) | ||
| Theorem | n0eldmqseq 38650 | The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 3-Nov-2018.) |
| ⊢ ((dom 𝑅 / 𝑅) = 𝐴 → ¬ ∅ ∈ 𝐴) | ||
| Theorem | n0elim 38651 | Implication of that the empty set is not an element of a class. (Contributed by Peter Mazsa, 30-Dec-2024.) |
| ⊢ (¬ ∅ ∈ 𝐴 → (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴) | ||
| Theorem | n0el3 38652 | Two ways of expressing that the empty set is not an element of a class. (Contributed by Peter Mazsa, 27-May-2021.) |
| ⊢ (¬ ∅ ∈ 𝐴 ↔ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴) | ||
| Theorem | cnvepresdmqss 38653 | The domain quotient binary relation of the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) DomainQss 𝐴 ↔ ¬ ∅ ∈ 𝐴)) | ||
| Theorem | cnvepresdmqs 38654 | The domain quotient predicate for the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021.) |
| ⊢ ((◡ E ↾ 𝐴) DomainQs 𝐴 ↔ ¬ ∅ ∈ 𝐴) | ||
| Theorem | unidmqs 38655 | The range of a relation is equal to the union of the domain quotient. (Contributed by Peter Mazsa, 13-Oct-2018.) |
| ⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ∪ (dom 𝑅 / 𝑅) = ran 𝑅)) | ||
| Theorem | unidmqseq 38656 | The union of the domain quotient of a relation is equal to the class 𝐴 if and only if the range is equal to it as well. (Contributed by Peter Mazsa, 21-Apr-2019.) (Revised by Peter Mazsa, 28-Dec-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → (∪ (dom 𝑅 / 𝑅) = 𝐴 ↔ ran 𝑅 = 𝐴))) | ||
| Theorem | dmqseqim 38657 | If the domain quotient of a relation is equal to the class 𝐴, then the range of the relation is the union of the class. (Contributed by Peter Mazsa, 29-Dec-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → ran 𝑅 = ∪ 𝐴))) | ||
| Theorem | dmqseqim2 38658 | Lemma for erimeq2 38679. (Contributed by Peter Mazsa, 29-Dec-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → (𝐵 ∈ ran 𝑅 ↔ 𝐵 ∈ ∪ 𝐴)))) | ||
| Theorem | releldmqs 38659* | Elementhood in the domain quotient of a relation. (Contributed by Peter Mazsa, 24-Apr-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → (Rel 𝑅 → (𝐴 ∈ (dom 𝑅 / 𝑅) ↔ ∃𝑢 ∈ dom 𝑅∃𝑥 ∈ [ 𝑢]𝑅𝐴 = [𝑢]𝑅))) | ||
| Theorem | eldmqs1cossres 38660* | Elementhood in the domain quotient of the class of cosets by a restriction. (Contributed by Peter Mazsa, 4-May-2019.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom ≀ (𝑅 ↾ 𝐴) / ≀ (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑥] ≀ (𝑅 ↾ 𝐴))) | ||
| Theorem | releldmqscoss 38661* | Elementhood in the domain quotient of the class of cosets by a relation. (Contributed by Peter Mazsa, 23-Apr-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → (Rel 𝑅 → (𝐴 ∈ (dom ≀ 𝑅 / ≀ 𝑅) ↔ ∃𝑢 ∈ dom 𝑅∃𝑥 ∈ [ 𝑢]𝑅𝐴 = [𝑥] ≀ 𝑅))) | ||
| Theorem | dmqscoelseq 38662 | Two ways to express the equality of the domain quotient of the coelements on the class 𝐴 with the class 𝐴. (Contributed by Peter Mazsa, 26-Sep-2021.) |
| ⊢ ((dom ∼ 𝐴 / ∼ 𝐴) = 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴) | ||
| Theorem | dmqs1cosscnvepreseq 38663 | Two ways to express the equality of the domain quotient of the coelements on the class 𝐴 with the class 𝐴. (Contributed by Peter Mazsa, 26-Sep-2021.) |
| ⊢ ((dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴) | ||
| Definition | df-ers 38664 |
Define the class of equivalence relations on domain quotients (or: domain
quotients restricted to equivalence relations).
The present definition of equivalence relation in set.mm df-er 8745 "is not standard", "somewhat cryptic", has no constant 0-ary class and does not follow the traditional transparent reflexive-symmetric-transitive relation way of definition of equivalence. Definitions df-eqvrels 38585, dfeqvrels2 38589, dfeqvrels3 38590 and df-eqvrel 38586, dfeqvrel2 38591, dfeqvrel3 38592 are fully transparent in this regard. However, they lack the domain component (dom 𝑅 = 𝐴) of the present df-er 8745. While we acknowledge the need of a domain component, the present df-er 8745 definition does not utilize the results revealed by the new theorems in the Partition-Equivalence Theorem part below (like pets 38853 and pet 38852). From those theorems follows that the natural domain of equivalence relations is not 𝑅Domain𝐴 (i.e. dom 𝑅 = 𝐴 see brdomaing 35936), but 𝑅 DomainQss 𝐴 (i.e. (dom 𝑅 / 𝑅) = 𝐴, see brdmqss 38647), see erimeq 38680 vs. prter3 38883. While I'm sure we need both equivalence relation df-eqvrels 38585 and equivalence relation on domain quotient df-ers 38664, I'm not sure whether we need a third equivalence relation concept with the present dom 𝑅 = 𝐴 component as well: this needs further investigation. As a default I suppose that these two concepts df-eqvrels 38585 and df-ers 38664 are enough and named the predicate version of the one on domain quotient as the alternate version df-erALTV 38665 of the present df-er 8745. (Contributed by Peter Mazsa, 26-Jun-2021.) |
| ⊢ Ers = ( DomainQss ↾ EqvRels ) | ||
| Definition | df-erALTV 38665 | Equivalence relation with natural domain predicate, see also the comment of df-ers 38664. Alternate definition is dferALTV2 38669. Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets, see brerser 38678. (Contributed by Peter Mazsa, 12-Aug-2021.) |
| ⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴)) | ||
| Definition | df-comembers 38666 | Define the class of comember equivalence relations on their domain quotients. (Contributed by Peter Mazsa, 28-Nov-2022.) (Revised by Peter Mazsa, 24-Jul-2023.) |
| ⊢ CoMembErs = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) Ers 𝑎} | ||
| Definition | df-comember 38667 |
Define the comember equivalence relation on the class 𝐴 (or, the
restricted coelement equivalence relation on its domain quotient 𝐴.)
Alternate definitions are dfcomember2 38674 and dfcomember3 38675.
Later on, in an application of set theory I make a distinction between the default elementhood concept and a special membership concept: membership equivalence relation will be an integral part of that membership concept. (Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa, 28-Nov-2022.) |
| ⊢ ( CoMembEr 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴) | ||
| Theorem | brers 38668 | Binary equivalence relation with natural domain, see the comment of df-ers 38664. (Contributed by Peter Mazsa, 23-Jul-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝑅 Ers 𝐴 ↔ (𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴))) | ||
| Theorem | dferALTV2 38669 | Equivalence relation with natural domain predicate, see the comment of df-ers 38664. (Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa, 30-Aug-2021.) |
| ⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) | ||
| Theorem | erALTVeq1 38670 | Equality theorem for equivalence relation on domain quotient. (Contributed by Peter Mazsa, 25-Sep-2021.) |
| ⊢ (𝑅 = 𝑆 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴)) | ||
| Theorem | erALTVeq1i 38671 | Equality theorem for equivalence relation on domain quotient, inference version. (Contributed by Peter Mazsa, 25-Sep-2021.) |
| ⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴) | ||
| Theorem | erALTVeq1d 38672 | Equality theorem for equivalence relation on domain quotient, deduction version. (Contributed by Peter Mazsa, 25-Sep-2021.) |
| ⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴)) | ||
| Theorem | dfcomember 38673 | Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 28-Nov-2022.) |
| ⊢ ( CoMembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴) | ||
| Theorem | dfcomember2 38674 | Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021.) |
| ⊢ ( CoMembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (dom ∼ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
| Theorem | dfcomember3 38675 | Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, 17-Jul-2023.) |
| ⊢ ( CoMembEr 𝐴 ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
| Theorem | eqvreldmqs 38676 | Two ways to express comember equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, 17-Jul-2023.) |
| ⊢ (( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
| Theorem | eqvreldmqs2 38677 | Two ways to express comember equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 30-Dec-2024.) |
| ⊢ (( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
| Theorem | brerser 38678 | Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 25-Aug-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Ers 𝐴 ↔ 𝑅 ErALTV 𝐴)) | ||
| Theorem | erimeq2 38679 | Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 38883 in a more convenient form , see also erimeq 38680). (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 29-Dec-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ∼ 𝐴 = 𝑅)) | ||
| Theorem | erimeq 38680 | Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is the most convenient form of prter3 38883 and erimeq2 38679). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.) |
| ⊢ (𝑅 ∈ 𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅)) | ||
| Definition | df-funss 38681 | Define the class of all function sets (but not necessarily function relations, cf. df-funsALTV 38682). It is used only by df-funsALTV 38682. (Contributed by Peter Mazsa, 17-Jul-2021.) |
| ⊢ Funss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels } | ||
| Definition | df-funsALTV 38682 | Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV 38684, ... , dffunsALTV5 38688. (Contributed by Peter Mazsa, 17-Jul-2021.) |
| ⊢ FunsALTV = ( Funss ∩ Rels ) | ||
| Definition | df-funALTV 38683 |
Define the function relation predicate, i.e., the function predicate.
This definition of the function predicate (based on a more general,
converse reflexive, relation) and the original definition of function in
set.mm df-fun 6563, are always the same, that is
( FunALTV 𝐹 ↔ Fun 𝐹), see funALTVfun 38699.
The element of the class of functions and the function predicate are the same, that is (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹) when 𝐹 is a set, see elfunsALTVfunALTV 38698. Alternate definitions are dffunALTV2 38689, ... , dffunALTV5 38692. (Contributed by Peter Mazsa, 17-Jul-2021.) |
| ⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹)) | ||
| Theorem | dffunsALTV 38684 | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021.) |
| ⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels } | ||
| Theorem | dffunsALTV2 38685 | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021.) |
| ⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ⊆ I } | ||
| Theorem | dffunsALTV3 38686* | Alternate definition of the class of functions. For the 𝑋 axis and the 𝑌 axis you can convert the right side to {𝑓 ∈ Rels ∣ ∀ x1 ∀ y1 ∀ y2 (( x1 𝑓 y1 ∧ x1 𝑓 y2 ) → y1 = y2 )}. (Contributed by Peter Mazsa, 30-Aug-2021.) |
| ⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑢∀𝑥∀𝑦((𝑢𝑓𝑥 ∧ 𝑢𝑓𝑦) → 𝑥 = 𝑦)} | ||
| Theorem | dffunsALTV4 38687* | Alternate definition of the class of functions. For the 𝑋 axis and the 𝑌 axis you can convert the right side to {𝑓 ∈ Rels ∣ ∀𝑥1∃*𝑦1𝑥1𝑓𝑦1}. (Contributed by Peter Mazsa, 31-Aug-2021.) |
| ⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑢∃*𝑥 𝑢𝑓𝑥} | ||
| Theorem | dffunsALTV5 38688* | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
| ⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑥 ∈ ran 𝑓∀𝑦 ∈ ran 𝑓(𝑥 = 𝑦 ∨ ([𝑥]◡𝑓 ∩ [𝑦]◡𝑓) = ∅)} | ||
| Theorem | dffunALTV2 38689 | Alternate definition of the function relation predicate, cf. dfdisjALTV2 38715. (Contributed by Peter Mazsa, 8-Feb-2018.) |
| ⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹)) | ||
| Theorem | dffunALTV3 38690* | Alternate definition of the function relation predicate, cf. dfdisjALTV3 38716. Reproduction of dffun2 6571. For the 𝑋 axis and the 𝑌 axis you can convert the right side to (∀ x1 ∀ y1 ∀ y2 (( x1 𝑓 y1 ∧ x1 𝑓 y2 ) → y1 = y2 ) ∧ Rel 𝐹). (Contributed by NM, 29-Dec-1996.) |
| ⊢ ( FunALTV 𝐹 ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ Rel 𝐹)) | ||
| Theorem | dffunALTV4 38691* | Alternate definition of the function relation predicate, cf. dfdisjALTV4 38717. This is dffun6 6574. For the 𝑋 axis and the 𝑌 axis you can convert the right side to (∀𝑥1∃*𝑦1𝑥1𝐹𝑦1 ∧ Rel 𝐹). (Contributed by NM, 9-Mar-1995.) |
| ⊢ ( FunALTV 𝐹 ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ Rel 𝐹)) | ||
| Theorem | dffunALTV5 38692* | Alternate definition of the function relation predicate, cf. dfdisjALTV5 38718. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹)) | ||
| Theorem | elfunsALTV 38693 | Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021.) |
| ⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels )) | ||
| Theorem | elfunsALTV2 38694 | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
| ⊢ (𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ⊆ I ∧ 𝐹 ∈ Rels )) | ||
| Theorem | elfunsALTV3 38695* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
| ⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝐹𝑥 ∧ 𝑢𝐹𝑦) → 𝑥 = 𝑦) ∧ 𝐹 ∈ Rels )) | ||
| Theorem | elfunsALTV4 38696* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
| ⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑢∃*𝑥 𝑢𝐹𝑥 ∧ 𝐹 ∈ Rels )) | ||
| Theorem | elfunsALTV5 38697* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.) |
| ⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels )) | ||
| Theorem | elfunsALTVfunALTV 38698 | The element of the class of functions and the function predicate are the same when 𝐹 is a set. (Contributed by Peter Mazsa, 26-Jul-2021.) |
| ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹)) | ||
| Theorem | funALTVfun 38699 | Our definition of the function predicate df-funALTV 38683 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6563, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.) |
| ⊢ ( FunALTV 𝐹 ↔ Fun 𝐹) | ||
| Theorem | funALTVss 38700 | Subclass theorem for function. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) (Revised by Peter Mazsa, 22-Sep-2021.) |
| ⊢ (𝐴 ⊆ 𝐵 → ( FunALTV 𝐵 → FunALTV 𝐴)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |