Home | Metamath
Proof Explorer Theorem List (p. 86 of 465) | < 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-29274) |
Hilbert Space Explorer
(29275-30797) |
Users' Mathboxes
(30798-46480) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | errn 8501 | 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 8502 | An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴)) | ||
Theorem | erex 8503 | 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 8504 | 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 8505* | 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 8506* | A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd 8505, 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 8507* | Alternate proof of iseri 8506, 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 8508 | Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
Theorem | swoer 8509* | 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 8510* | The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶)) | ||
Theorem | swoord2 8511* | The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵)) | ||
Theorem | swoso 8512* | 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 8513* | Lemma for eqer 8514. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝐴 = 𝐵} ⇒ ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴) | ||
Theorem | eqer 8514* | 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 8515 | 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 8516 | 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 8517 | Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶) | ||
Theorem | eceq1d 8518 | Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) | ||
Theorem | eceq2 8519 | Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵) | ||
Theorem | eceq2i 8520 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ [𝐶]𝐴 = [𝐶]𝐵 | ||
Theorem | eceq2d 8521 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵) | ||
Theorem | elecg 8522 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | ||
Theorem | elec 8523 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴) | ||
Theorem | relelec 8524 | Membership in an equivalence class when 𝑅 is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | ||
Theorem | ecss 8525 | 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 8526 | 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 8527 | 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 8528 | 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 8529 | 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 8530 | 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 8531 | 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 8532 | An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.) |
⊢ [𝐴] I = {𝐴} | ||
Theorem | qseq1 8533 | Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) | ||
Theorem | qseq2 8534 | Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) | ||
Theorem | qseq2i 8535 | Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 / 𝐴) = (𝐶 / 𝐵) | ||
Theorem | qseq2d 8536 | Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) | ||
Theorem | qseq12 8537 | Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 / 𝐶) = (𝐵 / 𝐷)) | ||
Theorem | elqsg 8538* | Closed form of elqs 8539. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)) | ||
Theorem | elqs 8539* | Membership in a quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) | ||
Theorem | elqsi 8540* | Membership in a quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) | ||
Theorem | elqsecl 8541* | 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 8542 | 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 8543 | 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 8544 | "Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.) |
⊢ 𝑅 ∈ V & ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [〈𝐵, 𝐶〉]𝑅 ∈ 𝑆) | ||
Theorem | qsexg 8545 | A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V) | ||
Theorem | qsex 8546 | A quotient set exists. (Contributed by NM, 14-Aug-1995.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 / 𝑅) ∈ V | ||
Theorem | uniqs 8547 | The union of a quotient set. (Contributed by NM, 9-Dec-2008.) |
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴)) | ||
Theorem | qsss 8548 | 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 8549 | The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴) | ||
Theorem | snec 8550 | The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅) | ||
Theorem | ecqs 8551 | Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.) |
⊢ 𝑅 ∈ V ⇒ ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅) | ||
Theorem | ecid 8552 | 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 8553 | 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 8554* | Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑆 = (𝐵 / 𝑅) & ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑) ⇒ ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) | ||
Theorem | ectocl 8555* | Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑆 = (𝐵 / 𝑅) & ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) | ||
Theorem | elqsn0 8556 | A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995.) |
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅) | ||
Theorem | ecelqsdm 8557 | Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.) |
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴) | ||
Theorem | xpider 8558 | 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 8559* | The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵) | ||
Theorem | riiner 8560* | The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ((𝐵 × 𝐵) ∩ ∩ 𝑥 ∈ 𝐴 𝑅) Er 𝐵) | ||
Theorem | erinxp 8561 | 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 8562 | Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ (((𝑅 “ 𝐴) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 = [𝐵](𝑅 ∩ (𝐴 × 𝐴))) | ||
Theorem | qsinxp 8563 | Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴)))) | ||
Theorem | qsdisj 8564 | 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 8565* | A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016.) |
⊢ (𝑅 Er 𝑋 → Disj 𝑥 ∈ (𝐴 / 𝑅)𝑥) | ||
Theorem | qsel 8566 | 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 8567 | Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 4871. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝑅 Er 𝑋 ⇒ ⊢ ((𝐵 ⊆ (𝐴 / 𝑅) ∧ 𝐶 ⊆ (𝐴 / 𝑅)) → ∪ (𝐵 ∩ 𝐶) = (∪ 𝐵 ∩ ∪ 𝐶)) | ||
Theorem | qliftlem 8568* | Lemma for theorems about a function lift. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅)) | ||
Theorem | qliftrel 8569* | 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌)) | ||
Theorem | qliftel 8570* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴))) | ||
Theorem | qliftel1 8571* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴) | ||
Theorem | qliftfun 8572* | 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 8573* | 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 8574* | 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 8575* | The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:(𝑋 / 𝑅)⟶𝑌)) | ||
Theorem | qliftval 8576* | The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵) | ||
Theorem | ecoptocl 8577* | Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅) & ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) | ||
Theorem | 2ecoptocl 8578* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅) & ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒) | ||
Theorem | 3ecoptocl 8579* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.) |
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅) & ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ([〈𝑣, 𝑢〉]𝑅 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃) | ||
Theorem | brecop 8580* | Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.) |
⊢ ∼ ∈ V & ⊢ ∼ Er (𝐺 × 𝐺) & ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) & ⊢ ≤ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ∼ ∧ 𝑦 = [〈𝑣, 𝑢〉] ∼ ) ∧ 𝜑))} & ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([〈𝑧, 𝑤〉] ∼ = [〈𝐴, 𝐵〉] ∼ ∧ [〈𝑣, 𝑢〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) → (𝜑 ↔ 𝜓))) ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([〈𝐴, 𝐵〉] ∼ ≤ [〈𝐶, 𝐷〉] ∼ ↔ 𝜓)) | ||
Theorem | brecop2 8581 | 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 8582* | Lemma for erov 8584 and eroprf 8585. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) | ||
Theorem | erovlem 8583* | Lemma for erov 8584 and eroprf 8585. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} ⇒ ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) | ||
Theorem | erov 8584* | 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 8585* | 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 8586* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ([𝑃] ∼ ⨣ [𝑄] ∼ ) = [(𝑃 + 𝑄)] ∼ ) | ||
Theorem | eroprf2 8587* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽) | ||
Theorem | ecopoveq 8588* | 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 8589* | 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 8590* | 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 8591* | 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 8592* | 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 8593* | 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 8594* | 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 8595* | 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 8596 | 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 8597 | 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 | ||
Definition | df-map 8598* | Define the mapping operation or set exponentiation. The set of all functions that map from 𝐵 to 𝐴 is written (𝐴 ↑m 𝐵) (see mapval 8608). Many authors write 𝐴 followed by 𝐵 as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring] p. 95). Other authors show 𝐵 as a prefixed superscript, which is read "𝐴 pre 𝐵 " (e.g., definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map(𝐵, 𝐴) for our (𝐴 ↑m 𝐵). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 8-Dec-2003.) |
⊢ ↑m = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) | ||
Definition | df-pm 8599* | Define the partial mapping operation. A partial function from 𝐵 to 𝐴 is a function from a subset of 𝐵 to 𝐴. The set of all partial functions from 𝐵 to 𝐴 is written (𝐴 ↑pm 𝐵) (see pmvalg 8607). A notation for this operation apparently does not appear in the literature. We use ↑pm to distinguish it from the less general set exponentiation operation ↑m (df-map 8598). See mapsspm 8645 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.) |
⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓}) | ||
Theorem | mapprc 8600* | When 𝐴 is a proper class, the class of all functions mapping 𝐴 to 𝐵 is empty. Exercise 4.41 of [Mendelson] p. 255. (Contributed by NM, 8-Dec-2003.) |
⊢ (¬ 𝐴 ∈ V → {𝑓 ∣ 𝑓:𝐴⟶𝐵} = ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |