![]() |
Metamath
Proof Explorer Theorem List (p. 381 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eleqvrels2 38001 | Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.) |
⊢ (𝑅 ∈ EqvRels ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eleqvrels3 38002* | Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.) |
⊢ (𝑅 ∈ EqvRels ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eleqvrelsrel 38003 | For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate. (Contributed by Peter Mazsa, 24-Aug-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ EqvRels ↔ EqvRel 𝑅)) | ||
Theorem | elcoeleqvrels 38004 | Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ ≀ (◡ E ↾ 𝐴) ∈ EqvRels )) | ||
Theorem | elcoeleqvrelsrel 38005 | For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate. (Contributed by Peter Mazsa, 24-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ CoElEqvRel 𝐴)) | ||
Theorem | eqvrelrel 38006 | An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019.) |
⊢ ( EqvRel 𝑅 → Rel 𝑅) | ||
Theorem | eqvrelrefrel 38007 | An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → RefRel 𝑅) | ||
Theorem | eqvrelsymrel 38008 | An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → SymRel 𝑅) | ||
Theorem | eqvreltrrel 38009 | An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → TrRel 𝑅) | ||
Theorem | eqvrelim 38010 | Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅) | ||
Theorem | eqvreleq 38011 | Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆)) | ||
Theorem | eqvreleqi 38012 | Equality theorem for equivalence relation, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ ( EqvRel 𝑅 ↔ EqvRel 𝑆) | ||
Theorem | eqvreleqd 38013 | Equality theorem for equivalence relation, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ( EqvRel 𝑅 ↔ EqvRel 𝑆)) | ||
Theorem | eqvrelsym 38014 | 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 38015 | 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 38016 | 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 38017 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqvreltr4d 38018 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.) |
⊢ (𝜑 → EqvRel 𝑅) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | eqvrelref 38019 | 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 38020 | 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 38021 | 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 38022 | 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 38023 | 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 38024 | 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 38025 | 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 38026 | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 20-Dec-2021.) |
⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅) | ||
Theorem | eqvrelcoss3 38027* | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧)) | ||
Theorem | eqvrelcoss2 38028 | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅) | ||
Theorem | eqvrelcoss4 38029* | Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 30-Sep-2021.) |
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅)) | ||
Theorem | dfcoeleqvrels 38030 | Alternate definition of the coelement equivalence relations class. Other alternate definitions should be based on eqvrelcoss2 38028, eqvrelcoss3 38027 and eqvrelcoss4 38029 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ CoElEqvRels = {𝑎 ∣ ∼ 𝑎 ∈ EqvRels } | ||
Theorem | dfcoeleqvrel 38031 | 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 38028, eqvrelcoss3 38027 and eqvrelcoss4 38029 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴) | ||
Definition | df-redunds 38032* | Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 38035) is equivalent to satisfying the redundancy predicate (df-redund 38033). (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))} | ||
Definition | df-redund 38033 | Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 38035) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))) | ||
Definition | df-redundp 38034 | Define the redundancy operator for propositions, cf. df-redund 38033. (Contributed by Peter Mazsa, 23-Oct-2022.) |
⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)))) | ||
Theorem | brredunds 38035 | Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))) | ||
Theorem | brredundsredund 38036 | For sets, binary relation on the class of all redundant sets (brredunds 38035) is equivalent to satisfying the redundancy predicate (df-redund 38033). (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ 𝐴 Redund ⟨𝐵, 𝐶⟩)) | ||
Theorem | redundss3 38037 | Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ 𝐷 ⊆ 𝐶 ⇒ ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ → 𝐴 Redund ⟨𝐵, 𝐷⟩) | ||
Theorem | redundeq1 38038 | Equivalence of redundancy predicates. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ 𝐴 = 𝐷 ⇒ ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ 𝐷 Redund ⟨𝐵, 𝐶⟩) | ||
Theorem | redundpim3 38039 | Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ (𝜃 → 𝜒) ⇒ ⊢ ( redund (𝜑, 𝜓, 𝜒) → redund (𝜑, 𝜓, 𝜃)) | ||
Theorem | redundpbi1 38040 | Equivalence of redundancy of propositions. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ (𝜑 ↔ 𝜃) ⇒ ⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ redund (𝜃, 𝜓, 𝜒)) | ||
Theorem | refrelsredund4 38041 | The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 37922) if the relations are symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , ( RefRels ∩ SymRels )⟩ | ||
Theorem | refrelsredund2 38042 | The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 37922) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , EqvRels ⟩ | ||
Theorem | refrelsredund3 38043* | The naive version of the class of reflexive relations {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥} is redundant with respect to the class of reflexive relations (see dfrefrels3 37923) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥} Redund ⟨ RefRels , EqvRels ⟩ | ||
Theorem | refrelredund4 38044 | The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 37924) if the relation is symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, ( RefRel 𝑅 ∧ SymRel 𝑅)) | ||
Theorem | refrelredund2 38045 | The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 37924) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅) | ||
Theorem | refrelredund3 38046* | The naive version of the definition of reflexive relation (∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 ∧ Rel 𝑅) is redundant with respect to reflexive relation (see dfrefrel3 37925) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.) |
⊢ redund ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅) | ||
Definition | df-dmqss 38047* | Define the class of domain quotients. Domain quotients are pairs of sets, typically a relation and a set, where the quotient (see df-qs 8724) of the relation on its domain is equal to the set. See comments of df-ers 38072 for the motivation for this definition. (Contributed by Peter Mazsa, 16-Apr-2019.) |
⊢ DomainQss = {⟨𝑥, 𝑦⟩ ∣ (dom 𝑥 / 𝑥) = 𝑦} | ||
Definition | df-dmqs 38048 | 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 38056. (Contributed by Peter Mazsa, 9-Aug-2021.) |
⊢ (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴) | ||
Theorem | dmqseq 38049 | Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ (𝑅 = 𝑆 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)) | ||
Theorem | dmqseqi 38050 | Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆) | ||
Theorem | dmqseqd 38051 | Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)) | ||
Theorem | dmqseqeq1 38052 | Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ (𝑅 = 𝑆 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)) | ||
Theorem | dmqseqeq1i 38053 | Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴) | ||
Theorem | dmqseqeq1d 38054 | Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)) | ||
Theorem | brdmqss 38055 | The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)) | ||
Theorem | brdmqssqs 38056 | 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 38057 | The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 2-Mar-2018.) |
⊢ ¬ ∅ ∈ (dom 𝑅 / 𝑅) | ||
Theorem | n0eldmqseq 38058 | The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 3-Nov-2018.) |
⊢ ((dom 𝑅 / 𝑅) = 𝐴 → ¬ ∅ ∈ 𝐴) | ||
Theorem | n0elim 38059 | 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 38060 | 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 38061 | 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 38062 | 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 38063 | 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 38064 | 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 38065 | 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 38066 | Lemma for erimeq2 38087. (Contributed by Peter Mazsa, 29-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → (𝐵 ∈ ran 𝑅 ↔ 𝐵 ∈ ∪ 𝐴)))) | ||
Theorem | releldmqs 38067* | Elementhood in the domain quotient of a relation. (Contributed by Peter Mazsa, 24-Apr-2021.) |
⊢ (𝐴 ∈ 𝑉 → (Rel 𝑅 → (𝐴 ∈ (dom 𝑅 / 𝑅) ↔ ∃𝑢 ∈ dom 𝑅∃𝑥 ∈ [ 𝑢]𝑅𝐴 = [𝑢]𝑅))) | ||
Theorem | eldmqs1cossres 38068* | Elementhood in the domain quotient of the class of cosets by a restriction. (Contributed by Peter Mazsa, 4-May-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom ≀ (𝑅 ↾ 𝐴) / ≀ (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑥] ≀ (𝑅 ↾ 𝐴))) | ||
Theorem | releldmqscoss 38069* | 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 38070 | 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 38071 | 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 38072 |
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 8718 "is not standard", "somewhat cryptic", has no costant 0-ary class and does not follow the traditional transparent reflexive-symmetric-transitive relation way of definition of equivalence. Definitions df-eqvrels 37993, dfeqvrels2 37997, dfeqvrels3 37998 and df-eqvrel 37994, dfeqvrel2 37999, dfeqvrel3 38000 are fully transparent in this regard. However, they lack the domain component (dom 𝑅 = 𝐴) of the present df-er 8718. While we acknowledge the need of a domain component, the present df-er 8718 definition does not utilize the results revealed by the new theorems in the Partition-Equivalence Theorem part below (like pets 38261 and pet 38260). From those theorems follows that the natural domain of equivalence relations is not 𝑅Domain𝐴 (i.e. dom 𝑅 = 𝐴 see brdomaing 35467), but 𝑅 DomainQss 𝐴 (i.e. (dom 𝑅 / 𝑅) = 𝐴, see brdmqss 38055), see erimeq 38088 vs. prter3 38291. While I'm sure we need both equivalence relation df-eqvrels 37993 and equivalence relation on domain quotient df-ers 38072, 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 37993 and df-ers 38072 are enough and named the predicate version of the one on domain quotient as the alternate version df-erALTV 38073 of the present df-er 8718. (Contributed by Peter Mazsa, 26-Jun-2021.) |
⊢ Ers = ( DomainQss ↾ EqvRels ) | ||
Definition | df-erALTV 38073 | Equivalence relation with natural domain predicate, see also the comment of df-ers 38072. Alternate definition is dferALTV2 38077. Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets, see brerser 38086. (Contributed by Peter Mazsa, 12-Aug-2021.) |
⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴)) | ||
Definition | df-comembers 38074 | 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 38075 |
Define the comember equivalence relation on the class 𝐴 (or, the
restricted coelement equivalence relation on its domain quotient 𝐴.)
Alternate definitions are dfcomember2 38082 and dfcomember3 38083.
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 38076 | Binary equivalence relation with natural domain, see the comment of df-ers 38072. (Contributed by Peter Mazsa, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝑅 Ers 𝐴 ↔ (𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴))) | ||
Theorem | dferALTV2 38077 | Equivalence relation with natural domain predicate, see the comment of df-ers 38072. (Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa, 30-Aug-2021.) |
⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) | ||
Theorem | erALTVeq1 38078 | Equality theorem for equivalence relation on domain quotient. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ (𝑅 = 𝑆 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴)) | ||
Theorem | erALTVeq1i 38079 | Equality theorem for equivalence relation on domain quotient, inference version. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ 𝑅 = 𝑆 ⇒ ⊢ (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴) | ||
Theorem | erALTVeq1d 38080 | Equality theorem for equivalence relation on domain quotient, deduction version. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝑅 ErALTV 𝐴 ↔ 𝑆 ErALTV 𝐴)) | ||
Theorem | dfcomember 38081 | Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ( CoMembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴) | ||
Theorem | dfcomember2 38082 | Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021.) |
⊢ ( CoMembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (dom ∼ 𝐴 / ∼ 𝐴) = 𝐴)) | ||
Theorem | dfcomember3 38083 | 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 38084 | 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 38085 | 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 38086 | 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 38087 | Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 38291 in a more convenient form , see also erimeq 38088). (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 38088 | 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 38291 and erimeq2 38087). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅)) | ||
Definition | df-funss 38089 | Define the class of all function sets (but not necessarily function relations, cf. df-funsALTV 38090). It is used only by df-funsALTV 38090. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Funss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels } | ||
Definition | df-funsALTV 38090 | Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV 38092, ... , dffunsALTV5 38096. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ FunsALTV = ( Funss ∩ Rels ) | ||
Definition | df-funALTV 38091 |
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 6544, are always the same, that is
( FunALTV 𝐹 ↔ Fun 𝐹), see funALTVfun 38107.
The element of the class of functions and the function predicate are the same, that is (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹) when 𝐹 is a set, see elfunsALTVfunALTV 38106. Alternate definitions are dffunALTV2 38097, ... , dffunALTV5 38100. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹)) | ||
Theorem | dffunsALTV 38092 | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels } | ||
Theorem | dffunsALTV2 38093 | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ≀ 𝑓 ⊆ I } | ||
Theorem | dffunsALTV3 38094* | 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 38095* | 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 38096* | Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021.) |
⊢ FunsALTV = {𝑓 ∈ Rels ∣ ∀𝑥 ∈ ran 𝑓∀𝑦 ∈ ran 𝑓(𝑥 = 𝑦 ∨ ([𝑥]◡𝑓 ∩ [𝑦]◡𝑓) = ∅)} | ||
Theorem | dffunALTV2 38097 | Alternate definition of the function relation predicate, cf. dfdisjALTV2 38123. (Contributed by Peter Mazsa, 8-Feb-2018.) |
⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹)) | ||
Theorem | dffunALTV3 38098* | Alternate definition of the function relation predicate, cf. dfdisjALTV3 38124. Reproduction of dffun2 6552. 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 38099* | Alternate definition of the function relation predicate, cf. dfdisjALTV4 38125. This is dffun6 6555. 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 38100* | Alternate definition of the function relation predicate, cf. dfdisjALTV5 38126. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( FunALTV 𝐹 ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ Rel 𝐹)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |