Home | Metamath
Proof Explorer Theorem List (p. 84 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ersym 8301 | An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐴) | ||
Theorem | ercl2 8302 | Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑋) | ||
Theorem | ersymb 8303 | An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
Theorem | ertr 8304 | An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) | ||
Theorem | ertrd 8305 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | ertr2d 8306 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐴) | ||
Theorem | ertr3d 8307 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐵𝑅𝐴) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | ertr4d 8308 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
Theorem | erref 8309 | 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 8310 | The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅) | ||
Theorem | errn 8311 | 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 8312 | An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.) |
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴)) | ||
Theorem | erex 8313 | 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 8314 | 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 8315* | 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 8316* | A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd 8315, 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 8317* | Alternate proof of iseri 8316, avoiding the usage of mptru 1544 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 8318 | Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
Theorem | swoer 8319* | 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 8320* | The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶)) | ||
Theorem | swoord2 8321* | The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵)) | ||
Theorem | swoso 8322* | 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 8323* | Lemma for eqer 8324. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝐴 = 𝐵} ⇒ ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴) | ||
Theorem | eqer 8324* | 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 8325 | 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 8326 | 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 8327 | Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶) | ||
Theorem | eceq1d 8328 | Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) | ||
Theorem | eceq2 8329 | Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵) | ||
Theorem | eceq2i 8330 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ [𝐶]𝐴 = [𝐶]𝐵 | ||
Theorem | eceq2d 8331 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵) | ||
Theorem | elecg 8332 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | ||
Theorem | elec 8333 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴) | ||
Theorem | relelec 8334 | Membership in an equivalence class when 𝑅 is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | ||
Theorem | ecss 8335 | 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 8336 | 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 8337 | 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 8338 | 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 8339 | 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 8340 | 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 8341 | 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 8342 | An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.) |
⊢ [𝐴] I = {𝐴} | ||
Theorem | qseq1 8343 | Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) | ||
Theorem | qseq2 8344 | Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) | ||
Theorem | qseq2i 8345 | Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 / 𝐴) = (𝐶 / 𝐵) | ||
Theorem | qseq2d 8346 | Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) | ||
Theorem | qseq12 8347 | Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 / 𝐶) = (𝐵 / 𝐷)) | ||
Theorem | elqsg 8348* | Closed form of elqs 8349. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)) | ||
Theorem | elqs 8349* | Membership in a quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) | ||
Theorem | elqsi 8350* | Membership in a quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) | ||
Theorem | elqsecl 8351* | 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 8352 | 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 8353 | 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 8354 | "Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.) |
⊢ 𝑅 ∈ V & ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [〈𝐵, 𝐶〉]𝑅 ∈ 𝑆) | ||
Theorem | qsexg 8355 | A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V) | ||
Theorem | qsex 8356 | A quotient set exists. (Contributed by NM, 14-Aug-1995.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 / 𝑅) ∈ V | ||
Theorem | uniqs 8357 | The union of a quotient set. (Contributed by NM, 9-Dec-2008.) |
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴)) | ||
Theorem | qsss 8358 | 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 8359 | The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴) | ||
Theorem | snec 8360 | The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅) | ||
Theorem | ecqs 8361 | Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.) |
⊢ 𝑅 ∈ V ⇒ ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅) | ||
Theorem | ecid 8362 | 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 8363 | 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 8364* | Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑆 = (𝐵 / 𝑅) & ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑) ⇒ ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) | ||
Theorem | ectocl 8365* | Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑆 = (𝐵 / 𝑅) & ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) | ||
Theorem | elqsn0 8366 | A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995.) |
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅) | ||
Theorem | ecelqsdm 8367 | Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.) |
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴) | ||
Theorem | xpider 8368 | 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 8369* | The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵) | ||
Theorem | riiner 8370* | The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ((𝐵 × 𝐵) ∩ ∩ 𝑥 ∈ 𝐴 𝑅) Er 𝐵) | ||
Theorem | erinxp 8371 | 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 8372 | Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ (((𝑅 “ 𝐴) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 = [𝐵](𝑅 ∩ (𝐴 × 𝐴))) | ||
Theorem | qsinxp 8373 | Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴)))) | ||
Theorem | qsdisj 8374 | 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 8375* | A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016.) |
⊢ (𝑅 Er 𝑋 → Disj 𝑥 ∈ (𝐴 / 𝑅)𝑥) | ||
Theorem | qsel 8376 | 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 8377 | Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 4862. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝑅 Er 𝑋 ⇒ ⊢ ((𝐵 ⊆ (𝐴 / 𝑅) ∧ 𝐶 ⊆ (𝐴 / 𝑅)) → ∪ (𝐵 ∩ 𝐶) = (∪ 𝐵 ∩ ∪ 𝐶)) | ||
Theorem | qliftlem 8378* | 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅)) | ||
Theorem | qliftrel 8379* | 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌)) | ||
Theorem | qliftel 8380* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴))) | ||
Theorem | qliftel1 8381* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴) | ||
Theorem | qliftfun 8382* | The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵))) | ||
Theorem | qliftfund 8383* | The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | qliftfuns 8384* | The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑦∀𝑧(𝑦𝑅𝑧 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴))) | ||
Theorem | qliftf 8385* | The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:(𝑋 / 𝑅)⟶𝑌)) | ||
Theorem | qliftval 8386* | The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵) | ||
Theorem | ecoptocl 8387* | Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅) & ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) | ||
Theorem | 2ecoptocl 8388* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅) & ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒) | ||
Theorem | 3ecoptocl 8389* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.) |
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅) & ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ([〈𝑣, 𝑢〉]𝑅 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃) | ||
Theorem | brecop 8390* | Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.) |
⊢ ∼ ∈ V & ⊢ ∼ Er (𝐺 × 𝐺) & ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) & ⊢ ≤ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ∼ ∧ 𝑦 = [〈𝑣, 𝑢〉] ∼ ) ∧ 𝜑))} & ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([〈𝑧, 𝑤〉] ∼ = [〈𝐴, 𝐵〉] ∼ ∧ [〈𝑣, 𝑢〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) → (𝜑 ↔ 𝜓))) ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([〈𝐴, 𝐵〉] ∼ ≤ [〈𝐶, 𝐷〉] ∼ ↔ 𝜓)) | ||
Theorem | brecop2 8391 | 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 8392* | Lemma for erov 8394 and eroprf 8395. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) | ||
Theorem | erovlem 8393* | Lemma for erov 8394 and eroprf 8395. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} ⇒ ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) | ||
Theorem | erov 8394* | 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 8395* | 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 8396* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ([𝑃] ∼ ⨣ [𝑄] ∼ ) = [(𝑃 + 𝑄)] ∼ ) | ||
Theorem | eroprf2 8397* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽) | ||
Theorem | ecopoveq 8398* | 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 8399* | 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 8400* | 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.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |