![]() |
Metamath
Proof Explorer Theorem List (p. 77 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | caovcl 7601* | Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.) |
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆) | ||
Theorem | caovcomg 7602* | Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) | ||
Theorem | caovcomd 7603* | Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) | ||
Theorem | caovcom 7604* | 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 7605* | Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro, 26-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) | ||
Theorem | caovassd 7606* | Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) | ||
Theorem | caovass 7607* | 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 7608* | Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | caovcand 7609* | Convert an operation cancellation law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | caovcanrd 7610* | Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ (𝜑 → ((𝐵𝐹𝐴) = (𝐶𝐹𝐴) ↔ 𝐵 = 𝐶)) | ||
Theorem | caovcan 7611* | Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) |
⊢ 𝐶 ∈ V & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) → 𝐵 = 𝐶)) | ||
Theorem | caovordig 7612* | Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | caovordid 7613* | Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | caovordg 7614* | Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | caovordd 7615* | Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | caovord2d 7616* | Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶))) | ||
Theorem | caovord3d 7617* | Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐶𝐹𝐷) → (𝐴𝑅𝐶 ↔ 𝐷𝑅𝐵))) | ||
Theorem | caovord 7618* | Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) | ||
Theorem | caovord2 7619* | Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) ⇒ ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶))) | ||
Theorem | caovord3 7620* | Ordering law. (Contributed by NM, 29-Feb-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ 𝐷 ∈ V ⇒ ⊢ (((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴𝐹𝐵) = (𝐶𝐹𝐷)) → (𝐴𝑅𝐶 ↔ 𝐷𝑅𝐵)) | ||
Theorem | caovdig 7621* | Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶))) | ||
Theorem | caovdid 7622* | Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶))) | ||
Theorem | caovdir2d 7623* | Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐶))) | ||
Theorem | caovdirg 7624* | Convert an operation reverse distributive law to class notation. (Contributed by Mario Carneiro, 19-Oct-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐾)) → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶))) | ||
Theorem | caovdird 7625* | Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶))) | ||
Theorem | caovdi 7626* | 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 7627* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵)) | ||
Theorem | caov12d 7628* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))) | ||
Theorem | caov31d 7629* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴)) | ||
Theorem | caov13d 7630* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴))) | ||
Theorem | caov4d 7631* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷))) | ||
Theorem | caov411d 7632* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹𝐵)𝐹(𝐴𝐹𝐷))) | ||
Theorem | caov42d 7633* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐷𝐹𝐵))) | ||
Theorem | caov32 7634* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵) | ||
Theorem | caov12 7635* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶)) | ||
Theorem | caov31 7636* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴) | ||
Theorem | caov13 7637* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴)) | ||
Theorem | caov4 7638* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) & ⊢ 𝐷 ∈ V ⇒ ⊢ ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷)) | ||
Theorem | caov411 7639* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) & ⊢ 𝐷 ∈ V ⇒ ⊢ ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹𝐵)𝐹(𝐴𝐹𝐷)) | ||
Theorem | caov42 7640* | Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) & ⊢ 𝐷 ∈ V ⇒ ⊢ ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐷𝐹𝐵)) | ||
Theorem | caovdir 7641* | Reverse distributive law. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥) & ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐶)) | ||
Theorem | caovdilem 7642* | Lemma used by real number construction. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥) & ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)) & ⊢ 𝐷 ∈ V & ⊢ 𝐻 ∈ V & ⊢ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ⇒ ⊢ (((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻) = ((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐵𝐺(𝐷𝐺𝐻))) | ||
Theorem | caovlem2 7643* | Lemma used in real number construction. (Contributed by NM, 26-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥) & ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)) & ⊢ 𝐷 ∈ V & ⊢ 𝐻 ∈ V & ⊢ ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) & ⊢ 𝑅 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻)𝐹(((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅)) = ((𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻)))) | ||
Theorem | caovmo 7644* | 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 | imaeqexov 7645* | Substitute an operation value into an existential quantifier over an image. (Contributed by Scott Fenton, 20-Jan-2025.) |
⊢ (𝑥 = (𝑦𝐹𝑧) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ (𝐵 × 𝐶) ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ (𝐵 × 𝐶))𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜓)) | ||
Theorem | imaeqalov 7646* | Substitute an operation value into a universal quantifier over an image. (Contributed by Scott Fenton, 20-Jan-2025.) |
⊢ (𝑥 = (𝑦𝐹𝑧) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ (𝐵 × 𝐶) ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ (𝐵 × 𝐶))𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)) | ||
Theorem | mpondm0 7647* | 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 7648* | If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵)) | ||
Theorem | elmpocl1 7649* | 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 7650* | 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 7651* |
Utility lemma for two-parameter classes.
EDITORIAL: can simplify isghm 19092, islmhm 20638. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐷 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐶 ∈ V & ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → 𝐶 = 𝐸) ⇒ ⊢ (𝐹 ∈ (𝑋𝐷𝑌) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 ∈ 𝐸)) | ||
Theorem | elovmporab 7652* | 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 7653* | 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. Version of elovmporab1 7654 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Alexander van der Vekens, 15-Jul-2018.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑍 ∈ (𝑋𝑂𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋𝑋 / 𝑚⦌𝑀)) | ||
Theorem | elovmporab1 7654* | 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. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker elovmporab1w 7653 when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (New usage is discouraged.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑍 ∈ (𝑋𝑂𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋𝑋 / 𝑚⦌𝑀)) | ||
Theorem | 2mpo0 7655* | 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 7656* | 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 7657* | Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) | ||
Theorem | f1od 7658* | Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | f1ocnv2d 7659* | Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) | ||
Theorem | f1o2d 7660* | Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | f1opw2 7661* | A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw 7662 avoids the Axiom of Replacement. (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → (◡𝐹 “ 𝑎) ∈ V) & ⊢ (𝜑 → (𝐹 “ 𝑏) ∈ V) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹 “ 𝑏)):𝒫 𝐴–1-1-onto→𝒫 𝐵) | ||
Theorem | f1opw 7662* | 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 7663* | 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 7664* | 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 7665* | 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 7666* | 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 7667* | 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 7668 | Extend class notation to include mapping of an operation to a function operation. |
class ∘f 𝑅 | ||
Syntax | cofr 7669 | Extend class notation to include mapping of a binary relation to a function relation. |
class ∘r 𝑅 | ||
Definition | df-of 7670* | 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 7671* | 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 | ofeqd 7672 | Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ∘f 𝑅 = ∘f 𝑆) | ||
Theorem | ofeq 7673 | Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝑅 = 𝑆 → ∘f 𝑅 = ∘f 𝑆) | ||
Theorem | ofreq 7674 | Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝑅 = 𝑆 → ∘r 𝑅 = ∘r 𝑆) | ||
Theorem | ofexg 7675 | A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → ( ∘f 𝑅 ↾ 𝐴) ∈ V) | ||
Theorem | nfof 7676 | Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘f 𝑅 | ||
Theorem | nfofr 7677 | Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘r 𝑅 | ||
Theorem | ofrfvalg 7678* | Value of a relation applied to two functions. Originally part of ofrfval 7680, this version assumes the functions are sets rather than their domains, avoiding ax-rep 5286. (Contributed by SN, 5-Aug-2024.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝑆 𝐶𝑅𝐷)) | ||
Theorem | offval 7679* | Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷))) | ||
Theorem | ofrfval 7680* | Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝑆 𝐶𝑅𝐷)) | ||
Theorem | ofval 7681 | Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷)) | ||
Theorem | ofrval 7682 | Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∘r 𝑅𝐺 ∧ 𝑋 ∈ 𝑆) → 𝐶𝑅𝐷) | ||
Theorem | offn 7683 | The function operation produces a function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) Fn 𝑆) | ||
Theorem | offun 7684 | The function operation produces a function. (Contributed by SN, 23-Jul-2024.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → Fun (𝐹 ∘f 𝑅𝐺)) | ||
Theorem | offval2f 7685* | The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 23-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofmresval 7686 | Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹( ∘f 𝑅 ↾ (𝐴 × 𝐵))𝐺) = (𝐹 ∘f 𝑅𝐺)) | ||
Theorem | fnfvof 7687 | Function value of a pointwise composition. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Jun-2015.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋))) | ||
Theorem | off 7688* | The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) | ||
Theorem | ofres 7689 | Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = ((𝐹 ↾ 𝐶) ∘f 𝑅(𝐺 ↾ 𝐶))) | ||
Theorem | offval2 7690* | The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofrfval2 7691* | The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶)) | ||
Theorem | ofmpteq 7692* | Value of a pointwise operation on two functions defined using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∘f 𝑅(𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofco 7693 | The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐻:𝐷⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘f 𝑅(𝐺 ∘ 𝐻))) | ||
Theorem | offveq 7694* | Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ (𝜑 → 𝐻 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵𝑅𝐶) = (𝐻‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = 𝐻) | ||
Theorem | offveqb 7695* | Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ (𝜑 → 𝐻 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶) ⇒ ⊢ (𝜑 → (𝐻 = (𝐹 ∘f 𝑅𝐺) ↔ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐵𝑅𝐶))) | ||
Theorem | ofc1 7696 | Left operation by a constant. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (((𝐴 × {𝐵}) ∘f 𝑅𝐹)‘𝑋) = (𝐵𝑅𝐶)) | ||
Theorem | ofc2 7697 | Right operation by a constant. (Contributed by NM, 7-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘f 𝑅(𝐴 × {𝐵}))‘𝑋) = (𝐶𝑅𝐵)) | ||
Theorem | ofc12 7698 | Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅(𝐴 × {𝐶})) = (𝐴 × {(𝐵𝑅𝐶)})) | ||
Theorem | caofref 7699* | Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥𝑅𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∘r 𝑅𝐹) | ||
Theorem | caofinvl 7700* | Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑁:𝑆⟶𝑆) & ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∘f 𝑅𝐹) = (𝐴 × {𝐵})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |