Home | Metamath
Proof Explorer Theorem List (p. 87 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ertr4d 8601 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | erref 8602 | 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.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐴) | ||
Theorem | ercnv 8603 | The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅) | ||
Theorem | errn 8604 | The range and domain of an equivalence relation are equal. (Contributed by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝑅 Er 𝐴 → ran 𝑅 = 𝐴) | ||
Theorem | erssxp 8605 | An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴)) | ||
Theorem | erex 8606 | An equivalence relation is a set if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝑅 Er 𝐴 → (𝐴 ∈ 𝑉 → 𝑅 ∈ V)) | ||
Theorem | erexb 8607 | An equivalence relation is a set if and only if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝑅 Er 𝐴 → (𝑅 ∈ V ↔ 𝐴 ∈ V)) | ||
Theorem | iserd 8608* | A reflexive, symmetric, transitive relation is an equivalence relation on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝜑 → Rel 𝑅) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦𝑅𝑥) & ⊢ ((𝜑 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)) ⇒ ⊢ (𝜑 → 𝑅 Er 𝐴) | ||
Theorem | iseri 8609* | A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd 8608, which avoids the need to provide a "dummy antecedent" 𝜑 if there is no natural one to choose. (Contributed by AV, 30-Apr-2021.) |
⊢ Rel 𝑅 & ⊢ (𝑥𝑅𝑦 → 𝑦𝑅𝑥) & ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) & ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥) ⇒ ⊢ 𝑅 Er 𝐴 | ||
Theorem | iseriALT 8610* | Alternate proof of iseri 8609, avoiding the usage of mptru 1549 and ⊤ as antecedent by using ax-mp 5 and one of the hypotheses as antecedent. This results, however, in a slightly longer proof. (Contributed by AV, 30-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Rel 𝑅 & ⊢ (𝑥𝑅𝑦 → 𝑦𝑅𝑥) & ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) & ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥) ⇒ ⊢ 𝑅 Er 𝐴 | ||
Theorem | brdifun 8611 | Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
Theorem | swoer 8612* | Incomparability under a strict weak partial order is an equivalence relation. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Er 𝑋) | ||
Theorem | swoord1 8613* | The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶)) | ||
Theorem | swoord2 8614* | The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵)) | ||
Theorem | swoso 8615* | If the incomparability relation is equivalent to equality in a subset, then the partial order strictly orders the subset. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ∧ 𝑥𝑅𝑦)) → 𝑥 = 𝑦) ⇒ ⊢ (𝜑 → < Or 𝑌) | ||
Theorem | eqerlem 8616* | Lemma for eqer 8617. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵} ⇒ ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴) | ||
Theorem | eqer 8617* | Equivalence relation involving equality of dependent classes 𝐴(𝑥) and 𝐵(𝑦). (Contributed by NM, 17-Mar-2008.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof shortened by AV, 1-May-2021.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵} ⇒ ⊢ 𝑅 Er V | ||
Theorem | ider 8618 | The identity relation is an equivalence relation. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 9-Jul-2014.) |
⊢ I Er V | ||
Theorem | 0er 8619 | The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 1-May-2021.) |
⊢ ∅ Er ∅ | ||
Theorem | eceq1 8620 | Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶) | ||
Theorem | eceq1d 8621 | Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) | ||
Theorem | eceq2 8622 | Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵) | ||
Theorem | eceq2i 8623 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ [𝐶]𝐴 = [𝐶]𝐵 | ||
Theorem | eceq2d 8624 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵) | ||
Theorem | elecg 8625 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | ||
Theorem | elec 8626 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴) | ||
Theorem | relelec 8627 | Membership in an equivalence class when 𝑅 is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | ||
Theorem | ecss 8628 | An equivalence class is a subset of the domain. (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → [𝐴]𝑅 ⊆ 𝑋) | ||
Theorem | ecdmn0 8629 | A representative of a nonempty equivalence class belongs to the domain of the equivalence relation. (Contributed by NM, 15-Feb-1996.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ dom 𝑅 ↔ [𝐴]𝑅 ≠ ∅) | ||
Theorem | ereldm 8630 | Equality of equivalence classes implies equivalence of domain membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋)) | ||
Theorem | erth 8631 | Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅)) | ||
Theorem | erth2 8632 | Basic property of equivalence relations. Compare Theorem 73 of [Suppes] p. 82. Assumes membership of the second argument in the domain. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅)) | ||
Theorem | erthi 8633 | 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.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅) | ||
Theorem | erdisj 8634 | 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.) |
⊢ (𝑅 Er 𝑋 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)) | ||
Theorem | ecidsn 8635 | An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.) |
⊢ [𝐴] I = {𝐴} | ||
Theorem | qseq1 8636 | Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) | ||
Theorem | qseq2 8637 | Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) | ||
Theorem | qseq2i 8638 | Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 / 𝐴) = (𝐶 / 𝐵) | ||
Theorem | qseq2d 8639 | Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) | ||
Theorem | qseq12 8640 | Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 / 𝐶) = (𝐵 / 𝐷)) | ||
Theorem | elqsg 8641* | Closed form of elqs 8642. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)) | ||
Theorem | elqs 8642* | Membership in a quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) | ||
Theorem | elqsi 8643* | Membership in a quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) | ||
Theorem | elqsecl 8644* | Membership in a quotient set by an equivalence class according to ∼. (Contributed by Alexander van der Vekens, 12-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ (𝐵 ∈ 𝑋 → (𝐵 ∈ (𝑊 / ∼ ) ↔ ∃𝑥 ∈ 𝑊 𝐵 = {𝑦 ∣ 𝑥 ∼ 𝑦})) | ||
Theorem | ecelqsg 8645 | Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅)) | ||
Theorem | ecelqsi 8646 | Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑅 ∈ V ⇒ ⊢ (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅)) | ||
Theorem | ecopqsi 8647 | "Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.) |
⊢ 𝑅 ∈ V & ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [⟨𝐵, 𝐶⟩]𝑅 ∈ 𝑆) | ||
Theorem | qsexg 8648 | A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V) | ||
Theorem | qsex 8649 | A quotient set exists. (Contributed by NM, 14-Aug-1995.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 / 𝑅) ∈ V | ||
Theorem | uniqs 8650 | The union of a quotient set. (Contributed by NM, 9-Dec-2008.) |
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴)) | ||
Theorem | qsss 8651 | A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝜑 → 𝑅 Er 𝐴) ⇒ ⊢ (𝜑 → (𝐴 / 𝑅) ⊆ 𝒫 𝐴) | ||
Theorem | uniqs2 8652 | The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴) | ||
Theorem | snec 8653 | The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅) | ||
Theorem | ecqs 8654 | Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.) |
⊢ 𝑅 ∈ V ⇒ ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅) | ||
Theorem | ecid 8655 | A set is equal to its coset under the converse membership relation. (Note: the converse membership relation is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ [𝐴]◡ E = 𝐴 | ||
Theorem | qsid 8656 | A set is equal to its quotient set modulo the converse membership relation. (Note: the converse membership relation is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 / ◡ E ) = 𝐴 | ||
Theorem | ectocld 8657* | Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑆 = (𝐵 / 𝑅) & ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑) ⇒ ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) | ||
Theorem | ectocl 8658* | Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑆 = (𝐵 / 𝑅) & ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) | ||
Theorem | elqsn0 8659 | A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995.) |
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅) | ||
Theorem | ecelqsdm 8660 | Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.) |
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴) | ||
Theorem | xpider 8661 | A Cartesian square is an equivalence relation (in general, it is not a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝐴 × 𝐴) Er 𝐴 | ||
Theorem | iiner 8662* | The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵) | ||
Theorem | riiner 8663* | The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ((𝐵 × 𝐵) ∩ ∩ 𝑥 ∈ 𝐴 𝑅) Er 𝐵) | ||
Theorem | erinxp 8664 | A restricted equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝜑 → 𝑅 Er 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑅 ∩ (𝐵 × 𝐵)) Er 𝐵) | ||
Theorem | ecinxp 8665 | Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ (((𝑅 “ 𝐴) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 = [𝐵](𝑅 ∩ (𝐴 × 𝐴))) | ||
Theorem | qsinxp 8666 | Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴)))) | ||
Theorem | qsdisj 8667 | Members of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 / 𝑅)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 / 𝑅)) ⇒ ⊢ (𝜑 → (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅)) | ||
Theorem | qsdisj2 8668* | A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016.) |
⊢ (𝑅 Er 𝑋 → Disj 𝑥 ∈ (𝐴 / 𝑅)𝑥) | ||
Theorem | qsel 8669 | 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.) |
⊢ ((𝑅 Er 𝑋 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅) | ||
Theorem | uniinqs 8670 | Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 4891. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝑅 Er 𝑋 ⇒ ⊢ ((𝐵 ⊆ (𝐴 / 𝑅) ∧ 𝐶 ⊆ (𝐴 / 𝑅)) → ∪ (𝐵 ∩ 𝐶) = (∪ 𝐵 ∩ ∪ 𝐶)) | ||
Theorem | qliftlem 8671* | Lemma for theorems about a function lift. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅)) | ||
Theorem | qliftrel 8672* | 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌)) | ||
Theorem | qliftel 8673* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴))) | ||
Theorem | qliftel1 8674* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴) | ||
Theorem | qliftfun 8675* | The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵))) | ||
Theorem | qliftfund 8676* | The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | qliftfuns 8677* | The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑦∀𝑧(𝑦𝑅𝑧 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴))) | ||
Theorem | qliftf 8678* | The domain and codomain of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:(𝑋 / 𝑅)⟶𝑌)) | ||
Theorem | qliftval 8679* | The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵) | ||
Theorem | ecoptocl 8680* | Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅) & ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) | ||
Theorem | 2ecoptocl 8681* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅) & ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([⟨𝑧, 𝑤⟩]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒) | ||
Theorem | 3ecoptocl 8682* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.) |
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅) & ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([⟨𝑧, 𝑤⟩]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ([⟨𝑣, 𝑢⟩]𝑅 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃) | ||
Theorem | brecop 8683* | Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.) |
⊢ ∼ ∈ V & ⊢ ∼ Er (𝐺 × 𝐺) & ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) & ⊢ ≤ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ∼ ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ∼ ) ∧ 𝜑))} & ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([⟨𝑧, 𝑤⟩] ∼ = [⟨𝐴, 𝐵⟩] ∼ ∧ [⟨𝑣, 𝑢⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) → (𝜑 ↔ 𝜓))) ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([⟨𝐴, 𝐵⟩] ∼ ≤ [⟨𝐶, 𝐷⟩] ∼ ↔ 𝜓)) | ||
Theorem | brecop2 8684 | Binary relation on a quotient set. Lemma for real number construction. Eliminates antecedent from last hypothesis. (Contributed by NM, 13-Feb-1996.) (Revised by AV, 12-Jul-2022.) |
⊢ dom ∼ = (𝐺 × 𝐺) & ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) & ⊢ 𝑅 ⊆ (𝐻 × 𝐻) & ⊢ ≤ ⊆ (𝐺 × 𝐺) & ⊢ ¬ ∅ ∈ 𝐺 & ⊢ dom + = (𝐺 × 𝐺) & ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) ≤ (𝐵 + 𝐶))) ⇒ ⊢ ([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) ≤ (𝐵 + 𝐶)) | ||
Theorem | eroveu 8685* | Lemma for erov 8687 and eroprf 8688. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) | ||
Theorem | erovlem 8686* | Lemma for erov 8687 and eroprf 8688. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} ⇒ ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) | ||
Theorem | erov 8687* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} & ⊢ (𝜑 → 𝑅 ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵) → ([𝑃]𝑅 ⨣ [𝑄]𝑆) = [(𝑃 + 𝑄)]𝑇) | ||
Theorem | eroprf 8688* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} & ⊢ (𝜑 → 𝑅 ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ∈ 𝑌) & ⊢ 𝐿 = (𝐶 / 𝑇) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐾)⟶𝐿) | ||
Theorem | erov2 8689* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ([𝑃] ∼ ⨣ [𝑄] ∼ ) = [(𝑃 + 𝑄)] ∼ ) | ||
Theorem | eroprf2 8690* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽) | ||
Theorem | ecopoveq 8691* | This is the first of several theorems about equivalence relations of the kind used in construction of fractions and signed reals, involving operations on equivalent classes of ordered pairs. This theorem expresses the relation ∼ (specified by the hypothesis) in terms of its operation 𝐹. (Contributed by NM, 16-Aug-1995.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⇒ ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩ ∼ ⟨𝐶, 𝐷⟩ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) | ||
Theorem | ecopovsym 8692* | Assuming the operation 𝐹 is commutative, show that the relation ∼, specified by the first hypothesis, is symmetric. (Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥) ⇒ ⊢ (𝐴 ∼ 𝐵 → 𝐵 ∼ 𝐴) | ||
Theorem | ecopovtrn 8693* | Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation ∼, specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶) | ||
Theorem | ecopover 8694* | Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation ∼, specified by the first hypothesis, is an equivalence relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof shortened by AV, 1-May-2021.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ∼ Er (𝑆 × 𝑆) | ||
Theorem | eceqoveq 8695* | Equality of equivalence relation in terms of an operation. (Contributed by NM, 15-Feb-1996.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ Er (𝑆 × 𝑆) & ⊢ dom + = (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩ ∼ ⟨𝐶, 𝐷⟩ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) | ||
Theorem | ecovcom 8696* | Lemma used to transfer a commutative law via an equivalence relation. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.) |
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝐷, 𝐺⟩] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑥, 𝑦⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ ) & ⊢ 𝐷 = 𝐻 & ⊢ 𝐺 = 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | ecovass 8697* | Lemma used to transfer an associative law via an equivalence relation. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.) |
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝐺, 𝐻⟩] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑁, 𝑄⟩] ∼ ) & ⊢ (((𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝐺, 𝐻⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝐽, 𝐾⟩] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑁, 𝑄⟩] ∼ ) = [⟨𝐿, 𝑀⟩] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆)) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) & ⊢ 𝐽 = 𝐿 & ⊢ 𝐾 = 𝑀 ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | ecovdi 8698* | Lemma used to transfer a distributive law via an equivalence relation. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.) |
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑀, 𝑁⟩] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝑊, 𝑋⟩] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑌, 𝑍⟩] ∼ ) & ⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([⟨𝑊, 𝑋⟩] ∼ + [⟨𝑌, 𝑍⟩] ∼ ) = [⟨𝐾, 𝐿⟩] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) & ⊢ 𝐻 = 𝐾 & ⊢ 𝐽 = 𝐿 ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Syntax | cmap 8699 | Extend the definition of a class to include the mapping operation. (Read for 𝐴 ↑m 𝐵, "the set of all functions that map from 𝐵 to 𝐴.) |
class ↑m | ||
Syntax | cpm 8700 | Extend the definition of a class to include the partial mapping operation. (Read for 𝐴 ↑pm 𝐵, "the set of all partial functions that map from 𝐵 to 𝐴.) |
class ↑pm |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |