Theorem List for Intuitionistic Logic Explorer - 6101-6200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | suppssfv 6101* |
Formula building theorem for support restriction, on a function which
preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ 𝐴) “ (V ∖ {𝑌})) ⊆ 𝐿)
& ⊢ (𝜑 → (𝐹‘𝑌) = 𝑍)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) “ (V ∖ {𝑍})) ⊆ 𝐿) |
|
Theorem | suppssov1 6102* |
Formula building theorem for support restrictions: operator with left
annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ 𝐴) “ (V ∖ {𝑌})) ⊆ 𝐿)
& ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) ⇒ ⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) “ (V ∖ {𝑍})) ⊆ 𝐿) |
|
2.6.13 Function operation
|
|
Syntax | cof 6103 |
Extend class notation to include mapping of an operation to a function
operation.
|
class ∘𝑓 𝑅 |
|
Syntax | cofr 6104 |
Extend class notation to include mapping of a binary relation to a
function relation.
|
class ∘𝑟 𝑅 |
|
Definition | df-of 6105* |
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 6106* |
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 | ofeqd 6107 |
Equality theorem for function operation, deduction form. (Contributed
by SN, 11-Nov-2024.)
|
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ∘𝑓 𝑅 = ∘𝑓
𝑆) |
|
Theorem | ofeq 6108 |
Equality theorem for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ (𝑅 = 𝑆 → ∘𝑓 𝑅 = ∘𝑓
𝑆) |
|
Theorem | ofreq 6109 |
Equality theorem for function relation. (Contributed by Mario Carneiro,
28-Jul-2014.)
|
⊢ (𝑅 = 𝑆 → ∘𝑟 𝑅 = ∘𝑟
𝑆) |
|
Theorem | ofexg 6110 |
A function operation restricted to a set is a set. (Contributed by NM,
28-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → ( ∘𝑓 𝑅 ↾ 𝐴) ∈ V) |
|
Theorem | nfof 6111 |
Hypothesis builder for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘𝑓
𝑅 |
|
Theorem | nfofr 6112 |
Hypothesis builder for function relation. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘𝑟
𝑅 |
|
Theorem | offval 6113* |
Value of an operation applied to two functions. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷))) |
|
Theorem | ofrfval 6114* |
Value of a relation applied to two functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀𝑥 ∈ 𝑆 𝐶𝑅𝐷)) |
|
Theorem | ofvalg 6115 |
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 6116 |
Exhibit a function relation at a point. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∘𝑟 𝑅𝐺 ∧ 𝑋 ∈ 𝑆) → 𝐶𝑅𝐷) |
|
Theorem | ofmresval 6117 |
Value of a restriction of the function operation map. (Contributed by
NM, 20-Oct-2014.)
|
⊢ (𝜑 → 𝐹 ∈ 𝐴)
& ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵))𝐺) = (𝐹 ∘𝑓 𝑅𝐺)) |
|
Theorem | off 6118* |
The function operation produces a function. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺):𝐶⟶𝑈) |
|
Theorem | offeq 6119* |
Convert an identity of the operation to the analogous identity on
the function operation. (Contributed by Jim Kingdon,
26-Nov-2023.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶
& ⊢ (𝜑 → 𝐻:𝐶⟶𝑈)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐷)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐸)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐷𝑅𝐸) = (𝐻‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = 𝐻) |
|
Theorem | ofres 6120 |
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 6121* |
The function operation expressed as a mapping. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) |
|
Theorem | ofrfval2 6122* |
The function relation acting on maps. (Contributed by Mario Carneiro,
20-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶)) |
|
Theorem | suppssof1 6123* |
Formula building theorem for support restrictions: vector operation with
left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ (𝜑 → (◡𝐴 “ (V ∖ {𝑌})) ⊆ 𝐿)
& ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)
& ⊢ (𝜑 → 𝐴:𝐷⟶𝑉)
& ⊢ (𝜑 → 𝐵:𝐷⟶𝑅)
& ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (◡(𝐴 ∘𝑓 𝑂𝐵) “ (V ∖ {𝑍})) ⊆ 𝐿) |
|
Theorem | ofco 6124 |
The composition of a function operation with another function.
(Contributed by Mario Carneiro, 19-Dec-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐻:𝐷⟶𝐶)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐷 ∈ 𝑋)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → ((𝐹 ∘𝑓 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘𝑓 𝑅(𝐺 ∘ 𝐻))) |
|
Theorem | offveqb 6125* |
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 6126 |
Function operation on two constant functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 𝑅(𝐴 × {𝐶})) = (𝐴 × {(𝐵𝑅𝐶)})) |
|
Theorem | caofref 6127* |
Transfer a reflexive law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥𝑅𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∘𝑟 𝑅𝐹) |
|
Theorem | caofinvl 6128* |
Transfer a left inverse law to the function operation. (Contributed
by NM, 22-Oct-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝑁:𝑆⟶𝑆)
& ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 𝑅𝐹) = (𝐴 × {𝐵})) |
|
Theorem | caofcom 6129* |
Transfer a commutative law to the function operation. (Contributed by
Mario Carneiro, 26-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦) = (𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝐺 ∘𝑓 𝑅𝐹)) |
|
Theorem | caofrss 6130* |
Transfer a relation subset law to the function relation. (Contributed
by Mario Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦 → 𝑥𝑇𝑦)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 → 𝐹 ∘𝑟 𝑇𝐺)) |
|
Theorem | caoftrn 6131* |
Transfer a transitivity law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐻:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧)) ⇒ ⊢ (𝜑 → ((𝐹 ∘𝑟 𝑅𝐺 ∧ 𝐺 ∘𝑟 𝑇𝐻) → 𝐹 ∘𝑟 𝑈𝐻)) |
|
2.6.14 Functions (continued)
|
|
Theorem | resfunexgALT 6132 |
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 5757 but requires ax-pow 4192 and ax-un 4451. (Contributed by NM,
7-Apr-1995.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) |
|
Theorem | cofunexg 6133 |
Existence of a composition when the first member is a function.
(Contributed by NM, 8-Oct-2007.)
|
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V) |
|
Theorem | cofunex2g 6134 |
Existence of a composition when the second member is one-to-one.
(Contributed by NM, 8-Oct-2007.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V) |
|
Theorem | fnexALT 6135 |
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 5319. This version of fnex 5758
uses
ax-pow 4192 and ax-un 4451, whereas fnex 5758
does not. (Contributed by NM,
14-Aug-1994.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) |
|
Theorem | funexw 6136 |
Weak version of funex 5759 that holds without ax-coll 4133. If the domain and
codomain of a function exist, so does the function. (Contributed by Rohan
Ridenour, 13-Aug-2023.)
|
⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ 𝐶) → 𝐹 ∈ V) |
|
Theorem | mptexw 6137* |
Weak version of mptex 5762 that holds without ax-coll 4133. If the domain
and codomain of a function given by maps-to notation are sets, the
function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V & ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V |
|
Theorem | funrnex 6138 |
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 5759. (Contributed by NM, 11-Nov-1995.)
|
⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V)) |
|
Theorem | focdmex 6139 |
If the domain of an onto function exists, so does its codomain.
(Contributed by NM, 23-Jul-2004.)
|
⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V)) |
|
Theorem | f1dmex 6140 |
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 6141* |
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 5761, funex 5759, fnex 5758, resfunexg 5757, and
funimaexg 5319. See also abrexex2 6148. (Contributed by NM, 16-Oct-2003.)
(Proof shortened by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V |
|
Theorem | abrexexg 6142* |
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 6143* |
The existence of an indexed union. 𝑥 is normally a free-variable
parameter in 𝐵. (Contributed by NM, 23-Mar-2006.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
|
Theorem | abrexex2g 6144* |
Existence of an existentially restricted class abstraction.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} ∈ 𝑊) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V) |
|
Theorem | opabex3d 6145* |
Existence of an ordered pair abstraction, deduction version.
(Contributed by Alexander van der Vekens, 19-Oct-2017.)
|
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑦 ∣ 𝜓} ∈ V) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ∈ V) |
|
Theorem | opabex3 6146* |
Existence of an ordered pair abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∣ 𝜑} ∈ V) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V |
|
Theorem | iunex 6147* |
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 6148* |
Existence of an existentially restricted class abstraction. 𝜑 is
normally has free-variable parameters 𝑥 and 𝑦. See
also
abrexex 6141. (Contributed by NM, 12-Sep-2004.)
|
⊢ 𝐴 ∈ V & ⊢ {𝑦 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} ∈ V |
|
Theorem | abexssex 6149* |
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 6150* |
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 6151* |
Existence of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ∃*𝑧𝜓)
& ⊢ (𝜑 → 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) |
|
Theorem | oprabex 6152* |
Existence of an operation class abstraction. (Contributed by NM,
19-Oct-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃*𝑧𝜑)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⇒ ⊢ 𝐹 ∈ V |
|
Theorem | oprabex3 6153* |
Existence of an operation class abstraction (special case).
(Contributed by NM, 19-Oct-2004.)
|
⊢ 𝐻 ∈ V & ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} ⇒ ⊢ 𝐹 ∈ V |
|
Theorem | oprabrexex2 6154* |
Existence of an existentially restricted operation abstraction.
(Contributed by Jeff Madsen, 11-Jun-2010.)
|
⊢ 𝐴 ∈ V & ⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} ∈ V ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑤 ∈ 𝐴 𝜑} ∈ V |
|
Theorem | ab2rexex 6155* |
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 6141. (Contributed by NM,
20-Sep-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} ∈ V |
|
Theorem | ab2rexex2 6156* |
Existence of an existentially restricted class abstraction. 𝜑
normally has free-variable parameters 𝑥, 𝑦, and 𝑧.
Compare abrexex2 6148. (Contributed by NM, 20-Sep-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ {𝑧 ∣ 𝜑} ∈ V ⇒ ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} ∈ V |
|
Theorem | xpexgALT 6157 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. This
version is proven using Replacement; see
xpexg 4758 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 6158* |
General value of (𝐹 ∘𝑓 𝑅𝐺) with no assumptions on
functionality
of 𝐹 and 𝐺. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
|
Theorem | offres 6159 |
Pointwise combination commutes with restriction. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘𝑓 𝑅𝐺) ↾ 𝐷) = ((𝐹 ↾ 𝐷) ∘𝑓 𝑅(𝐺 ↾ 𝐷))) |
|
Theorem | ofmres 6160* |
Equivalent expressions for a restriction of the function operation map.
Unlike ∘𝑓 𝑅 which is a proper class, ( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) can
be a set by ofmresex 6161, allowing it to be used as a function or
structure argument. By ofmresval 6117, 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 6161 |
Existence of a restriction of the function operation map. (Contributed
by NM, 20-Oct-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵)) ∈ V) |
|
2.6.15 First and second members of an ordered
pair
|
|
Syntax | c1st 6162 |
Extend the definition of a class to include the first member an ordered
pair function.
|
class 1st |
|
Syntax | c2nd 6163 |
Extend the definition of a class to include the second member an ordered
pair function.
|
class 2nd |
|
Definition | df-1st 6164 |
Define a function that extracts the first member, or abscissa, of an
ordered pair. Theorem op1st 6170 proves that it does this. For example,
(1st ‘〈 3 , 4 〉) = 3 . Equivalent to Definition 5.13 (i) of
[Monk1] p. 52 (compare op1sta 5128 and op1stb 4496). The notation is the same
as Monk's. (Contributed by NM, 9-Oct-2004.)
|
⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) |
|
Definition | df-2nd 6165 |
Define a function that extracts the second member, or ordinate, of an
ordered pair. Theorem op2nd 6171 proves that it does this. For example,
(2nd ‘〈 3 , 4 〉) = 4 . Equivalent to Definition 5.13 (ii)
of [Monk1] p. 52 (compare op2nda 5131 and op2ndb 5130). The notation is the
same as Monk's. (Contributed by NM, 9-Oct-2004.)
|
⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) |
|
Theorem | 1stvalg 6166 |
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 6167 |
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 6168 |
The value of the first-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
⊢ (1st ‘∅) =
∅ |
|
Theorem | 2nd0 6169 |
The value of the second-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
⊢ (2nd ‘∅) =
∅ |
|
Theorem | op1st 6170 |
Extract the first member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (1st
‘〈𝐴, 𝐵〉) = 𝐴 |
|
Theorem | op2nd 6171 |
Extract the second member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (2nd
‘〈𝐴, 𝐵〉) = 𝐵 |
|
Theorem | op1std 6172 |
Extract the first member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (1st ‘𝐶) = 𝐴) |
|
Theorem | op2ndd 6173 |
Extract the second member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐶 = 〈𝐴, 𝐵〉 → (2nd ‘𝐶) = 𝐵) |
|
Theorem | op1stg 6174 |
Extract the first member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) |
|
Theorem | op2ndg 6175 |
Extract the second member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
|
Theorem | ot1stg 6176 |
Extract the first member of an ordered triple. (Due to infrequent
usage, it isn't worthwhile at this point to define special extractors
for triples, so we reuse the ordered pair extractors for ot1stg 6176,
ot2ndg 6177, ot3rdgg 6178.) (Contributed by NM, 3-Apr-2015.) (Revised
by
Mario Carneiro, 2-May-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (1st
‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐴) |
|
Theorem | ot2ndg 6177 |
Extract the second member of an ordered triple. (See ot1stg 6176 comment.)
(Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro,
2-May-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd
‘(1st ‘〈𝐴, 𝐵, 𝐶〉)) = 𝐵) |
|
Theorem | ot3rdgg 6178 |
Extract the third member of an ordered triple. (See ot1stg 6176 comment.)
(Contributed by NM, 3-Apr-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (2nd ‘〈𝐴, 𝐵, 𝐶〉) = 𝐶) |
|
Theorem | 1stval2 6179 |
Alternate value of the function that extracts the first member of an
ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by
NM, 18-Aug-2006.)
|
⊢ (𝐴 ∈ (V × V) →
(1st ‘𝐴)
= ∩ ∩ 𝐴) |
|
Theorem | 2ndval2 6180 |
Alternate value of the function that extracts the second member of an
ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by
NM, 18-Aug-2006.)
|
⊢ (𝐴 ∈ (V × V) →
(2nd ‘𝐴)
= ∩ ∩ ∩ ◡{𝐴}) |
|
Theorem | fo1st 6181 |
The 1st function maps the universe onto the
universe. (Contributed
by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
⊢ 1st :V–onto→V |
|
Theorem | fo2nd 6182 |
The 2nd function maps the universe onto the
universe. (Contributed
by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
⊢ 2nd :V–onto→V |
|
Theorem | f1stres 6183 |
Mapping of a restriction of the 1st (first
member of an ordered
pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario
Carneiro, 8-Sep-2013.)
|
⊢ (1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 |
|
Theorem | f2ndres 6184 |
Mapping of a restriction of the 2nd (second
member of an ordered
pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario
Carneiro, 8-Sep-2013.)
|
⊢ (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐵 |
|
Theorem | fo1stresm 6185* |
Onto mapping of a restriction of the 1st
(first member of an ordered
pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|
⊢ (∃𝑦 𝑦 ∈ 𝐵 → (1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐴) |
|
Theorem | fo2ndresm 6186* |
Onto mapping of a restriction of the 2nd
(second member of an
ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐵) |
|
Theorem | 1stcof 6187 |
Composition of the first member function with another function.
(Contributed by NM, 12-Oct-2007.)
|
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (1st ∘ 𝐹):𝐴⟶𝐵) |
|
Theorem | 2ndcof 6188 |
Composition of the second member function with another function.
(Contributed by FL, 15-Oct-2012.)
|
⊢ (𝐹:𝐴⟶(𝐵 × 𝐶) → (2nd ∘ 𝐹):𝐴⟶𝐶) |
|
Theorem | xp1st 6189 |
Location of the first element of a Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵) |
|
Theorem | xp2nd 6190 |
Location of the second element of a Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶) |
|
Theorem | 1stexg 6191 |
Existence of the first member of a set. (Contributed by Jim Kingdon,
26-Jan-2019.)
|
⊢ (𝐴 ∈ 𝑉 → (1st ‘𝐴) ∈ V) |
|
Theorem | 2ndexg 6192 |
Existence of the first member of a set. (Contributed by Jim Kingdon,
26-Jan-2019.)
|
⊢ (𝐴 ∈ 𝑉 → (2nd ‘𝐴) ∈ V) |
|
Theorem | elxp6 6193 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 5134. (Contributed by NM, 9-Oct-2004.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st
‘𝐴) ∈ 𝐵 ∧ (2nd
‘𝐴) ∈ 𝐶))) |
|
Theorem | elxp7 6194 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 5134. (Contributed by NM, 19-Aug-2006.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧
((1st ‘𝐴)
∈ 𝐵 ∧
(2nd ‘𝐴)
∈ 𝐶))) |
|
Theorem | oprssdmm 6195* |
Domain of closure of an operation. (Contributed by Jim Kingdon,
23-Oct-2023.)
|
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ∃𝑣 𝑣 ∈ 𝑢)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)
& ⊢ (𝜑 → Rel 𝐹) ⇒ ⊢ (𝜑 → (𝑆 × 𝑆) ⊆ dom 𝐹) |
|
Theorem | eqopi 6196 |
Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.)
(Revised by Mario Carneiro, 23-Feb-2014.)
|
⊢ ((𝐴 ∈ (𝑉 × 𝑊) ∧ ((1st ‘𝐴) = 𝐵 ∧ (2nd ‘𝐴) = 𝐶)) → 𝐴 = 〈𝐵, 𝐶〉) |
|
Theorem | xp2 6197* |
Representation of cross product based on ordered pair component
functions. (Contributed by NM, 16-Sep-2006.)
|
⊢ (𝐴 × 𝐵) = {𝑥 ∈ (V × V) ∣
((1st ‘𝑥)
∈ 𝐴 ∧
(2nd ‘𝑥)
∈ 𝐵)} |
|
Theorem | unielxp 6198 |
The membership relation for a cross product is inherited by union.
(Contributed by NM, 16-Sep-2006.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) → ∪ 𝐴 ∈ ∪ (𝐵
× 𝐶)) |
|
Theorem | 1st2nd2 6199 |
Reconstruction of a member of a cross product in terms of its ordered pair
components. (Contributed by NM, 20-Oct-2013.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
|
Theorem | xpopth 6200 |
An ordered pair theorem for members of cross products. (Contributed by
NM, 20-Jun-2007.)
|
⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (((1st ‘𝐴) = (1st
‘𝐵) ∧
(2nd ‘𝐴)
= (2nd ‘𝐵)) ↔ 𝐴 = 𝐵)) |