Home | Metamath
Proof Explorer Theorem List (p. 79 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | curry1 7801* | Composition with ◡(2nd ↾ ({𝐶} × V)) turns any binary operation 𝐹 with a constant first operand into a function 𝐺 of the second operand only. This transformation is called "currying." (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥))) | ||
Theorem | curry1val 7802 | The value of a curried function with a constant first argument. (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → (𝐺‘𝐷) = (𝐶𝐹𝐷)) | ||
Theorem | curry1f 7803 | Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008.) |
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) ⇒ ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐷 ∧ 𝐶 ∈ 𝐴) → 𝐺:𝐵⟶𝐷) | ||
Theorem | curry2 7804* | Composition with ◡(1st ↾ (V × {𝐶})) turns any binary operation 𝐹 with a constant second operand into a function 𝐺 of the first operand only. This transformation is called "currying." (If this becomes frequently used, we can introduce a new notation for the hypothesis.) (Contributed by NM, 16-Dec-2008.) |
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶}))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶))) | ||
Theorem | curry2f 7805 | Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.) |
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶}))) ⇒ ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐷 ∧ 𝐶 ∈ 𝐵) → 𝐺:𝐴⟶𝐷) | ||
Theorem | curry2val 7806 | The value of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.) |
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶}))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝐺‘𝐷) = (𝐷𝐹𝐶)) | ||
Theorem | cnvf1olem 7807 | Lemma for cnvf1o 7808. (Contributed by Mario Carneiro, 27-Apr-2014.) |
⊢ ((Rel 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → (𝐶 ∈ ◡𝐴 ∧ 𝐵 = ∪ ◡{𝐶})) | ||
Theorem | cnvf1o 7808* | Describe a function that maps the elements of a set to its converse bijectively. (Contributed by Mario Carneiro, 27-Apr-2014.) |
⊢ (Rel 𝐴 → (𝑥 ∈ 𝐴 ↦ ∪ ◡{𝑥}):𝐴–1-1-onto→◡𝐴) | ||
Theorem | fparlem1 7809 | Lemma for fpar 7813. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (◡(1st ↾ (V × V)) “ {𝑥}) = ({𝑥} × V) | ||
Theorem | fparlem2 7810 | Lemma for fpar 7813. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (◡(2nd ↾ (V × V)) “ {𝑦}) = (V × {𝑦}) | ||
Theorem | fparlem3 7811* | Lemma for fpar 7813. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐹 Fn 𝐴 → (◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) = ∪ 𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V))) | ||
Theorem | fparlem4 7812* | Lemma for fpar 7813. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))) = ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) | ||
Theorem | fpar 7813* | Merge two functions in parallel. Use as the second argument of a composition with a binary operation to build compound functions such as (𝑥 ∈ (0[,)+∞), 𝑦 ∈ ℝ ↦ ((√‘𝑥) + (sin‘𝑦))), see also ex-fpar 28243. (Contributed by NM, 17-Sep-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V))))) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉)) | ||
Theorem | fsplit 7814 | A function that can be used to feed a common value to both operands of an operation. Use as the second argument of a composition with the function of fpar 7813 in order to build compound functions such as (𝑥 ∈ (0[,)+∞) ↦ ((√‘𝑥) + (sin‘𝑥))). (Contributed by NM, 17-Sep-2007.) Replace use of dfid2 5465 with df-id 5462. (Revised by BJ, 31-Dec-2023.) |
⊢ ◡(1st ↾ I ) = (𝑥 ∈ V ↦ 〈𝑥, 𝑥〉) | ||
Theorem | fsplitOLD 7815 | Obsolete proof of fsplit 7814 as of 31-Dec-2023 . (Contributed by NM, 17-Sep-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ◡(1st ↾ I ) = (𝑥 ∈ V ↦ 〈𝑥, 𝑥〉) | ||
Theorem | fsplitfpar 7816* | Merge two functions with a common argument in parallel. Combination of fsplit 7814 and fpar 7813. (Contributed by AV, 3-Jan-2024.) |
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V))))) & ⊢ 𝑆 = (◡(1st ↾ I ) ↾ 𝐴) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐻 ∘ 𝑆) = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) | ||
Theorem | offsplitfpar 7817 | Express the function operation map ∘f by the functions defined in fsplit 7814 and fpar 7813. (Contributed by AV, 4-Jan-2024.) |
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V))))) & ⊢ 𝑆 = (◡(1st ↾ I ) ↾ 𝐴) ⇒ ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → ( + ∘ (𝐻 ∘ 𝑆)) = (𝐹 ∘f + 𝐺)) | ||
Theorem | f2ndf 7818 | The 2nd (second component of an ordered pair) function restricted to a function 𝐹 is a function from 𝐹 into the codomain of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹⟶𝐵) | ||
Theorem | fo2ndf 7819 | The 2nd (second component of an ordered pair) function restricted to a function 𝐹 is a function from 𝐹 onto the range of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹–onto→ran 𝐹) | ||
Theorem | f1o2ndf1 7820 | The 2nd (second component of an ordered pair) function restricted to a one-to-one function 𝐹 is a one-to-one function from 𝐹 onto the range of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
⊢ (𝐹:𝐴–1-1→𝐵 → (2nd ↾ 𝐹):𝐹–1-1-onto→ran 𝐹) | ||
Theorem | algrflem 7821 | Lemma for algrf 15919 and related theorems. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐵(𝐹 ∘ 1st )𝐶) = (𝐹‘𝐵) | ||
Theorem | frxp 7822* | A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) (Proof shortened by Wolf Lammen, 4-Oct-2014.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵)) | ||
Theorem | xporderlem 7823* | Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ (〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))) | ||
Theorem | poxp 7824* | A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵)) | ||
Theorem | soxp 7825* | A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵)) | ||
Theorem | wexp 7826* | A lexicographical ordering of two well-ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑆 We 𝐵) → 𝑇 We (𝐴 × 𝐵)) | ||
Theorem | fnwelem 7827* | Lemma for fnwe 7828. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐵) & ⊢ (𝜑 → 𝑆 We 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V) & ⊢ 𝑄 = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd ‘𝑢)𝑆(2nd ‘𝑣))))} & ⊢ 𝐺 = (𝑧 ∈ 𝐴 ↦ 〈(𝐹‘𝑧), 𝑧〉) ⇒ ⊢ (𝜑 → 𝑇 We 𝐴) | ||
Theorem | fnwe 7828* | A variant on lexicographic order, which sorts first by some function of the base set, and then by a "backup" well-ordering when the function value is equal on both elements. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐵) & ⊢ (𝜑 → 𝑆 We 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V) ⇒ ⊢ (𝜑 → 𝑇 We 𝐴) | ||
Theorem | fnse 7829* | Condition for the well-order in fnwe 7828 to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 Se 𝐵) & ⊢ (𝜑 → (◡𝐹 “ 𝑤) ∈ V) ⇒ ⊢ (𝜑 → 𝑇 Se 𝐴) | ||
Theorem | fvproj 7830* | Value of a function on ordered pairs with values expressed as ordered pairs. Note that 𝐹 and 𝐺 are the projections of 𝐻 to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019.) |
⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻‘〈𝑋, 𝑌〉) = 〈(𝐹‘𝑋), (𝐺‘𝑌)〉) | ||
Theorem | fimaproj 7831* | Image of a cartesian product for a function on ordered pairs with values expressed as ordered pairs. Note that 𝐹 and 𝐺 are the projections of 𝐻 to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019.) |
⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝑌 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 “ (𝑋 × 𝑌)) = ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) | ||
In this section, the support of functions is defined and corresponding theorems are provided. Since basic properties (see suppval 7834) are based on the Axiom of Union (usage of dmexg 7615), these definition and theorems cannot be provided earlier. Until April 2019, the support of a function was represented by the expression (◡𝑅 “ (V ∖ {𝑍})) (see suppimacnv 7843). The theorems which are based on this representation and which are provided in previous sections could be moved into this section to have all related theorems in one section, although they do not depend on the Axiom of Union. This was possible because they are not used before. The current theorems differ from the original ones by requiring that the classes representing the "function" (or its "domain") and the "zero element" are sets. Actually, this does not cause any problem (until now). | ||
Syntax | csupp 7832 | Extend class definition to include the support of functions. |
class supp | ||
Definition | df-supp 7833* | Define the support of a function against a "zero" value. According to Wikipedia ("Support (mathematics)", 31-Mar-2019, https://en.wikipedia.org/wiki/Support_(mathematics)) "In mathematics, the support of a real-valued function f is the subset of the domain containing those elements which are not mapped to zero." and "The notion of support also extends in a natural way to functions taking values in more general sets than R [the real numbers] and to other objects.". The following definition allows for such extensions, being applicable for any sets (which usually are functions) and any element (even not necessarily from the range of the function) regarded as "zero". (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.) |
⊢ supp = (𝑥 ∈ V, 𝑧 ∈ V ↦ {𝑖 ∈ dom 𝑥 ∣ (𝑥 “ {𝑖}) ≠ {𝑧}}) | ||
Theorem | suppval 7834* | The value of the operation constructing the support of a function. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 supp 𝑍) = {𝑖 ∈ dom 𝑋 ∣ (𝑋 “ {𝑖}) ≠ {𝑍}}) | ||
Theorem | supp0prc 7835 | The support of a class is empty if either the class or the "zero" is a proper class. (Contributed by AV, 28-May-2019.) |
⊢ (¬ (𝑋 ∈ V ∧ 𝑍 ∈ V) → (𝑋 supp 𝑍) = ∅) | ||
Theorem | suppvalbr 7836* | The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑦 𝑥𝑅𝑦 ∧ ∃𝑦(𝑥𝑅𝑦 ↔ 𝑦 ≠ 𝑍))}) | ||
Theorem | supp0 7837 | The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019.) |
⊢ (𝑍 ∈ 𝑊 → (∅ supp 𝑍) = ∅) | ||
Theorem | suppval1 7838* | The value of the operation constructing the support of a function. (Contributed by AV, 6-Apr-2019.) |
⊢ ((Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 supp 𝑍) = {𝑖 ∈ dom 𝑋 ∣ (𝑋‘𝑖) ≠ 𝑍}) | ||
Theorem | suppvalfn 7839* | The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by AV, 22-Apr-2019.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = {𝑖 ∈ 𝑋 ∣ (𝐹‘𝑖) ≠ 𝑍}) | ||
Theorem | elsuppfn 7840 | An element of the support of a function with a given domain. (Contributed by AV, 27-May-2019.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑆 ∈ (𝐹 supp 𝑍) ↔ (𝑆 ∈ 𝑋 ∧ (𝐹‘𝑆) ≠ 𝑍))) | ||
Theorem | cnvimadfsn 7841* | The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019.) |
⊢ (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)} | ||
Theorem | suppimacnvss 7842 | The support of functions "defined" by inverse images is a subset of the support defined by df-supp 7833. (Contributed by AV, 7-Apr-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍)) | ||
Theorem | suppimacnv 7843 | Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 7-Apr-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = (◡𝑅 “ (V ∖ {𝑍}))) | ||
Theorem | frnsuppeq 7844 | Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 supp 𝑍) = (◡𝐹 “ (𝑆 ∖ {𝑍})))) | ||
Theorem | suppssdm 7845 | The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019.) |
⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹 | ||
Theorem | suppsnop 7846 | The support of a singleton of an ordered pair. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐹 = {〈𝑋, 𝑌〉} ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = if(𝑌 = 𝑍, ∅, {𝑋})) | ||
Theorem | snopsuppss 7847 | The support of a singleton containing an ordered pair is a subset of the singleton containing the first element of the ordered pair, i.e. it is empty or the singleton itself. (Contributed by AV, 19-Jul-2019.) |
⊢ ({〈𝑋, 𝑌〉} supp 𝑍) ⊆ {𝑋} | ||
Theorem | fvn0elsupp 7848 | If the function value for a given argument is not empty, the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 2-Jul-2019.) (Revised by AV, 4-Apr-2020.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ (𝐺 Fn 𝐵 ∧ (𝐺‘𝑋) ≠ ∅)) → 𝑋 ∈ (𝐺 supp ∅)) | ||
Theorem | fvn0elsuppb 7849 | The function value for a given argument is not empty iff the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 4-Apr-2020.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵) → ((𝐺‘𝑋) ≠ ∅ ↔ 𝑋 ∈ (𝐺 supp ∅))) | ||
Theorem | rexsupp 7850* | Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by AV, 27-May-2019.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∃𝑥 ∈ (𝐹 supp 𝑍)𝜑 ↔ ∃𝑥 ∈ 𝑋 ((𝐹‘𝑥) ≠ 𝑍 ∧ 𝜑))) | ||
Theorem | ressuppss 7851 | The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝐹 ↾ 𝐵) supp 𝑍) ⊆ (𝐹 supp 𝑍)) | ||
Theorem | suppun 7852 | The support of a class/function is a subset of the support of the union of this class/function with another class/function. (Contributed by AV, 4-Jun-2019.) |
⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍)) | ||
Theorem | ressuppssdif 7853 | The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) ⊆ (((𝐹 ↾ 𝐵) supp 𝑍) ∪ (dom 𝐹 ∖ 𝐵))) | ||
Theorem | mptsuppdifd 7854* | The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (V ∖ {𝑍})}) | ||
Theorem | mptsuppd 7855* | The support of a function in maps-to notation. (Contributed by AV, 10-Apr-2019.) (Revised by AV, 28-May-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝑍}) | ||
Theorem | extmptsuppeq 7856* | The support of an extended function is the same as the original. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 30-Jun-2019.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐵 ∖ 𝐴)) → 𝑋 = 𝑍) ⇒ ⊢ (𝜑 → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍)) | ||
Theorem | suppfnss 7857* | The support of a function which has the same zero values (in its domain) as another function is a subset of the support of this other function. (Contributed by AV, 30-Apr-2019.) (Proof shortened by AV, 6-Jun-2022.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))) | ||
Theorem | funsssuppss 7858 | The support of a function which is a subset of another function is a subset of the support of this other function. (Contributed by AV, 27-Jul-2019.) |
⊢ ((Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)) | ||
Theorem | fnsuppres 7859 | Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015.) (Revised by AV, 28-May-2019.) |
⊢ ((𝐹 Fn (𝐴 ∪ 𝐵) ∧ (𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 supp 𝑍) ⊆ 𝐴 ↔ (𝐹 ↾ 𝐵) = (𝐵 × {𝑍}))) | ||
Theorem | fnsuppeq0 7860 | The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉) → ((𝐹 supp 𝑍) = ∅ ↔ 𝐹 = (𝐴 × {𝑍}))) | ||
Theorem | fczsupp0 7861 | The support of a constant function with value zero is empty. (Contributed by AV, 30-Jun-2019.) |
⊢ ((𝐵 × {𝑍}) supp 𝑍) = ∅ | ||
Theorem | suppss 7862* | Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑘) = 𝑍) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) | ||
Theorem | suppssr 7863 | A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍) | ||
Theorem | suppssov1 7864* | Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) & ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) & ⊢ (𝜑 → 𝑌 ∈ 𝑊) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) | ||
Theorem | suppssof1 7865* | Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → (𝐴 supp 𝑌) ⊆ 𝐿) & ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) & ⊢ (𝜑 → 𝐴:𝐷⟶𝑉) & ⊢ (𝜑 → 𝐵:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 ∘f 𝑂𝐵) supp 𝑍) ⊆ 𝐿) | ||
Theorem | suppss2 7866* | Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 22-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊) | ||
Theorem | suppsssn 7867* | Show that the support of a function is a subset of a singleton. (Contributed by AV, 21-Jul-2019.) |
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ 𝑘 ≠ 𝑊) → 𝐵 = 𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ {𝑊}) | ||
Theorem | suppssfv 7868* | Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) & ⊢ (𝜑 → (𝐹‘𝑌) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿) | ||
Theorem | suppofssd 7869 | Condition for the support of a function operation to be a subset of the union of the supports of the left and right function terms. (Contributed by Steven Nguyen, 28-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → (𝑍𝑋𝑍) = 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑋𝐺) supp 𝑍) ⊆ ((𝐹 supp 𝑍) ∪ (𝐺 supp 𝑍))) | ||
Theorem | suppofss1d 7870* | Condition for the support of a function operation to be a subset of the support of the left function term. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑍𝑋𝑥) = 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑋𝐺) supp 𝑍) ⊆ (𝐹 supp 𝑍)) | ||
Theorem | suppofss2d 7871* | Condition for the support of a function operation to be a subset of the support of the right function term. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥𝑋𝑍) = 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑋𝐺) supp 𝑍) ⊆ (𝐺 supp 𝑍)) | ||
Theorem | suppco 7872 | The support of the composition of two functions is the inverse image by the inner function of the support of the outer function. (Contributed by AV, 30-May-2019.) Extract this statement from the proof of supp0cosupp0 7874. (Revised by SN, 15-Sep-2023.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍))) | ||
Theorem | suppcofnd 7873* | The support of the composition of two functions. (Contributed by SN, 15-Sep-2023.) |
⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ((𝐹 ∘ 𝐺) supp 𝑍) = {𝑥 ∈ 𝐵 ∣ ((𝐺‘𝑥) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑥)) ≠ 𝑍)}) | ||
Theorem | supp0cosupp0 7874 | The support of the composition of two functions is empty if the support of the outer function is empty. (Contributed by AV, 30-May-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 supp 𝑍) = ∅ → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅)) | ||
Theorem | supp0cosupp0OLD 7875 | Obsolete version of supp0cosupp0 7874 as of 15-Sep-2023. The support of the composition of two functions is empty if the support of the outer function is empty. (Contributed by AV, 30-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 supp 𝑍) = ∅ → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅)) | ||
Theorem | imacosupp 7876 | The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍))) | ||
Theorem | imacosuppOLD 7877 | Obsolete version of imacosupp 7876 as of 15-Sep-2023. The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍))) | ||
The following theorems are about maps-to operations (see df-mpo 7163) where the domain of the second argument depends on the domain of the first argument, especially when the first argument is a pair and the base set of the second argument is the first component of the first argument, in short "x-maps-to operations". For labels, the abbreviations "mpox" are used (since "x" usually denotes the first argument). This is in line with the currently used conventions for such cases (see cbvmpox 7249, ovmpox 7305 and fmpox 7767). If the first argument is an ordered pair, as in the following, the abbreviation is extended to "mpoxop", and the maps-to operations are called "x-op maps-to operations" for short. | ||
Theorem | opeliunxp2f 7878* | Membership in a union of Cartesian products, using bound-variable hypothesis for 𝐸 instead of distinct variable conditions as in opeliunxp2 5711. (Contributed by AV, 25-Oct-2020.) |
⊢ Ⅎ𝑥𝐸 & ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) ⇒ ⊢ (〈𝐶, 𝐷〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) | ||
Theorem | mpoxeldm 7879* | If there is an element of the value of an operation given by a maps-to rule, then the first argument is an element of the first component of the domain and the second argument is an element of the second component of the domain depending on the first argument. (Contributed by AV, 25-Oct-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐷)) | ||
Theorem | mpoxneldm 7880* | If the first argument of an operation given by a maps-to rule is not an element of the first component of the domain or the second argument is not an element of the second component of the domain depending on the first argument, then the value of the operation is the empty set. (Contributed by AV, 25-Oct-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝑋 ∉ 𝐶 ∨ 𝑌 ∉ ⦋𝑋 / 𝑥⦌𝐷) → (𝑋𝐹𝑌) = ∅) | ||
Theorem | mpoxopn0yelv 7881* | If there is an element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, then the second argument is an element of the first component of the first argument. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑁 ∈ (〈𝑉, 𝑊〉𝐹𝐾) → 𝐾 ∈ 𝑉)) | ||
Theorem | mpoxopynvov0g 7882* | If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) ∧ 𝐾 ∉ 𝑉) → (〈𝑉, 𝑊〉𝐹𝐾) = ∅) | ||
Theorem | mpoxopxnop0 7883* | If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is not an ordered pair, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (¬ 𝑉 ∈ (V × V) → (𝑉𝐹𝐾) = ∅) | ||
Theorem | mpoxopx0ov0 7884* | If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is the empty set, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (∅𝐹𝐾) = ∅ | ||
Theorem | mpoxopxprcov0 7885* | If the components of the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, are not sets, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (¬ (𝑉 ∈ V ∧ 𝑊 ∈ V) → (〈𝑉, 𝑊〉𝐹𝐾) = ∅) | ||
Theorem | mpoxopynvov0 7886* | If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (𝐾 ∉ 𝑉 → (〈𝑉, 𝑊〉𝐹𝐾) = ∅) | ||
Theorem | mpoxopoveq 7887* | Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑}) ⇒ ⊢ (((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) ∧ 𝐾 ∈ 𝑉) → (〈𝑉, 𝑊〉𝐹𝐾) = {𝑛 ∈ 𝑉 ∣ [〈𝑉, 𝑊〉 / 𝑥][𝐾 / 𝑦]𝜑}) | ||
Theorem | mpoxopovel 7888* | Element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens and Mario Carneiro, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑}) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑁 ∈ (〈𝑉, 𝑊〉𝐹𝐾) ↔ (𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ [〈𝑉, 𝑊〉 / 𝑥][𝐾 / 𝑦][𝑁 / 𝑛]𝜑))) | ||
Theorem | mpoxopoveqd 7889* | Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑}) & ⊢ (𝜓 → (𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌)) & ⊢ ((𝜓 ∧ ¬ 𝐾 ∈ 𝑉) → {𝑛 ∈ 𝑉 ∣ [〈𝑉, 𝑊〉 / 𝑥][𝐾 / 𝑦]𝜑} = ∅) ⇒ ⊢ (𝜓 → (〈𝑉, 𝑊〉𝐹𝐾) = {𝑛 ∈ 𝑉 ∣ [〈𝑉, 𝑊〉 / 𝑥][𝐾 / 𝑦]𝜑}) | ||
Theorem | brovex 7890* | A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) & ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → Rel (𝑉𝑂𝐸)) ⇒ ⊢ (𝐹(𝑉𝑂𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | ||
Theorem | brovmpoex 7891* | A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {〈𝑧, 𝑤〉 ∣ 𝜑}) ⇒ ⊢ (𝐹(𝑉𝑂𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | ||
Theorem | sprmpod 7892* | The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 20-Jun-2019.) |
⊢ 𝑀 = (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥(𝑣𝑅𝑒)𝑦 ∧ 𝜒)}) & ⊢ ((𝜑 ∧ 𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) & ⊢ (𝜑 → ∀𝑥∀𝑦(𝑥(𝑉𝑅𝐸)𝑦 → 𝜃)) & ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜃} ∈ V) ⇒ ⊢ (𝜑 → (𝑉𝑀𝐸) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝑉𝑅𝐸)𝑦 ∧ 𝜓)}) | ||
Syntax | ctpos 7893 | The transposition of a function. |
class tpos 𝐹 | ||
Definition | df-tpos 7894* | Define the transposition of a function, which is a function 𝐺 = tpos 𝐹 satisfying 𝐺(𝑥, 𝑦) = 𝐹(𝑦, 𝑥). (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) | ||
Theorem | tposss 7895 | Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺) | ||
Theorem | tposeq 7896 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺) | ||
Theorem | tposeqd 7897 | Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → tpos 𝐹 = tpos 𝐺) | ||
Theorem | tposssxp 7898 | The transposition is a subset of a Cartesian product. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ tpos 𝐹 ⊆ ((◡dom 𝐹 ∪ {∅}) × ran 𝐹) | ||
Theorem | reltpos 7899 | The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ Rel tpos 𝐹 | ||
Theorem | brtpos2 7900 | Value of the transposition at a pair 〈𝐴, 𝐵〉. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴tpos 𝐹𝐵 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |