Theorem List for Intuitionistic Logic Explorer - 5901-6000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | caovdird 5901* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶))) |
|
Theorem | caovdi 5902* |
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 5903* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵)) |
|
Theorem | caov12d 5904* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))) |
|
Theorem | caov31d 5905* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴)) |
|
Theorem | caov13d 5906* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴))) |
|
Theorem | caov4d 5907* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷))) |
|
Theorem | caov411d 5908* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹𝐵)𝐹(𝐴𝐹𝐷))) |
|
Theorem | caov42d 5909* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐷𝐹𝐵))) |
|
Theorem | caov32 5910* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
& ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵) |
|
Theorem | caov12 5911* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
& ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶)) |
|
Theorem | caov31 5912* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
& ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴) |
|
Theorem | caov13 5913* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
& ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴)) |
|
Theorem | caovdilemd 5914* |
Lemma used by real number construction. (Contributed by Jim Kingdon,
16-Sep-2019.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐹(𝑦𝐺𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) ∈ 𝑆)
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ (𝜑 → 𝐷 ∈ 𝑆)
& ⊢ (𝜑 → 𝐻 ∈ 𝑆) ⇒ ⊢ (𝜑 → (((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻) = ((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐵𝐺(𝐷𝐺𝐻)))) |
|
Theorem | caovlem2d 5915* |
Rearrangement of expression involving multiplication (𝐺) and
addition (𝐹). (Contributed by Jim Kingdon,
3-Jan-2020.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐹(𝑦𝐺𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) ∈ 𝑆)
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ (𝜑 → 𝐷 ∈ 𝑆)
& ⊢ (𝜑 → 𝐻 ∈ 𝑆)
& ⊢ (𝜑 → 𝑅 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻)𝐹(((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅)) = ((𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻))))) |
|
Theorem | caovimo 5916* |
Uniqueness of inverse element in commutative, associative operation with
identity. The identity element is 𝐵. (Contributed by Jim Kingdon,
18-Sep-2019.)
|
⊢ 𝐵 ∈ 𝑆
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝑥 ∈ 𝑆 → (𝑥𝐹𝐵) = 𝑥) ⇒ ⊢ (𝐴 ∈ 𝑆 → ∃*𝑤(𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵)) |
|
Theorem | grprinvlem 5917* |
Lemma for grprinvd 5918. (Contributed by NM, 9-Aug-2013.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
& ⊢ (𝜑 → 𝑂 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂)
& ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝜓) → (𝑋 + 𝑋) = 𝑋) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝑋 = 𝑂) |
|
Theorem | grprinvd 5918* |
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.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
& ⊢ (𝜑 → 𝑂 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂)
& ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝜓) → (𝑁 + 𝑋) = 𝑂) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑋 + 𝑁) = 𝑂) |
|
Theorem | grpridd 5919* |
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
|
|
Theorem | elmpocl 5920* |
If a two-parameter class is inhabited, constrain the implicit pair.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵)) |
|
Theorem | elmpocl1 5921* |
If a two-parameter class is inhabited, the first argument is in its
nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan
O'Rear, 7-Mar-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → 𝑆 ∈ 𝐴) |
|
Theorem | elmpocl2 5922* |
If a two-parameter class is inhabited, the second argument is in its
nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan
O'Rear, 7-Mar-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → 𝑇 ∈ 𝐵) |
|
Theorem | elovmpo 5923* |
Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear,
21-Jan-2015.)
|
⊢ 𝐷 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)
& ⊢ 𝐶 ∈ V & ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → 𝐶 = 𝐸) ⇒ ⊢ (𝐹 ∈ (𝑋𝐷𝑌) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 ∈ 𝐸)) |
|
Theorem | f1ocnvd 5924* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑋)
& ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) |
|
Theorem | f1od 5925* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑋)
& ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |
|
Theorem | f1ocnv2d 5926* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) |
|
Theorem | f1o2d 5927* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |
|
Theorem | f1opw2 5928* |
A one-to-one mapping induces a one-to-one mapping on power sets. This
version of f1opw 5929 avoids the Axiom of Replacement.
(Contributed by
Mario Carneiro, 26-Jun-2015.)
|
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
& ⊢ (𝜑 → (◡𝐹 “ 𝑎) ∈ V) & ⊢ (𝜑 → (𝐹 “ 𝑏) ∈ V) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹 “ 𝑏)):𝒫 𝐴–1-1-onto→𝒫 𝐵) |
|
Theorem | f1opw 5929* |
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 | suppssfv 5930* |
Formula building theorem for support restriction, on a function which
preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ 𝐴) “ (V ∖ {𝑌})) ⊆ 𝐿)
& ⊢ (𝜑 → (𝐹‘𝑌) = 𝑍)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) “ (V ∖ {𝑍})) ⊆ 𝐿) |
|
Theorem | suppssov1 5931* |
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
|
|
Syntax | cof 5932 |
Extend class notation to include mapping of an operation to a function
operation.
|
class ∘𝑓 𝑅 |
|
Syntax | cofr 5933 |
Extend class notation to include mapping of a binary relation to a
function relation.
|
class ∘𝑟 𝑅 |
|
Definition | df-of 5934* |
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 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥)))) |
|
Definition | df-ofr 5935* |
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 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)} |
|
Theorem | ofeq 5936 |
Equality theorem for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ (𝑅 = 𝑆 → ∘𝑓 𝑅 = ∘𝑓
𝑆) |
|
Theorem | ofreq 5937 |
Equality theorem for function relation. (Contributed by Mario Carneiro,
28-Jul-2014.)
|
⊢ (𝑅 = 𝑆 → ∘𝑟 𝑅 = ∘𝑟
𝑆) |
|
Theorem | ofexg 5938 |
A function operation restricted to a set is a set. (Contributed by NM,
28-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → ( ∘𝑓 𝑅 ↾ 𝐴) ∈ V) |
|
Theorem | nfof 5939 |
Hypothesis builder for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘𝑓
𝑅 |
|
Theorem | nfofr 5940 |
Hypothesis builder for function relation. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘𝑟
𝑅 |
|
Theorem | offval 5941* |
Value of an operation applied to two functions. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷))) |
|
Theorem | ofrfval 5942* |
Value of a relation applied to two functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀𝑥 ∈ 𝑆 𝐶𝑅𝐷)) |
|
Theorem | ofvalg 5943 |
Evaluate a function operation at a point. (Contributed by Mario
Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷)
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐶𝑅𝐷) ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘𝑓 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷)) |
|
Theorem | ofrval 5944 |
Exhibit a function relation at a point. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∘𝑟 𝑅𝐺 ∧ 𝑋 ∈ 𝑆) → 𝐶𝑅𝐷) |
|
Theorem | ofmresval 5945 |
Value of a restriction of the function operation map. (Contributed by
NM, 20-Oct-2014.)
|
⊢ (𝜑 → 𝐹 ∈ 𝐴)
& ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵))𝐺) = (𝐹 ∘𝑓 𝑅𝐺)) |
|
Theorem | off 5946* |
The function operation produces a function. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺):𝐶⟶𝑈) |
|
Theorem | offeq 5947* |
Convert an identity of the operation to the analogous identity on
the function operation. (Contributed by Jim Kingdon,
26-Nov-2023.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶
& ⊢ (𝜑 → 𝐻:𝐶⟶𝑈)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐷)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐸)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐷𝑅𝐸) = (𝐻‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = 𝐻) |
|
Theorem | ofres 5948 |
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 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = ((𝐹 ↾ 𝐶) ∘𝑓 𝑅(𝐺 ↾ 𝐶))) |
|
Theorem | offval2 5949* |
The function operation expressed as a mapping. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) |
|
Theorem | ofrfval2 5950* |
The function relation acting on maps. (Contributed by Mario Carneiro,
20-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶)) |
|
Theorem | suppssof1 5951* |
Formula building theorem for support restrictions: vector operation with
left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ (𝜑 → (◡𝐴 “ (V ∖ {𝑌})) ⊆ 𝐿)
& ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)
& ⊢ (𝜑 → 𝐴:𝐷⟶𝑉)
& ⊢ (𝜑 → 𝐵:𝐷⟶𝑅)
& ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (◡(𝐴 ∘𝑓 𝑂𝐵) “ (V ∖ {𝑍})) ⊆ 𝐿) |
|
Theorem | ofco 5952 |
The composition of a function operation with another function.
(Contributed by Mario Carneiro, 19-Dec-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐻:𝐷⟶𝐶)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐷 ∈ 𝑋)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → ((𝐹 ∘𝑓 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘𝑓 𝑅(𝐺 ∘ 𝐻))) |
|
Theorem | offveqb 5953* |
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 𝐴)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶) ⇒ ⊢ (𝜑 → (𝐻 = (𝐹 ∘𝑓 𝑅𝐺) ↔ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐵𝑅𝐶))) |
|
Theorem | ofc12 5954 |
Function operation on two constant functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 𝑅(𝐴 × {𝐶})) = (𝐴 × {(𝐵𝑅𝐶)})) |
|
Theorem | caofref 5955* |
Transfer a reflexive law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥𝑅𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∘𝑟 𝑅𝐹) |
|
Theorem | caofinvl 5956* |
Transfer a left inverse law to the function operation. (Contributed
by NM, 22-Oct-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝑁:𝑆⟶𝑆)
& ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 𝑅𝐹) = (𝐴 × {𝐵})) |
|
Theorem | caofcom 5957* |
Transfer a commutative law to the function operation. (Contributed by
Mario Carneiro, 26-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦) = (𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝐺 ∘𝑓 𝑅𝐹)) |
|
Theorem | caofrss 5958* |
Transfer a relation subset law to the function relation. (Contributed
by Mario Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦 → 𝑥𝑇𝑦)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 → 𝐹 ∘𝑟 𝑇𝐺)) |
|
Theorem | caoftrn 5959* |
Transfer a transitivity law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐻:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧)) ⇒ ⊢ (𝜑 → ((𝐹 ∘𝑟 𝑅𝐺 ∧ 𝐺 ∘𝑟 𝑇𝐻) → 𝐹 ∘𝑟 𝑈𝐻)) |
|
2.6.13 Functions (continued)
|
|
Theorem | resfunexgALT 5960 |
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 5593 but requires ax-pow 4056 and ax-un 4313. (Contributed by NM,
7-Apr-1995.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) |
|
Theorem | cofunexg 5961 |
Existence of a composition when the first member is a function.
(Contributed by NM, 8-Oct-2007.)
|
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V) |
|
Theorem | cofunex2g 5962 |
Existence of a composition when the second member is one-to-one.
(Contributed by NM, 8-Oct-2007.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V) |
|
Theorem | fnexALT 5963 |
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 5163. This version of fnex 5594
uses
ax-pow 4056 and ax-un 4313, whereas fnex 5594
does not. (Contributed by NM,
14-Aug-1994.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) |
|
Theorem | funrnex 5964 |
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 5595. (Contributed by NM, 11-Nov-1995.)
|
⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V)) |
|
Theorem | fornex 5965 |
If the domain of an onto function exists, so does its codomain.
(Contributed by NM, 23-Jul-2004.)
|
⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V)) |
|
Theorem | f1dmex 5966 |
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) |
|
Theorem | abrexex 5967* |
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 5597, funex 5595, fnex 5594, resfunexg 5593, and
funimaexg 5163. See also abrexex2 5974. (Contributed by NM, 16-Oct-2003.)
(Proof shortened by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V |
|
Theorem | abrexexg 5968* |
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) |
|
Theorem | iunexg 5969* |
The existence of an indexed union. 𝑥 is normally a free-variable
parameter in 𝐵. (Contributed by NM, 23-Mar-2006.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
|
Theorem | abrexex2g 5970* |
Existence of an existentially restricted class abstraction.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V) |
|
Theorem | opabex3d 5971* |
Existence of an ordered pair abstraction, deduction version.
(Contributed by Alexander van der Vekens, 19-Oct-2017.)
|
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝜓} ∈ V) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ∈ V) |
|
Theorem | opabex3 5972* |
Existence of an ordered pair abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V |
|
Theorem | iunex 5973* |
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 |
|
Theorem | abrexex2 5974* |
Existence of an existentially restricted class abstraction. 𝜑 is
normally has free-variable parameters 𝑥 and 𝑦. See
also
abrexex 5967. (Contributed by NM, 12-Sep-2004.)
|
⊢ 𝐴 ∈ V & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V |
|
Theorem | abexssex 5975* |
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 |
|
Theorem | abexex 5976* |
A condition where a class builder continues to exist after its wff is
existentially quantified. (Contributed by NM, 4-Mar-2007.)
|
⊢ 𝐴 ∈ V & ⊢ (𝜑 → 𝑥 ∈ 𝐴)
& ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥𝜑} ∈ V |
|
Theorem | oprabexd 5977* |
Existence of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓)
& ⊢ (𝜑 → 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) |
|
Theorem | oprabex 5978* |
Existence of an operation class abstraction. (Contributed by NM,
19-Oct-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧𝜑)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V |
|
Theorem | oprabex3 5979* |
Existence of an operation class abstraction (special case).
(Contributed by NM, 19-Oct-2004.)
|
⊢ 𝐻 ∈ V & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} ⇒ ⊢ 𝐹 ∈ V |
|
Theorem | oprabrexex2 5980* |
Existence of an existentially restricted operation abstraction.
(Contributed by Jeff Madsen, 11-Jun-2010.)
|
⊢ 𝐴 ∈ V & ⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ∈ V ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V |
|
Theorem | ab2rexex 5981* |
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 5967. (Contributed by NM,
20-Sep-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V |
|
Theorem | ab2rexex2 5982* |
Existence of an existentially restricted class abstraction. 𝜑
normally has free-variable parameters 𝑥, 𝑦, and 𝑧.
Compare abrexex2 5974. (Contributed by NM, 20-Sep-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ {𝑧 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V |
|
Theorem | xpexgALT 5983 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. This
version is proven using Replacement; see
xpexg 4611 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) |
|
Theorem | offval3 5984* |
General value of (𝐹 ∘𝑓 𝑅𝐺) with no assumptions on
functionality
of 𝐹 and 𝐺. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
|
Theorem | offres 5985 |
Pointwise combination commutes with restriction. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘𝑓 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘𝑓 𝑅(𝐺 ↾ 𝐷))) |
|
Theorem | ofmres 5986* |
Equivalent expressions for a restriction of the function operation map.
Unlike ∘𝑓 𝑅 which is a proper class, ( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) can
be a set by ofmresex 5987, allowing it to be used as a function or
structure argument. By ofmresval 5945, the restricted operation map
values are the same as the original values, allowing theorems for
∘𝑓 𝑅 to be reused. (Contributed by NM,
20-Oct-2014.)
|
⊢ ( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) = (𝑓 ∈ 𝐴, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘𝑓 𝑅𝑔)) |
|
Theorem | ofmresex 5987 |
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
|
|
Syntax | c1st 5988 |
Extend the definition of a class to include the first member an ordered
pair function.
|
class 1st |
|
Syntax | c2nd 5989 |
Extend the definition of a class to include the second member an ordered
pair function.
|
class 2nd |
|
Definition | df-1st 5990 |
Define a function that extracts the first member, or abscissa, of an
ordered pair. Theorem op1st 5996 proves that it does this. For example,
(1st ‘〈 3 , 4 〉) = 3 . Equivalent to Definition 5.13 (i) of
[Monk1] p. 52 (compare op1sta 4976 and op1stb 4357). The notation is the same
as Monk's. (Contributed by NM, 9-Oct-2004.)
|
⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) |
|
Definition | df-2nd 5991 |
Define a function that extracts the second member, or ordinate, of an
ordered pair. Theorem op2nd 5997 proves that it does this. For example,
(2nd ‘〈 3 , 4 〉) = 4 . Equivalent to Definition 5.13 (ii)
of [Monk1] p. 52 (compare op2nda 4979 and op2ndb 4978). The notation is the
same as Monk's. (Contributed by NM, 9-Oct-2004.)
|
⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) |
|
Theorem | 1stvalg 5992 |
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 {𝐴}) |
|
Theorem | 2ndvalg 5993 |
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 {𝐴}) |
|
Theorem | 1st0 5994 |
The value of the first-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
⊢ (1st ‘∅) =
∅ |
|
Theorem | 2nd0 5995 |
The value of the second-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
⊢ (2nd ‘∅) =
∅ |
|
Theorem | op1st 5996 |
Extract the first member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (1st
‘〈𝐴, 𝐵〉) = 𝐴 |
|
Theorem | op2nd 5997 |
Extract the second member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (2nd
‘〈𝐴, 𝐵〉) = 𝐵 |
|
Theorem | op1std 5998 |
Extract the first member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (1st ‘𝐶) = 𝐴) |
|
Theorem | op2ndd 5999 |
Extract the second member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = 𝐵) |
|
Theorem | op1stg 6000 |
Extract the first member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) |