HomeHome Intuitionistic Logic Explorer
Theorem List (p. 58 of 105)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 5701-5800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcaovdid 5701* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝐾𝑦𝑆𝑧𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧)))    &   (𝜑𝐴𝐾)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)       (𝜑 → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶)))
 
Theoremcaovdir2d 5702* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)))    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))       (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐶)))
 
Theoremcaovdirg 5703* Convert an operation reverse distributive law to class notation. (Contributed by Mario Carneiro, 19-Oct-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧)))       ((𝜑 ∧ (𝐴𝑆𝐵𝑆𝐶𝐾)) → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶)))
 
Theoremcaovdird 5704* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧)))    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝐾)       (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶)))
 
Theoremcaovdi 5705* Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))       (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐹(𝐴𝐺𝐶))
 
Theoremcaov32d 5706* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))       (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵))
 
Theoremcaov12d 5707* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))       (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶)))
 
Theoremcaov31d 5708* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))       (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴))
 
Theoremcaov13d 5709* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))       (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴)))
 
Theoremcaov4d 5710* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   (𝜑𝐷𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)       (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷)))
 
Theoremcaov411d 5711* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   (𝜑𝐷𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)       (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹𝐵)𝐹(𝐴𝐹𝐷)))
 
Theoremcaov42d 5712* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   (𝜑𝐷𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)       (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐷𝐹𝐵)))
 
Theoremcaov32 5713* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))       ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵)
 
Theoremcaov12 5714* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))       (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))
 
Theoremcaov31 5715* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))       ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴)
 
Theoremcaov13 5716* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))       (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴))
 
Theoremcaovdilemd 5717* Lemma used by real number construction. (Contributed by Jim Kingdon, 16-Sep-2019.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐹(𝑦𝐺𝑧)))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐺𝑦) ∈ 𝑆)    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   (𝜑𝐷𝑆)    &   (𝜑𝐻𝑆)       (𝜑 → (((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻) = ((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐵𝐺(𝐷𝐺𝐻))))
 
Theoremcaovlem2d 5718* Rearrangement of expression involving multiplication (𝐺) and addition (𝐹). (Contributed by Jim Kingdon, 3-Jan-2020.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐹(𝑦𝐺𝑧)))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐺𝑦) ∈ 𝑆)    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   (𝜑𝐷𝑆)    &   (𝜑𝐻𝑆)    &   (𝜑𝑅𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)       (𝜑 → ((((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻)𝐹(((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅)) = ((𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻)))))
 
Theoremcaovimo 5719* Uniqueness of inverse element in commutative, associative operation with identity. The identity element is 𝐵. (Contributed by Jim Kingdon, 18-Sep-2019.)
𝐵𝑆    &   ((𝑥𝑆𝑦𝑆) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝑥𝑆𝑦𝑆𝑧𝑆) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   (𝑥𝑆 → (𝑥𝐹𝐵) = 𝑥)       (𝐴𝑆 → ∃*𝑤(𝑤𝑆 ∧ (𝐴𝐹𝑤) = 𝐵))
 
Theoremgrprinvlem 5720* Lemma for grprinvd 5721. (Contributed by NM, 9-Aug-2013.)
((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   (𝜑𝑂𝐵)    &   ((𝜑𝑥𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ((𝜑𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 𝑂)    &   ((𝜑𝜓) → 𝑋𝐵)    &   ((𝜑𝜓) → (𝑋 + 𝑋) = 𝑋)       ((𝜑𝜓) → 𝑋 = 𝑂)
 
Theoremgrprinvd 5721* Deduce right inverse from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   (𝜑𝑂𝐵)    &   ((𝜑𝑥𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ((𝜑𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 𝑂)    &   ((𝜑𝜓) → 𝑋𝐵)    &   ((𝜑𝜓) → 𝑁𝐵)    &   ((𝜑𝜓) → (𝑁 + 𝑋) = 𝑂)       ((𝜑𝜓) → (𝑋 + 𝑁) = 𝑂)
 
Theoremgrpridd 5722* Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   (𝜑𝑂𝐵)    &   ((𝜑𝑥𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ((𝜑𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 𝑂)       ((𝜑𝑥𝐵) → (𝑥 + 𝑂) = 𝑥)
 
2.6.11  "Maps to" notation
 
Theoremelmpt2cl 5723* If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)
𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)       (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆𝐴𝑇𝐵))
 
Theoremelmpt2cl1 5724* 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.)
𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)       (𝑋 ∈ (𝑆𝐹𝑇) → 𝑆𝐴)
 
Theoremelmpt2cl2 5725* 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.)
𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)       (𝑋 ∈ (𝑆𝐹𝑇) → 𝑇𝐵)
 
Theoremelovmpt2 5726* Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.)
𝐷 = (𝑎𝐴, 𝑏𝐵𝐶)    &   𝐶 ∈ V    &   ((𝑎 = 𝑋𝑏 = 𝑌) → 𝐶 = 𝐸)       (𝐹 ∈ (𝑋𝐷𝑌) ↔ (𝑋𝐴𝑌𝐵𝐹𝐸))
 
Theoremf1ocnvd 5727* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
𝐹 = (𝑥𝐴𝐶)    &   ((𝜑𝑥𝐴) → 𝐶𝑊)    &   ((𝜑𝑦𝐵) → 𝐷𝑋)    &   (𝜑 → ((𝑥𝐴𝑦 = 𝐶) ↔ (𝑦𝐵𝑥 = 𝐷)))       (𝜑 → (𝐹:𝐴1-1-onto𝐵𝐹 = (𝑦𝐵𝐷)))
 
Theoremf1od 5728* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
𝐹 = (𝑥𝐴𝐶)    &   ((𝜑𝑥𝐴) → 𝐶𝑊)    &   ((𝜑𝑦𝐵) → 𝐷𝑋)    &   (𝜑 → ((𝑥𝐴𝑦 = 𝐶) ↔ (𝑦𝐵𝑥 = 𝐷)))       (𝜑𝐹:𝐴1-1-onto𝐵)
 
Theoremf1ocnv2d 5729* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
𝐹 = (𝑥𝐴𝐶)    &   ((𝜑𝑥𝐴) → 𝐶𝐵)    &   ((𝜑𝑦𝐵) → 𝐷𝐴)    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑥 = 𝐷𝑦 = 𝐶))       (𝜑 → (𝐹:𝐴1-1-onto𝐵𝐹 = (𝑦𝐵𝐷)))
 
Theoremf1o2d 5730* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
𝐹 = (𝑥𝐴𝐶)    &   ((𝜑𝑥𝐴) → 𝐶𝐵)    &   ((𝜑𝑦𝐵) → 𝐷𝐴)    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑥 = 𝐷𝑦 = 𝐶))       (𝜑𝐹:𝐴1-1-onto𝐵)
 
Theoremf1opw2 5731* A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw 5732 avoids the Axiom of Replacement. (Contributed by Mario Carneiro, 26-Jun-2015.)
(𝜑𝐹:𝐴1-1-onto𝐵)    &   (𝜑 → (𝐹𝑎) ∈ V)    &   (𝜑 → (𝐹𝑏) ∈ V)       (𝜑 → (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹𝑏)):𝒫 𝐴1-1-onto→𝒫 𝐵)
 
Theoremf1opw 5732* 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→𝒫 𝐵)
 
Theoremsuppssfv 5733* Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
(𝜑 → ((𝑥𝐷𝐴) “ (V ∖ {𝑌})) ⊆ 𝐿)    &   (𝜑 → (𝐹𝑌) = 𝑍)    &   ((𝜑𝑥𝐷) → 𝐴𝑉)       (𝜑 → ((𝑥𝐷 ↦ (𝐹𝐴)) “ (V ∖ {𝑍})) ⊆ 𝐿)
 
Theoremsuppssov1 5734* Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
(𝜑 → ((𝑥𝐷𝐴) “ (V ∖ {𝑌})) ⊆ 𝐿)    &   ((𝜑𝑣𝑅) → (𝑌𝑂𝑣) = 𝑍)    &   ((𝜑𝑥𝐷) → 𝐴𝑉)    &   ((𝜑𝑥𝐷) → 𝐵𝑅)       (𝜑 → ((𝑥𝐷 ↦ (𝐴𝑂𝐵)) “ (V ∖ {𝑍})) ⊆ 𝐿)
 
2.6.12  Function operation
 
Syntaxcof 5735 Extend class notation to include mapping of an operation to a function operation.
class 𝑓 𝑅
 
Syntaxcofr 5736 Extend class notation to include mapping of a binary relation to a function relation.
class 𝑟 𝑅
 
Definitiondf-of 5737* Define the function operation map. The definition is designed so that if 𝑅 is a binary operation, then 𝑓 𝑅 is the analogous operation on functions which corresponds to applying 𝑅 pointwise to the values of the functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓𝑥)𝑅(𝑔𝑥))))
 
Definitiondf-ofr 5738* Define the function relation map. The definition is designed so that if 𝑅 is a binary relation, then 𝑓 𝑅 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.)
𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
 
Theoremofeq 5739 Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
(𝑅 = 𝑆 → ∘𝑓 𝑅 = ∘𝑓 𝑆)
 
Theoremofreq 5740 Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝑅 = 𝑆 → ∘𝑟 𝑅 = ∘𝑟 𝑆)
 
Theoremofexg 5741 A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014.)
(𝐴𝑉 → ( ∘𝑓 𝑅𝐴) ∈ V)
 
Theoremnfof 5742* Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
𝑥𝑅       𝑥𝑓 𝑅
 
Theoremnfofr 5743* Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
𝑥𝑅       𝑥𝑟 𝑅
 
Theoremoffval 5744* Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝑆    &   ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐶)    &   ((𝜑𝑥𝐵) → (𝐺𝑥) = 𝐷)       (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝑆 ↦ (𝐶𝑅𝐷)))
 
Theoremofrfval 5745* Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝑆    &   ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐶)    &   ((𝜑𝑥𝐵) → (𝐺𝑥) = 𝐷)       (𝜑 → (𝐹𝑟 𝑅𝐺 ↔ ∀𝑥𝑆 𝐶𝑅𝐷))
 
Theoremfnofval 5746 Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝑆    &   ((𝜑𝑋𝐴) → (𝐹𝑋) = 𝐶)    &   ((𝜑𝑋𝐵) → (𝐺𝑋) = 𝐷)    &   (𝜑𝑅 Fn (𝑈 × 𝑉))    &   (𝜑𝐶𝑈)    &   (𝜑𝐷𝑉)       ((𝜑𝑋𝑆) → ((𝐹𝑓 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷))
 
Theoremofrval 5747 Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝑆    &   ((𝜑𝑋𝐴) → (𝐹𝑋) = 𝐶)    &   ((𝜑𝑋𝐵) → (𝐺𝑋) = 𝐷)       ((𝜑𝐹𝑟 𝑅𝐺𝑋𝑆) → 𝐶𝑅𝐷)
 
Theoremofmresval 5748 Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
(𝜑𝐹𝐴)    &   (𝜑𝐺𝐵)       (𝜑 → (𝐹( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵))𝐺) = (𝐹𝑓 𝑅𝐺))
 
Theoremoff 5749* The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   (𝜑𝐹:𝐴𝑆)    &   (𝜑𝐺:𝐵𝑇)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝐶       (𝜑 → (𝐹𝑓 𝑅𝐺):𝐶𝑈)
 
Theoremofres 5750 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 𝐵)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝐶       (𝜑 → (𝐹𝑓 𝑅𝐺) = ((𝐹𝐶) ∘𝑓 𝑅(𝐺𝐶)))
 
Theoremoffval2 5751* The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.)
(𝜑𝐴𝑉)    &   ((𝜑𝑥𝐴) → 𝐵𝑊)    &   ((𝜑𝑥𝐴) → 𝐶𝑋)    &   (𝜑𝐹 = (𝑥𝐴𝐵))    &   (𝜑𝐺 = (𝑥𝐴𝐶))       (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝐴 ↦ (𝐵𝑅𝐶)))
 
Theoremofrfval2 5752* The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.)
(𝜑𝐴𝑉)    &   ((𝜑𝑥𝐴) → 𝐵𝑊)    &   ((𝜑𝑥𝐴) → 𝐶𝑋)    &   (𝜑𝐹 = (𝑥𝐴𝐵))    &   (𝜑𝐺 = (𝑥𝐴𝐶))       (𝜑 → (𝐹𝑟 𝑅𝐺 ↔ ∀𝑥𝐴 𝐵𝑅𝐶))
 
Theoremsuppssof1 5753* Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
(𝜑 → (𝐴 “ (V ∖ {𝑌})) ⊆ 𝐿)    &   ((𝜑𝑣𝑅) → (𝑌𝑂𝑣) = 𝑍)    &   (𝜑𝐴:𝐷𝑉)    &   (𝜑𝐵:𝐷𝑅)    &   (𝜑𝐷𝑊)       (𝜑 → ((𝐴𝑓 𝑂𝐵) “ (V ∖ {𝑍})) ⊆ 𝐿)
 
Theoremofco 5754 The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐻:𝐷𝐶)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝜑𝐷𝑋)    &   (𝐴𝐵) = 𝐶       (𝜑 → ((𝐹𝑓 𝑅𝐺) ∘ 𝐻) = ((𝐹𝐻) ∘𝑓 𝑅(𝐺𝐻)))
 
Theoremoffveqb 5755* 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 𝐴)    &   ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)    &   ((𝜑𝑥𝐴) → (𝐺𝑥) = 𝐶)       (𝜑 → (𝐻 = (𝐹𝑓 𝑅𝐺) ↔ ∀𝑥𝐴 (𝐻𝑥) = (𝐵𝑅𝐶)))
 
Theoremofc12 5756 Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝜑𝐶𝑋)       (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 𝑅(𝐴 × {𝐶})) = (𝐴 × {(𝐵𝑅𝐶)}))
 
Theoremcaofref 5757* Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝜑𝐴𝑉)    &   (𝜑𝐹:𝐴𝑆)    &   ((𝜑𝑥𝑆) → 𝑥𝑅𝑥)       (𝜑𝐹𝑟 𝑅𝐹)
 
Theoremcaofinvl 5758* Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.)
(𝜑𝐴𝑉)    &   (𝜑𝐹:𝐴𝑆)    &   (𝜑𝐵𝑊)    &   (𝜑𝑁:𝑆𝑆)    &   (𝜑𝐺 = (𝑣𝐴 ↦ (𝑁‘(𝐹𝑣))))    &   ((𝜑𝑥𝑆) → ((𝑁𝑥)𝑅𝑥) = 𝐵)       (𝜑 → (𝐺𝑓 𝑅𝐹) = (𝐴 × {𝐵}))
 
Theoremcaofcom 5759* Transfer a commutative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.)
(𝜑𝐴𝑉)    &   (𝜑𝐹:𝐴𝑆)    &   (𝜑𝐺:𝐴𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝑅𝑦) = (𝑦𝑅𝑥))       (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝐺𝑓 𝑅𝐹))
 
Theoremcaofrss 5760* Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝜑𝐴𝑉)    &   (𝜑𝐹:𝐴𝑆)    &   (𝜑𝐺:𝐴𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝑅𝑦𝑥𝑇𝑦))       (𝜑 → (𝐹𝑟 𝑅𝐺𝐹𝑟 𝑇𝐺))
 
Theoremcaoftrn 5761* Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝜑𝐴𝑉)    &   (𝜑𝐹:𝐴𝑆)    &   (𝜑𝐺:𝐴𝑆)    &   (𝜑𝐻:𝐴𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝑅𝑦𝑦𝑇𝑧) → 𝑥𝑈𝑧))       (𝜑 → ((𝐹𝑟 𝑅𝐺𝐺𝑟 𝑇𝐻) → 𝐹𝑟 𝑈𝐻))
 
2.6.13  Functions (continued)
 
TheoremresfunexgALT 5762 The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. This version has a shorter proof than resfunexg 5407 but requires ax-pow 3952 and ax-un 4195. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
((Fun 𝐴𝐵𝐶) → (𝐴𝐵) ∈ V)
 
Theoremcofunexg 5763 Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.)
((Fun 𝐴𝐵𝐶) → (𝐴𝐵) ∈ V)
 
Theoremcofunex2g 5764 Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.)
((𝐴𝑉 ∧ Fun 𝐵) → (𝐴𝐵) ∈ V)
 
TheoremfnexALT 5765 If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of funimaexg 5008. This version of fnex 5408 uses ax-pow 3952 and ax-un 4195, whereas fnex 5408 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝐹 Fn 𝐴𝐴𝐵) → 𝐹 ∈ V)
 
Theoremfunrnex 5766 If the domain of a function exists, so does its range. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of funex 5409. (Contributed by NM, 11-Nov-1995.)
(dom 𝐹𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V))
 
Theoremfornex 5767 If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.)
(𝐴𝐶 → (𝐹:𝐴onto𝐵𝐵 ∈ V))
 
Theoremf1dmex 5768 If the codomain of a one-to-one function exists, so does its domain. This can be thought of as a form of the Axiom of Replacement. (Contributed by NM, 4-Sep-2004.)
((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐴 ∈ V)
 
Theoremabrexex 5769* Existence of a class abstraction of existentially restricted sets. 𝑥 is normally a free-variable parameter in the class expression substituted for 𝐵, which can be thought of as 𝐵(𝑥). This simple-looking theorem is actually quite powerful and appears to involve the Axiom of Replacement in an intrinsic way, as can be seen by tracing back through the path mptexg 5411, funex 5409, fnex 5408, resfunexg 5407, and funimaexg 5008. See also abrexex2 5776. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
𝐴 ∈ V       {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V
 
Theoremabrexexg 5770* Existence of a class abstraction of existentially restricted sets. 𝑥 is normally a free-variable parameter in 𝐵. The antecedent assures us that 𝐴 is a set. (Contributed by NM, 3-Nov-2003.)
(𝐴𝑉 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
 
Theoremiunexg 5771* The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.)
((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → 𝑥𝐴 𝐵 ∈ V)
 
Theoremabrexex2g 5772* Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
((𝐴𝑉 ∧ ∀𝑥𝐴 {𝑦𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥𝐴 𝜑} ∈ V)
 
Theoremopabex3d 5773* Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017.)
(𝜑𝐴 ∈ V)    &   ((𝜑𝑥𝐴) → {𝑦𝜓} ∈ V)       (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝜓)} ∈ V)
 
Theoremopabex3 5774* Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
𝐴 ∈ V    &   (𝑥𝐴 → {𝑦𝜑} ∈ V)       {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝜑)} ∈ V
 
Theoremiunex 5775* The existence of an indexed union. 𝑥 is normally a free-variable parameter in the class expression substituted for 𝐵, which can be read informally as 𝐵(𝑥). (Contributed by NM, 13-Oct-2003.)
𝐴 ∈ V    &   𝐵 ∈ V        𝑥𝐴 𝐵 ∈ V
 
Theoremabrexex2 5776* Existence of an existentially restricted class abstraction. 𝜑 is normally has free-variable parameters 𝑥 and 𝑦. See also abrexex 5769. (Contributed by NM, 12-Sep-2004.)
𝐴 ∈ V    &   {𝑦𝜑} ∈ V       {𝑦 ∣ ∃𝑥𝐴 𝜑} ∈ V
 
Theoremabexssex 5777* Existence of a class abstraction with an existentially quantified expression. Both 𝑥 and 𝑦 can be free in 𝜑. (Contributed by NM, 29-Jul-2006.)
𝐴 ∈ V    &   {𝑦𝜑} ∈ V       {𝑦 ∣ ∃𝑥(𝑥𝐴𝜑)} ∈ V
 
Theoremabexex 5778* A condition where a class builder continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007.)
𝐴 ∈ V    &   (𝜑𝑥𝐴)    &   {𝑦𝜑} ∈ V       {𝑦 ∣ ∃𝑥𝜑} ∈ V
 
Theoremoprabexd 5779* Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
(𝜑𝐴 ∈ V)    &   (𝜑𝐵 ∈ V)    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → ∃*𝑧𝜓)    &   (𝜑𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜓)})       (𝜑𝐹 ∈ V)
 
Theoremoprabex 5780* Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.)
𝐴 ∈ V    &   𝐵 ∈ V    &   ((𝑥𝐴𝑦𝐵) → ∃*𝑧𝜑)    &   𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜑)}       𝐹 ∈ V
 
Theoremoprabex3 5781* Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.)
𝐻 ∈ V    &   𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}       𝐹 ∈ V
 
Theoremoprabrexex2 5782* Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.)
𝐴 ∈ V    &   {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ∈ V       {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑤𝐴 𝜑} ∈ V
 
Theoremab2rexex 5783* Existence of a class abstraction of existentially restricted sets. Variables 𝑥 and 𝑦 are normally free-variable parameters in the class expression substituted for 𝐶, which can be thought of as 𝐶(𝑥, 𝑦). See comments for abrexex 5769. (Contributed by NM, 20-Sep-2011.)
𝐴 ∈ V    &   𝐵 ∈ V       {𝑧 ∣ ∃𝑥𝐴𝑦𝐵 𝑧 = 𝐶} ∈ V
 
Theoremab2rexex2 5784* Existence of an existentially restricted class abstraction. 𝜑 normally has free-variable parameters 𝑥, 𝑦, and 𝑧. Compare abrexex2 5776. (Contributed by NM, 20-Sep-2011.)
𝐴 ∈ V    &   𝐵 ∈ V    &   {𝑧𝜑} ∈ V       {𝑧 ∣ ∃𝑥𝐴𝑦𝐵 𝜑} ∈ V
 
TheoremxpexgALT 5785 The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. This version is proven using Replacement; see xpexg 4477 for a version that uses the Power Set axiom instead. (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
 
Theoremoffval3 5786* General value of (𝐹𝑓 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.)
((𝐹𝑉𝐺𝑊) → (𝐹𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
 
Theoremoffres 5787 Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.)
((𝐹𝑉𝐺𝑊) → ((𝐹𝑓 𝑅𝐺) ↾ 𝐷) = ((𝐹𝐷) ∘𝑓 𝑅(𝐺𝐷)))
 
Theoremofmres 5788* Equivalent expressions for a restriction of the function operation map. Unlike 𝑓 𝑅 which is a proper class, ( ∘𝑓 𝑅 ∣ ‘(𝐴 × 𝐵)) can be a set by ofmresex 5789, allowing it to be used as a function or structure argument. By ofmresval 5748, the restricted operation map values are the same as the original values, allowing theorems for 𝑓 𝑅 to be reused. (Contributed by NM, 20-Oct-2014.)
( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) = (𝑓𝐴, 𝑔𝐵 ↦ (𝑓𝑓 𝑅𝑔))
 
Theoremofmresex 5789 Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
(𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)       (𝜑 → ( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) ∈ V)
 
2.6.14  First and second members of an ordered pair
 
Syntaxc1st 5790 Extend the definition of a class to include the first member an ordered pair function.
class 1st
 
Syntaxc2nd 5791 Extend the definition of a class to include the second member an ordered pair function.
class 2nd
 
Definitiondf-1st 5792 Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 5798 proves that it does this. For example, (1st ‘⟨ 3 , 4 ) = 3 . Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 4827 and op1stb 4234). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
1st = (𝑥 ∈ V ↦ dom {𝑥})
 
Definitiondf-2nd 5793 Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 5799 proves that it does this. For example, (2nd ‘⟨ 3 , 4 ) = 4 . Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 4830 and op2ndb 4829). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
2nd = (𝑥 ∈ V ↦ ran {𝑥})
 
Theorem1stvalg 5794 The value of the function that extracts the first member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
(𝐴 ∈ V → (1st𝐴) = dom {𝐴})
 
Theorem2ndvalg 5795 The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
(𝐴 ∈ V → (2nd𝐴) = ran {𝐴})
 
Theorem1st0 5796 The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
(1st ‘∅) = ∅
 
Theorem2nd0 5797 The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
(2nd ‘∅) = ∅
 
Theoremop1st 5798 Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
𝐴 ∈ V    &   𝐵 ∈ V       (1st ‘⟨𝐴, 𝐵⟩) = 𝐴
 
Theoremop2nd 5799 Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
𝐴 ∈ V    &   𝐵 ∈ V       (2nd ‘⟨𝐴, 𝐵⟩) = 𝐵
 
Theoremop1std 5800 Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
𝐴 ∈ V    &   𝐵 ∈ V       (𝐶 = ⟨𝐴, 𝐵⟩ → (1st𝐶) = 𝐴)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10454
  Copyright terms: Public domain < Previous  Next >