![]() |
Metamath
Proof Explorer Theorem List (p. 84 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | brdifun 8301 | Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
Theorem | swoer 8302* | 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 8303* | The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶)) | ||
Theorem | swoord2 8304* | The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵)) | ||
Theorem | swoso 8305* | 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 8306* | Lemma for eqer 8307. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝐴 = 𝐵} ⇒ ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴) | ||
Theorem | eqer 8307* | 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 8308 | 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 8309 | 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 8310 | Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶) | ||
Theorem | eceq1d 8311 | Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) | ||
Theorem | eceq2 8312 | Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵) | ||
Theorem | eceq2i 8313 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ [𝐶]𝐴 = [𝐶]𝐵 | ||
Theorem | eceq2d 8314 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵) | ||
Theorem | elecg 8315 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | ||
Theorem | elec 8316 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴) | ||
Theorem | relelec 8317 | Membership in an equivalence class when 𝑅 is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | ||
Theorem | ecss 8318 | 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 8319 | 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 8320 | 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 8321 | 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 8322 | 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 8323 | 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 8324 | 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 8325 | An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.) |
⊢ [𝐴] I = {𝐴} | ||
Theorem | qseq1 8326 | Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) | ||
Theorem | qseq2 8327 | Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) | ||
Theorem | qseq2i 8328 | Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 / 𝐴) = (𝐶 / 𝐵) | ||
Theorem | qseq2d 8329 | Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) | ||
Theorem | qseq12 8330 | Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 / 𝐶) = (𝐵 / 𝐷)) | ||
Theorem | elqsg 8331* | Closed form of elqs 8332. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)) | ||
Theorem | elqs 8332* | Membership in a quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) | ||
Theorem | elqsi 8333* | Membership in a quotient set. (Contributed by NM, 23-Jul-1995.) |
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) | ||
Theorem | elqsecl 8334* | 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 8335 | 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 8336 | 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 8337 | "Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.) |
⊢ 𝑅 ∈ V & ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [〈𝐵, 𝐶〉]𝑅 ∈ 𝑆) | ||
Theorem | qsexg 8338 | A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V) | ||
Theorem | qsex 8339 | A quotient set exists. (Contributed by NM, 14-Aug-1995.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 / 𝑅) ∈ V | ||
Theorem | uniqs 8340 | The union of a quotient set. (Contributed by NM, 9-Dec-2008.) |
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴)) | ||
Theorem | qsss 8341 | 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 8342 | The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴) | ||
Theorem | snec 8343 | The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅) | ||
Theorem | ecqs 8344 | Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.) |
⊢ 𝑅 ∈ V ⇒ ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅) | ||
Theorem | ecid 8345 | 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 8346 | 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 8347* | Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑆 = (𝐵 / 𝑅) & ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑) ⇒ ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) | ||
Theorem | ectocl 8348* | Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝑆 = (𝐵 / 𝑅) & ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) | ||
Theorem | elqsn0 8349 | A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995.) |
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅) | ||
Theorem | ecelqsdm 8350 | Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.) |
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴) | ||
Theorem | xpider 8351 | 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 8352* | The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵) | ||
Theorem | riiner 8353* | The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ((𝐵 × 𝐵) ∩ ∩ 𝑥 ∈ 𝐴 𝑅) Er 𝐵) | ||
Theorem | erinxp 8354 | 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 8355 | Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ (((𝑅 “ 𝐴) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 = [𝐵](𝑅 ∩ (𝐴 × 𝐴))) | ||
Theorem | qsinxp 8356 | Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴)))) | ||
Theorem | qsdisj 8357 | 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 8358* | A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016.) |
⊢ (𝑅 Er 𝑋 → Disj 𝑥 ∈ (𝐴 / 𝑅)𝑥) | ||
Theorem | qsel 8359 | 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 8360 | Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 4824. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝑅 Er 𝑋 ⇒ ⊢ ((𝐵 ⊆ (𝐴 / 𝑅) ∧ 𝐶 ⊆ (𝐴 / 𝑅)) → ∪ (𝐵 ∩ 𝐶) = (∪ 𝐵 ∩ ∪ 𝐶)) | ||
Theorem | qliftlem 8361* | 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅)) | ||
Theorem | qliftrel 8362* | 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌)) | ||
Theorem | qliftel 8363* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴))) | ||
Theorem | qliftel1 8364* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴) | ||
Theorem | qliftfun 8365* | 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 8366* | 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 8367* | 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 8368* | The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:(𝑋 / 𝑅)⟶𝑌)) | ||
Theorem | qliftval 8369* | The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵) | ||
Theorem | ecoptocl 8370* | Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅) & ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) | ||
Theorem | 2ecoptocl 8371* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅) & ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒) | ||
Theorem | 3ecoptocl 8372* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.) |
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅) & ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ([〈𝑣, 𝑢〉]𝑅 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃) | ||
Theorem | brecop 8373* | Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.) |
⊢ ∼ ∈ V & ⊢ ∼ Er (𝐺 × 𝐺) & ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) & ⊢ ≤ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ∼ ∧ 𝑦 = [〈𝑣, 𝑢〉] ∼ ) ∧ 𝜑))} & ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([〈𝑧, 𝑤〉] ∼ = [〈𝐴, 𝐵〉] ∼ ∧ [〈𝑣, 𝑢〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) → (𝜑 ↔ 𝜓))) ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([〈𝐴, 𝐵〉] ∼ ≤ [〈𝐶, 𝐷〉] ∼ ↔ 𝜓)) | ||
Theorem | brecop2 8374 | 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 8375* | Lemma for erov 8377 and eroprf 8378. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) | ||
Theorem | erovlem 8376* | Lemma for erov 8377 and eroprf 8378. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} ⇒ ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) | ||
Theorem | erov 8377* | 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 8378* | 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 8379* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ([𝑃] ∼ ⨣ [𝑄] ∼ ) = [(𝑃 + 𝑄)] ∼ ) | ||
Theorem | eroprf2 8380* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽) | ||
Theorem | ecopoveq 8381* | 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 8382* | 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 8383* | 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 8384* | 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 8385* | 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 8386* | 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 8387* | 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 8388* | 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 8389 | 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 8390 | 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 8391* | Define the mapping operation or set exponentiation. The set of all functions that map from 𝐵 to 𝐴 is written (𝐴 ↑m 𝐵) (see mapval 8401). 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 8392* | 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 8400). 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 8391). See mapsspm 8423 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.) |
⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓}) | ||
Theorem | mapprc 8393* | 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 → {𝑓 ∣ 𝑓:𝐴⟶𝐵} = ∅) | ||
Theorem | pmex 8394* | The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ (Fun 𝑓 ∧ 𝑓 ⊆ (𝐴 × 𝐵))} ∈ V) | ||
Theorem | mapex 8395* | The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) | ||
Theorem | fnmap 8396 | Set exponentiation has a universal domain. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ↑m Fn (V × V) | ||
Theorem | fnpm 8397 | Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ ↑pm Fn (V × V) | ||
Theorem | reldmmap 8398 | Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ Rel dom ↑m | ||
Theorem | mapvalg 8399* | The value of set exponentiation. (𝐴 ↑m 𝐵) is the set of all functions that map from 𝐵 to 𝐴. Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ↑m 𝐵) = {𝑓 ∣ 𝑓:𝐵⟶𝐴}) | ||
Theorem | pmvalg 8400* | The value of the partial mapping operation. (𝐴 ↑pm 𝐵) is the set of all partial functions that map from 𝐵 to 𝐴. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ↑pm 𝐵) = {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |