Home | Metamath
Proof Explorer Theorem List (p. 74 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmoprab 7301* | The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ ∃𝑧𝜑} | ||
Theorem | dmoprabss 7302* | The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.) |
⊢ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) | ||
Theorem | rnoprab 7303* | The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.) |
⊢ ran {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦𝜑} | ||
Theorem | rnoprab2 7304* | The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.) |
⊢ ran {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} | ||
Theorem | reldmoprab 7305* | The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.) |
⊢ Rel dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | oprabss 7306* | Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ ((V × V) × V) | ||
Theorem | eloprabga 7307* | The law of concretion for operation class abstraction. Compare elopab 5397. (Contributed by NM, 14-Sep-1999.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.) Avoid ax-10 2141, ax-11 2158. (Revised by Wolf Lammen, 15-Oct-2024.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | eloprabgaOLD 7308* | Obsolete version of eloprabga 7307 as of 15-Oct-2024. (Contributed by NM, 14-Sep-1999.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) | ||
Theorem | eloprabg 7309* | The law of concretion for operation class abstraction. Compare elopab 5397. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜃)) | ||
Theorem | ssoprab2i 7310* | Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} | ||
Theorem | mpov 7311* | Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝐶} | ||
Theorem | mpomptx 7312* | Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐵(𝑥) is not assumed to be constant w.r.t 𝑥. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | mpompt 7313* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | mpodifsnif 7314 | A mapping with two arguments with the first argument from a difference set with a singleton and a conditional as result. (Contributed by AV, 13-Feb-2019.) |
⊢ (𝑖 ∈ (𝐴 ∖ {𝑋}), 𝑗 ∈ 𝐵 ↦ if(𝑖 = 𝑋, 𝐶, 𝐷)) = (𝑖 ∈ (𝐴 ∖ {𝑋}), 𝑗 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | mposnif 7315 | A mapping with two arguments with the first argument from a singleton and a conditional as result. (Contributed by AV, 14-Feb-2019.) |
⊢ (𝑖 ∈ {𝑋}, 𝑗 ∈ 𝐵 ↦ if(𝑖 = 𝑋, 𝐶, 𝐷)) = (𝑖 ∈ {𝑋}, 𝑗 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | fconstmpo 7316* | Representation of a constant operation using the mapping operation. (Contributed by SO, 11-Jul-2018.) |
⊢ ((𝐴 × 𝐵) × {𝐶}) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | resoprab 7317* | Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.) |
⊢ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↾ (𝐴 × 𝐵)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} | ||
Theorem | resoprab2 7318* | Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ↾ (𝐶 × 𝐷)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)}) | ||
Theorem | resmpo 7319* | Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.) |
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) | ||
Theorem | funoprabg 7320* | "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007.) |
⊢ (∀𝑥∀𝑦∃*𝑧𝜑 → Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}) | ||
Theorem | funoprab 7321* | "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 17-Mar-1995.) |
⊢ ∃*𝑧𝜑 ⇒ ⊢ Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | fnoprabg 7322* | Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.) |
⊢ (∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} Fn {〈𝑥, 𝑦〉 ∣ 𝜑}) | ||
Theorem | mpofun 7323* | The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.) (Proof shortened by SN, 23-Jul-2024.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ Fun 𝐹 | ||
Theorem | mpofunOLD 7324* | Obsolete version of mpofun 7323 as of 23-Jul-2024. (Contributed by Scott Fenton, 21-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ Fun 𝐹 | ||
Theorem | fnoprab 7325* | Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.) |
⊢ (𝜑 → ∃!𝑧𝜓) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} Fn {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | ffnov 7326* | An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.) |
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶)) | ||
Theorem | fovcl 7327 | Closure law for an operation. (Contributed by NM, 19-Apr-2007.) |
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) | ||
Theorem | eqfnov 7328* | Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.) |
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐶 × 𝐷)) → (𝐹 = 𝐺 ↔ ((𝐴 × 𝐵) = (𝐶 × 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)))) | ||
Theorem | eqfnov2 7329* | Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010.) |
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐴 × 𝐵)) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦))) | ||
Theorem | fnov 7330* | Representation of a function in terms of its values. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐹 Fn (𝐴 × 𝐵) ↔ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑥𝐹𝑦))) | ||
Theorem | mpo2eqb 7331* | Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 7329. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 = 𝐷)) | ||
Theorem | rnmpo 7332* | The range of an operation given by the maps-to notation. (Contributed by FL, 20-Jun-2011.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} | ||
Theorem | reldmmpo 7333* | The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ Rel dom 𝐹 | ||
Theorem | elrnmpog 7334* | Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶)) | ||
Theorem | elrnmpo 7335* | Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶) | ||
Theorem | elrnmpores 7336* | Membership in the range of a restricted operation class abstraction. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran (𝐹 ↾ 𝑅) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐷 = 𝐶 ∧ 𝑥𝑅𝑦))) | ||
Theorem | ralrnmpo 7337* | A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∀𝑧 ∈ ran 𝐹𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | rexrnmpo 7338* | A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∃𝑧 ∈ ran 𝐹𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | ovid 7339* | The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = 𝑧 ↔ 𝜑)) | ||
Theorem | ovidig 7340* | The value of an operation class abstraction. Compare ovidi 7341. The condition (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ ∃*𝑧𝜑 & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ (𝜑 → (𝑥𝐹𝑦) = 𝑧) | ||
Theorem | ovidi 7341* | The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃*𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → (𝜑 → (𝑥𝐹𝑦) = 𝑧)) | ||
Theorem | ov 7342* | The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃)) | ||
Theorem | ovigg 7343* | The value of an operation class abstraction. Compare ovig 7344. The condition (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) is been removed. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ ∃*𝑧𝜑 & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → (𝐴𝐹𝐵) = 𝐶)) | ||
Theorem | ovig 7344* | The value of an operation class abstraction (weak version). (Contributed by NM, 14-Sep-1999.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃*𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷) → (𝜓 → (𝐴𝐹𝐵) = 𝐶)) | ||
Theorem | ovmpt4g 7345* | Value of a function given by the maps-to notation. (This is the operation analogue of fvmpt2 6818.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) = 𝐶) | ||
Theorem | ovmpos 7346* | Value of a function given by the maps-to notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝑅 ∈ 𝑉) → (𝐴𝐹𝐵) = ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝑅) | ||
Theorem | ov2gf 7347* | The value of an operation class abstraction. A version of ovmpog 7357 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐺 & ⊢ Ⅎ𝑦𝑆 & ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺) & ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpodxf 7348* | Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐿) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑆 & ⊢ Ⅎ𝑦𝑆 ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpodx 7349* | Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐿) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpod 7350* | Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpox 7351* | The value of an operation class abstraction. Variant of ovmpoga 7352 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ (𝑥 = 𝐴 → 𝐷 = 𝐿) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpoga 7352* | Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpoa 7353* | Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) & ⊢ 𝑆 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpodf 7354* | Alternate deduction version of ovmpo 7358, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓)) & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝐹 & ⊢ Ⅎ𝑦𝜓 ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) | ||
Theorem | ovmpodv 7355* | Alternate deduction version of ovmpo 7358, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓)) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) | ||
Theorem | ovmpodv2 7356* | Alternate deduction version of ovmpo 7358, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → (𝐴𝐹𝐵) = 𝑆)) | ||
Theorem | ovmpog 7357* | Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺) & ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovmpo 7358* | Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺) & ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) & ⊢ 𝑆 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | fvmpopr2d 7359* | Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024.) |
⊢ (𝜑 → 𝐹 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)) & ⊢ (𝜑 → 𝑃 = 〈𝑎, 𝑏〉) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑃) = 𝐶) | ||
Theorem | ov3 7360* | The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.) |
⊢ 𝑆 ∈ V & ⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑅 = 𝑆) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} ⇒ ⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑆) | ||
Theorem | ov6g 7361* | The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.) |
⊢ (〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → 𝑅 = 𝑆) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (〈𝑥, 𝑦〉 ∈ 𝐶 ∧ 𝑧 = 𝑅)} ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ 〈𝐴, 𝐵〉 ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovg 7362* | The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝜏 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)) → ∃!𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃)) | ||
Theorem | ovres 7363 | The value of a restricted operation. (Contributed by FL, 10-Nov-2006.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵)) | ||
Theorem | ovresd 7364 | Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵)) | ||
Theorem | oprres 7365* | The restriction of an operation is an operation. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝐹:(𝑌 × 𝑌)⟶𝑅) & ⊢ (𝜑 → 𝐺:(𝑋 × 𝑋)⟶𝑆) ⇒ ⊢ (𝜑 → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌))) | ||
Theorem | oprssov 7366 | The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.) |
⊢ (((Fun 𝐹 ∧ 𝐺 Fn (𝐶 × 𝐷) ∧ 𝐺 ⊆ 𝐹) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵)) | ||
Theorem | fovrn 7367 | An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.) |
⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) | ||
Theorem | fovrnda 7368 | An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶) | ||
Theorem | fovrnd 7369 | An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶) | ||
Theorem | fnrnov 7370* | The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.) |
⊢ (𝐹 Fn (𝐴 × 𝐵) → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦)}) | ||
Theorem | foov 7371* | An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.) |
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑧 ∈ 𝐶 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦))) | ||
Theorem | fnovrn 7372 | An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.) |
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶𝐹𝐷) ∈ ran 𝐹) | ||
Theorem | ovelrn 7373* | A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 30-Jan-2014.) |
⊢ (𝐹 Fn (𝐴 × 𝐵) → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥𝐹𝑦))) | ||
Theorem | funimassov 7374* | Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.) |
⊢ ((Fun 𝐹 ∧ (𝐴 × 𝐵) ⊆ dom 𝐹) → ((𝐹 “ (𝐴 × 𝐵)) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶)) | ||
Theorem | ovelimab 7375* | Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.) |
⊢ ((𝐹 Fn 𝐴 ∧ (𝐵 × 𝐶) ⊆ 𝐴) → (𝐷 ∈ (𝐹 “ (𝐵 × 𝐶)) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐷 = (𝑥𝐹𝑦))) | ||
Theorem | ovima0 7376 | An operation value is a member of the image plus null. (Contributed by Thierry Arnoux, 25-Jun-2019.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝑅𝑌) ∈ ((𝑅 “ (𝐴 × 𝐵)) ∪ {∅})) | ||
Theorem | ovconst2 7377 | The value of a constant operation. (Contributed by NM, 5-Nov-2006.) |
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵) → (𝑅((𝐴 × 𝐵) × {𝐶})𝑆) = 𝐶) | ||
Theorem | oprssdm 7378* | Domain of closure of an operation. (Contributed by NM, 24-Aug-1995.) |
⊢ ¬ ∅ ∈ 𝑆 & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝑆 × 𝑆) ⊆ dom 𝐹 | ||
Theorem | nssdmovg 7379 | The value of an operation outside its domain. (Contributed by Alexander van der Vekens, 7-Sep-2017.) |
⊢ ((dom 𝐹 ⊆ (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = ∅) | ||
Theorem | ndmovg 7380 | The value of an operation outside its domain. (Contributed by NM, 28-Mar-2008.) |
⊢ ((dom 𝐹 = (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = ∅) | ||
Theorem | ndmov 7381 | The value of an operation outside its domain. (Contributed by NM, 24-Aug-1995.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = ∅) | ||
Theorem | ndmovcl 7382 | The closure of an operation outside its domain, when the domain includes the empty set. This technical lemma can make the operation more convenient to work in some cases. It is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by NM, 24-Sep-2004.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆) & ⊢ ∅ ∈ 𝑆 ⇒ ⊢ (𝐴𝐹𝐵) ∈ 𝑆 | ||
Theorem | ndmovrcl 7383 | Reverse closure law, when an operation's domain doesn't contain the empty set. (Contributed by NM, 3-Feb-1996.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 ⇒ ⊢ ((𝐴𝐹𝐵) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) | ||
Theorem | ndmovcom 7384 | Any operation is commutative outside its domain. (Contributed by NM, 24-Aug-1995.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) | ||
Theorem | ndmovass 7385 | Any operation is associative outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) | ||
Theorem | ndmovdistr 7386 | Any operation is distributive outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 & ⊢ dom 𝐺 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐹(𝐴𝐺𝐶))) | ||
Theorem | ndmovord 7387 | Elimination of redundant antecedents in an ordering law. (Contributed by NM, 7-Mar-1996.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) ⇒ ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | ndmovordi 7388 | Elimination of redundant antecedent in an ordering law. (Contributed by NM, 25-Jun-1998.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 & ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) ⇒ ⊢ ((𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵) → 𝐴𝑅𝐵) | ||
Theorem | caovclg 7389* | Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) ∈ 𝐸) | ||
Theorem | caovcld 7390* | Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐸) | ||
Theorem | caovcl 7391* | Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.) |
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆) | ||
Theorem | caovcomg 7392* | Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) | ||
Theorem | caovcomd 7393* | Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) | ||
Theorem | caovcom 7394* | Convert an operation commutative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) ⇒ ⊢ (𝐴𝐹𝐵) = (𝐵𝐹𝐴) | ||
Theorem | caovassg 7395* | Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro, 26-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) | ||
Theorem | caovassd 7396* | Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) | ||
Theorem | caovass 7397* | Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)) | ||
Theorem | caovcang 7398* | Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | caovcand 7399* | Convert an operation cancellation law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | caovcanrd 7400* | Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ (𝜑 → ((𝐵𝐹𝐴) = (𝐶𝐹𝐴) ↔ 𝐵 = 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |