Home | Metamath
Proof Explorer Theorem List (p. 74 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ov6g 7301* | The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.) |
⊢ (〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → 𝑅 = 𝑆) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (〈𝑥, 𝑦〉 ∈ 𝐶 ∧ 𝑧 = 𝑅)} ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ 〈𝐴, 𝐵〉 ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ovg 7302* | The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝜏 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)) → ∃!𝑧𝜑) & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃)) | ||
Theorem | ovres 7303 | The value of a restricted operation. (Contributed by FL, 10-Nov-2006.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵)) | ||
Theorem | ovresd 7304 | Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵)) | ||
Theorem | oprres 7305* | The restriction of an operation is an operation. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝐹:(𝑌 × 𝑌)⟶𝑅) & ⊢ (𝜑 → 𝐺:(𝑋 × 𝑋)⟶𝑆) ⇒ ⊢ (𝜑 → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌))) | ||
Theorem | oprssov 7306 | The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.) |
⊢ (((Fun 𝐹 ∧ 𝐺 Fn (𝐶 × 𝐷) ∧ 𝐺 ⊆ 𝐹) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵)) | ||
Theorem | fovrn 7307 | An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.) |
⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) | ||
Theorem | fovrnda 7308 | An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶) | ||
Theorem | fovrnd 7309 | An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶) | ||
Theorem | fnrnov 7310* | The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.) |
⊢ (𝐹 Fn (𝐴 × 𝐵) → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦)}) | ||
Theorem | foov 7311* | An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.) |
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑧 ∈ 𝐶 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦))) | ||
Theorem | fnovrn 7312 | An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.) |
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶𝐹𝐷) ∈ ran 𝐹) | ||
Theorem | ovelrn 7313* | 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 7314* | Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.) |
⊢ ((Fun 𝐹 ∧ (𝐴 × 𝐵) ⊆ dom 𝐹) → ((𝐹 “ (𝐴 × 𝐵)) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶)) | ||
Theorem | ovelimab 7315* | Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.) |
⊢ ((𝐹 Fn 𝐴 ∧ (𝐵 × 𝐶) ⊆ 𝐴) → (𝐷 ∈ (𝐹 “ (𝐵 × 𝐶)) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐷 = (𝑥𝐹𝑦))) | ||
Theorem | ovima0 7316 | An operation value is a member of the image plus null. (Contributed by Thierry Arnoux, 25-Jun-2019.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝑅𝑌) ∈ ((𝑅 “ (𝐴 × 𝐵)) ∪ {∅})) | ||
Theorem | ovconst2 7317 | The value of a constant operation. (Contributed by NM, 5-Nov-2006.) |
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵) → (𝑅((𝐴 × 𝐵) × {𝐶})𝑆) = 𝐶) | ||
Theorem | oprssdm 7318* | Domain of closure of an operation. (Contributed by NM, 24-Aug-1995.) |
⊢ ¬ ∅ ∈ 𝑆 & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝑆 × 𝑆) ⊆ dom 𝐹 | ||
Theorem | nssdmovg 7319 | The value of an operation outside its domain. (Contributed by Alexander van der Vekens, 7-Sep-2017.) |
⊢ ((dom 𝐹 ⊆ (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = ∅) | ||
Theorem | ndmovg 7320 | The value of an operation outside its domain. (Contributed by NM, 28-Mar-2008.) |
⊢ ((dom 𝐹 = (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = ∅) | ||
Theorem | ndmov 7321 | The value of an operation outside its domain. (Contributed by NM, 24-Aug-1995.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = ∅) | ||
Theorem | ndmovcl 7322 | 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 7323 | Reverse closure law, when an operation's domain doesn't contain the empty set. (Contributed by NM, 3-Feb-1996.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 ⇒ ⊢ ((𝐴𝐹𝐵) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) | ||
Theorem | ndmovcom 7324 | Any operation is commutative outside its domain. (Contributed by NM, 24-Aug-1995.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) | ||
Theorem | ndmovass 7325 | 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 7326 | 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 7327 | Elimination of redundant antecedents in an ordering law. (Contributed by NM, 7-Mar-1996.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) ⇒ ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | ndmovordi 7328 | Elimination of redundant antecedent in an ordering law. (Contributed by NM, 25-Jun-1998.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 & ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) ⇒ ⊢ ((𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵) → 𝐴𝑅𝐵) | ||
Theorem | caovclg 7329* | Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) ∈ 𝐸) | ||
Theorem | caovcld 7330* | Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐸) | ||
Theorem | caovcl 7331* | Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.) |
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆) | ||
Theorem | caovcomg 7332* | Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) | ||
Theorem | caovcomd 7333* | Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) | ||
Theorem | caovcom 7334* | 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 7335* | Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro, 26-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) | ||
Theorem | caovassd 7336* | Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) | ||
Theorem | caovass 7337* | 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 7338* | Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | caovcand 7339* | Convert an operation cancellation law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | caovcanrd 7340* | Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ (𝜑 → ((𝐵𝐹𝐴) = (𝐶𝐹𝐴) ↔ 𝐵 = 𝐶)) | ||
Theorem | caovcan 7341* | Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) |
⊢ 𝐶 ∈ V & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) → 𝐵 = 𝐶)) | ||
Theorem | caovordig 7342* | Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | caovordid 7343* | Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | caovordg 7344* | Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | caovordd 7345* | Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | caovord2d 7346* | Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶))) | ||
Theorem | caovord3d 7347* | Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐶𝐹𝐷) → (𝐴𝑅𝐶 ↔ 𝐷𝑅𝐵))) | ||
Theorem | caovord 7348* | Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | caovord2 7349* | Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) ⇒ ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶))) | ||
Theorem | caovord3 7350* | Ordering law. (Contributed by NM, 29-Feb-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ 𝐷 ∈ V ⇒ ⊢ (((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴𝐹𝐵) = (𝐶𝐹𝐷)) → (𝐴𝑅𝐶 ↔ 𝐷𝑅𝐵)) | ||
Theorem | caovdig 7351* | Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶))) | ||
Theorem | caovdid 7352* | Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶))) | ||
Theorem | caovdir2d 7353* | Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐶))) | ||
Theorem | caovdirg 7354* | Convert an operation reverse distributive law to class notation. (Contributed by Mario Carneiro, 19-Oct-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐾)) → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶))) | ||
Theorem | caovdird 7355* | Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶))) | ||
Theorem | caovdi 7356* | Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)) ⇒ ⊢ (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐹(𝐴𝐺𝐶)) | ||
Theorem | caov32d 7357* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵)) | ||
Theorem | caov12d 7358* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))) | ||
Theorem | caov31d 7359* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴)) | ||
Theorem | caov13d 7360* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴))) | ||
Theorem | caov4d 7361* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷))) | ||
Theorem | caov411d 7362* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹𝐵)𝐹(𝐴𝐹𝐷))) | ||
Theorem | caov42d 7363* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐷𝐹𝐵))) | ||
Theorem | caov32 7364* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵) | ||
Theorem | caov12 7365* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶)) | ||
Theorem | caov31 7366* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴) | ||
Theorem | caov13 7367* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴)) | ||
Theorem | caov4 7368* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) & ⊢ 𝐷 ∈ V ⇒ ⊢ ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷)) | ||
Theorem | caov411 7369* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) & ⊢ 𝐷 ∈ V ⇒ ⊢ ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹𝐵)𝐹(𝐴𝐹𝐷)) | ||
Theorem | caov42 7370* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) & ⊢ 𝐷 ∈ V ⇒ ⊢ ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐷𝐹𝐵)) | ||
Theorem | caovdir 7371* | Reverse distributive law. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥) & ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐶)) | ||
Theorem | caovdilem 7372* | Lemma used by real number construction. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥) & ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)) & ⊢ 𝐷 ∈ V & ⊢ 𝐻 ∈ V & ⊢ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ⇒ ⊢ (((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻) = ((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐵𝐺(𝐷𝐺𝐻))) | ||
Theorem | caovlem2 7373* | Lemma used in real number construction. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥) & ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)) & ⊢ 𝐷 ∈ V & ⊢ 𝐻 ∈ V & ⊢ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) & ⊢ 𝑅 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻)𝐹(((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅)) = ((𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻)))) | ||
Theorem | caovmo 7374* | Uniqueness of inverse element in commutative, associative operation with identity. Remark in proof of Proposition 9-2.4 of [Gleason] p. 119. (Contributed by NM, 4-Mar-1996.) |
⊢ 𝐵 ∈ 𝑆 & ⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) & ⊢ (𝑥 ∈ 𝑆 → (𝑥𝐹𝐵) = 𝑥) ⇒ ⊢ ∃*𝑤(𝐴𝐹𝑤) = 𝐵 | ||
Theorem | mpondm0 7375* | The value of an operation given by a maps-to rule is the empty set if the arguments are not contained in the base sets of the rule. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) ⇒ ⊢ (¬ (𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉𝐹𝑊) = ∅) | ||
Theorem | elmpocl 7376* | If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵)) | ||
Theorem | elmpocl1 7377* | If a two-parameter class is not empty, the first argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → 𝑆 ∈ 𝐴) | ||
Theorem | elmpocl2 7378* | If a two-parameter class is not empty, the second argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → 𝑇 ∈ 𝐵) | ||
Theorem | elovmpo 7379* |
Utility lemma for two-parameter classes.
EDITORIAL: can simplify isghm 18298, islmhm 19730. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐷 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐶 ∈ V & ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → 𝐶 = 𝐸) ⇒ ⊢ (𝐹 ∈ (𝑋𝐷𝑌) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 ∈ 𝐸)) | ||
Theorem | elovmporab 7380* | Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ 𝑀 ∣ 𝜑}) & ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → 𝑀 ∈ V) ⇒ ⊢ (𝑍 ∈ (𝑋𝑂𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ 𝑀)) | ||
Theorem | elovmporab1w 7381* | Version of elovmporab1 7382 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑍 ∈ (𝑋𝑂𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋𝑋 / 𝑚⦌𝑀)) | ||
Theorem | elovmporab1 7382* | Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑍 ∈ (𝑋𝑂𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋𝑋 / 𝑚⦌𝑀)) | ||
Theorem | 2mpo0 7383* | If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021.) |
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) & ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝑂𝑌) = (𝑠 ∈ 𝐶, 𝑡 ∈ 𝐷 ↦ 𝐹)) ⇒ ⊢ (¬ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷)) → (𝑆(𝑋𝑂𝑌)𝑇) = ∅) | ||
Theorem | relmptopab 7384* | Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 7-Aug-2014.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {〈𝑦, 𝑧〉 ∣ 𝜑}) ⇒ ⊢ Rel (𝐹‘𝐵) | ||
Theorem | f1ocnvd 7385* | Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) | ||
Theorem | f1od 7386* | Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | f1ocnv2d 7387* | Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) | ||
Theorem | f1o2d 7388* | Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | f1opw2 7389* | A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw 7390 avoids the Axiom of Replacement. (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → (◡𝐹 “ 𝑎) ∈ V) & ⊢ (𝜑 → (𝐹 “ 𝑏) ∈ V) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹 “ 𝑏)):𝒫 𝐴–1-1-onto→𝒫 𝐵) | ||
Theorem | f1opw 7390* | A one-to-one mapping induces a one-to-one mapping on power sets. (Contributed by Stefan O'Rear, 18-Nov-2014.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹 “ 𝑏)):𝒫 𝐴–1-1-onto→𝒫 𝐵) | ||
Theorem | elovmpt3imp 7391* | If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands must be sets. Remark: a function which is the result of an operation can be regared as operation with 3 operands - therefore the abbreviation "mpt3" is used in the label. (Contributed by AV, 16-May-2019.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑧 ∈ 𝑀 ↦ 𝐵)) ⇒ ⊢ (𝐴 ∈ ((𝑋𝑂𝑌)‘𝑍) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) | ||
Theorem | ovmpt3rab1 7392* | The value of an operation defined by the maps-to notation with a function into a class abstraction as a result. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑧 ∈ 𝑀 ↦ {𝑎 ∈ 𝑁 ∣ 𝜑})) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑀 = 𝐾) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑁 = 𝐿) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈) → (𝑋𝑂𝑌) = (𝑧 ∈ 𝐾 ↦ {𝑎 ∈ 𝐿 ∣ 𝜓})) | ||
Theorem | ovmpt3rabdm 7393* | If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands and the argument of the function must be sets. (Contributed by AV, 16-May-2019.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑧 ∈ 𝑀 ↦ {𝑎 ∈ 𝑁 ∣ 𝜑})) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑀 = 𝐾) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑁 = 𝐿) ⇒ ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈) ∧ 𝐿 ∈ 𝑇) → dom (𝑋𝑂𝑌) = 𝐾) | ||
Theorem | elovmpt3rab1 7394* | Implications for the value of an operation defined by the maps-to notation with a function into a class abstraction as a result having an element. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑧 ∈ 𝑀 ↦ {𝑎 ∈ 𝑁 ∣ 𝜑})) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑀 = 𝐾) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑁 = 𝐿) ⇒ ⊢ ((𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇) → (𝐴 ∈ ((𝑋𝑂𝑌)‘𝑍) → ((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ (𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿)))) | ||
Theorem | elovmpt3rab 7395* | Implications for the value of an operation defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by AV, 17-Jul-2018.) (Revised by AV, 16-May-2019.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑧 ∈ 𝑀 ↦ {𝑎 ∈ 𝑁 ∣ 𝜑})) ⇒ ⊢ ((𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑇) → (𝐴 ∈ ((𝑋𝑂𝑌)‘𝑍) → ((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ (𝑍 ∈ 𝑀 ∧ 𝐴 ∈ 𝑁)))) | ||
Syntax | cof 7396 | Extend class notation to include mapping of an operation to a function operation. |
class ∘f 𝑅 | ||
Syntax | cofr 7397 | Extend class notation to include mapping of a binary relation to a function relation. |
class ∘r 𝑅 | ||
Definition | df-of 7398* | Define the function operation map. The definition is designed so that if 𝑅 is a binary operation, then ∘f 𝑅 is the analogous operation on functions which corresponds to applying 𝑅 pointwise to the values of the functions. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ ∘f 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥)))) | ||
Definition | df-ofr 7399* | Define the function relation map. The definition is designed so that if 𝑅 is a binary relation, then ∘r 𝑅 is the analogous relation on functions which is true when each element of the left function relates to the corresponding element of the right function. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ ∘r 𝑅 = {〈𝑓, 𝑔〉 ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)} | ||
Theorem | ofeq 7400 | Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝑅 = 𝑆 → ∘f 𝑅 = ∘f 𝑆) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |