Home | Metamath
Proof Explorer Theorem List (p. 452 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-afv 45101* | Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹‘𝐴) = ∅ (see df-fv 6499 and ndmfv 6872), (𝐹'''𝐴) = V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.) (Revised by BJ/AV, 25-Aug-2022.) |
⊢ (𝐹'''𝐴) = (℩'𝑥𝐴𝐹𝑥) | ||
Definition | df-aov 45102 | Define the value of an operation. In contrast to df-ov 7352, the alternative definition for a function value (see df-afv 45101) is used. By this, the value of the operation applied to two arguments is the universal class if the operation is not defined for these two arguments. There are still no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩) | ||
Theorem | ralbinrald 45103* | Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 = 𝑋) & ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ 𝜃)) | ||
Theorem | nvelim 45104 | If a class is the universal class it doesn't belong to any class, generalization of nvel 5271. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐴 = V → ¬ 𝐴 ∈ 𝐵) | ||
Theorem | alneu 45105 | If a statement holds for all sets, there is not a unique set for which the statement holds. (Contributed by Alexander van der Vekens, 28-Nov-2017.) |
⊢ (∀𝑥𝜑 → ¬ ∃!𝑥𝜑) | ||
Theorem | eu2ndop1stv 45106* | If there is a unique second component in an ordered pair contained in a given set, the first component must be a set. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ (∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | dfateq12d 45107 | Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 defAt 𝐴 ↔ 𝐺 defAt 𝐵)) | ||
Theorem | nfdfat 45108 | Bound-variable hypothesis builder for "defined at". To prove a deduction version of this theorem is not easily possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of "defined at" is based on are not available (e.g., for Fun/Rel, dom, ⊆, etc.). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐹 defAt 𝐴 | ||
Theorem | dfdfat2 45109* | Alternate definition of the predicate "defined at" not using the Fun predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ ∃!𝑦 𝐴𝐹𝑦)) | ||
Theorem | fundmdfat 45110 | A function is defined at any element of its domain. (Contributed by AV, 2-Sep-2022.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 𝐹 defAt 𝐴) | ||
Theorem | dfatprc 45111 | A function is not defined at a proper class. (Contributed by AV, 1-Sep-2022.) |
⊢ (¬ 𝐴 ∈ V → ¬ 𝐹 defAt 𝐴) | ||
Theorem | dfatelrn 45112 | The value of a function 𝐹 at a set 𝐴 is in the range of the function 𝐹 if 𝐹 is defined at 𝐴. (Contributed by AV, 1-Sep-2022.) |
⊢ (𝐹 defAt 𝐴 → (𝐹‘𝐴) ∈ ran 𝐹) | ||
Theorem | dfafv2 45113 | Alternative definition of (𝐹'''𝐴) using (𝐹‘𝐴) directly. (Contributed by Alexander van der Vekens, 22-Jul-2017.) (Revised by AV, 25-Aug-2022.) |
⊢ (𝐹'''𝐴) = if(𝐹 defAt 𝐴, (𝐹‘𝐴), V) | ||
Theorem | afveq12d 45114 | Equality deduction for function value, analogous to fveq12d 6844. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹'''𝐴) = (𝐺'''𝐵)) | ||
Theorem | afveq1 45115 | Equality theorem for function value, analogous to fveq1 6836. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐹 = 𝐺 → (𝐹'''𝐴) = (𝐺'''𝐴)) | ||
Theorem | afveq2 45116 | Equality theorem for function value, analogous to fveq1 6836. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐴 = 𝐵 → (𝐹'''𝐴) = (𝐹'''𝐵)) | ||
Theorem | nfafv 45117 | Bound-variable hypothesis builder for function value, analogous to nffv 6847. To prove a deduction version of this analogous to nffvd 6849 is not easily possible because a deduction version of nfdfat 45108 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹'''𝐴) | ||
Theorem | csbafv12g 45118 | Move class substitution in and out of a function value, analogous to csbfv12 6885, with a direct proof proposed by Mario Carneiro, analogous to csbov123 7391. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐹'''𝐵) = (⦋𝐴 / 𝑥⦌𝐹'''⦋𝐴 / 𝑥⦌𝐵)) | ||
Theorem | afvfundmfveq 45119 | If a class is a function restricted to a member of its domain, then the function value for this member is equal for both definitions. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 defAt 𝐴 → (𝐹'''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afvnfundmuv 45120 | If a set is not in the domain of a class or the class is not a function restricted to the set, then the function value for this set is the universe. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (¬ 𝐹 defAt 𝐴 → (𝐹'''𝐴) = V) | ||
Theorem | ndmafv 45121 | The value of a class outside its domain is the universe, compare with ndmfv 6872. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹'''𝐴) = V) | ||
Theorem | afvvdm 45122 | If the function value of a class for an argument is a set, the argument is contained in the domain of the class. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ∈ 𝐵 → 𝐴 ∈ dom 𝐹) | ||
Theorem | nfunsnafv 45123 | If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 6879. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹'''𝐴) = V) | ||
Theorem | afvvfunressn 45124 | If the function value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ∈ 𝐵 → Fun (𝐹 ↾ {𝐴})) | ||
Theorem | afvprc 45125 | A function's value at a proper class is the universe, compare with fvprc 6829. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ 𝐴 ∈ V → (𝐹'''𝐴) = V) | ||
Theorem | afvvv 45126 | If a function's value at an argument is a set, the argument is also a set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ∈ 𝐵 → 𝐴 ∈ V) | ||
Theorem | afvpcfv0 45127 | If the value of the alternative function at an argument is the universe, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) = V → (𝐹‘𝐴) = ∅) | ||
Theorem | afvnufveq 45128 | The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ≠ V → (𝐹'''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afvvfveq 45129 | The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ∈ 𝐵 → (𝐹'''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afv0fv0 45130 | If the value of the alternative function at an argument is the empty set, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) = ∅ → (𝐹‘𝐴) = ∅) | ||
Theorem | afvfvn0fveq 45131 | If the function's value at an argument is not the empty set, it equals the value of the alternative function at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹‘𝐴) ≠ ∅ → (𝐹'''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afv0nbfvbi 45132 | The function's value at an argument is an element of a set if and only if the value of the alternative function at this argument is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (∅ ∉ 𝐵 → ((𝐹'''𝐴) ∈ 𝐵 ↔ (𝐹‘𝐴) ∈ 𝐵)) | ||
Theorem | afvfv0bi 45133 | The function's value at an argument is the empty set if and only if the value of the alternative function at this argument is either the empty set or the universe. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹‘𝐴) = ∅ ↔ ((𝐹'''𝐴) = ∅ ∨ (𝐹'''𝐴) = V)) | ||
Theorem | afveu 45134* | The value of a function at a unique point, analogous to fveu 6826. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹'''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥}) | ||
Theorem | fnbrafvb 45135 | Equivalence of function value and binary relation, analogous to fnbrfvb 6890. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ 𝐵𝐹𝐶)) | ||
Theorem | fnopafvb 45136 | Equivalence of function value and ordered pair membership, analogous to fnopfvb 6891. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐹)) | ||
Theorem | funbrafvb 45137 | Equivalence of function value and binary relation, analogous to funbrfvb 6892. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹'''𝐴) = 𝐵 ↔ 𝐴𝐹𝐵)) | ||
Theorem | funopafvb 45138 | Equivalence of function value and ordered pair membership, analogous to funopfvb 6893. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹'''𝐴) = 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝐹)) | ||
Theorem | funbrafv 45139 | The second argument of a binary relation on a function is the function's value, analogous to funbrfv 6888. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹'''𝐴) = 𝐵)) | ||
Theorem | funbrafv2b 45140 | Function value in terms of a binary relation, analogous to funbrfv2b 6895. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 ↔ (𝐴 ∈ dom 𝐹 ∧ (𝐹'''𝐴) = 𝐵))) | ||
Theorem | dfafn5a 45141* | Representation of a function in terms of its values, analogous to dffn5 6896 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹'''𝑥))) | ||
Theorem | dfafn5b 45142* | Representation of a function in terms of its values, analogous to dffn5 6896 (only if it is assumed that the function value for each x is a set). (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (∀𝑥 ∈ 𝐴 (𝐹'''𝑥) ∈ 𝑉 → (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹'''𝑥)))) | ||
Theorem | fnrnafv 45143* | The range of a function expressed as a collection of the function's values, analogous to fnrnfv 6897. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹'''𝑥)}) | ||
Theorem | afvelrnb 45144* | A member of a function's range is a value of the function, analogous to fvelrnb 6898 with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝐵)) | ||
Theorem | afvelrnb0 45145* | A member of a function's range is a value of the function, only one direction of implication of fvelrnb 6898. (Contributed by Alexander van der Vekens, 1-Jun-2017.) |
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝐵)) | ||
Theorem | dfaimafn 45146* | Alternate definition of the image of a function, analogous to dfimafn 6900. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝑦}) | ||
Theorem | dfaimafn2 45147* | Alternate definition of the image of a function as an indexed union of singletons of function values, analogous to dfimafn2 6901. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = ∪ 𝑥 ∈ 𝐴 {(𝐹'''𝑥)}) | ||
Theorem | afvelima 45148* | Function value in an image, analogous to fvelima 6903. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹'''𝑥) = 𝐴) | ||
Theorem | afvelrn 45149 | A function's value belongs to its range, analogous to fvelrn 7022. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹'''𝐴) ∈ ran 𝐹) | ||
Theorem | fnafvelrn 45150 | A function's value belongs to its range, analogous to fnfvelrn 7026. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹'''𝐵) ∈ ran 𝐹) | ||
Theorem | fafvelcdm 45151 | A function's value belongs to its codomain, analogous to ffvelcdm 7027. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹'''𝐶) ∈ 𝐵) | ||
Theorem | ffnafv 45152* | A function maps to a class to which all values belong, analogous to ffnfv 7060. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹'''𝑥) ∈ 𝐵)) | ||
Theorem | afvres 45153 | The value of a restricted function, analogous to fvres 6856. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)'''𝐴) = (𝐹'''𝐴)) | ||
Theorem | tz6.12-afv 45154* | Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 6862. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹'''𝐴) = 𝑦) | ||
Theorem | tz6.12-1-afv 45155* | Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12-1 6860. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹'''𝐴) = 𝑦) | ||
Theorem | dmfcoafv 45156 | Domains of a function composition, analogous to dmfco 6932. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺'''𝐴) ∈ dom 𝐹)) | ||
Theorem | afvco2 45157 | Value of a function composition, analogous to fvco2 6933. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = (𝐹'''(𝐺'''𝑋))) | ||
Theorem | rlimdmafv 45158 | Two ways to express that a function has a limit, analogous to rlimdm 15367. (Contributed by Alexander van der Vekens, 27-Nov-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 '''𝐹))) | ||
Theorem | aoveq123d 45159 | Equality deduction for operation value, analogous to oveq123d 7370. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐶)) = ((𝐵𝐺𝐷)) ) | ||
Theorem | nfaov 45160 | Bound-variable hypothesis builder for operation value, analogous to nfov 7379. To prove a deduction version of this analogous to nfovd 7378 is not quickly possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of alternative operation values is based on are not available (see nfafv 45117). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 ((𝐴𝐹𝐵)) | ||
Theorem | csbaovg 45161 | Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌ ((𝐵𝐹𝐶)) = ((⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶)) ) | ||
Theorem | aovfundmoveq 45162 | If a class is a function restricted to an ordered pair of its domain, then the value of the operation on this pair is equal for both definitions. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐹 defAt ⟨𝐴, 𝐵⟩ → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵)) | ||
Theorem | aovnfundmuv 45163 | If an ordered pair is not in the domain of a class or the class is not a function restricted to the ordered pair, then the operation value for this pair is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (¬ 𝐹 defAt ⟨𝐴, 𝐵⟩ → ((𝐴𝐹𝐵)) = V) | ||
Theorem | ndmaov 45164 | The value of an operation outside its domain, analogous to ndmafv 45121. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (¬ ⟨𝐴, 𝐵⟩ ∈ dom 𝐹 → ((𝐴𝐹𝐵)) = V) | ||
Theorem | ndmaovg 45165 | The value of an operation outside its domain, analogous to ndmovg 7529. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((dom 𝐹 = (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → ((𝐴𝐹𝐵)) = V) | ||
Theorem | aovvdm 45166 | If the operation value of a class for an ordered pair is a set, the ordered pair is contained in the domain of the class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → ⟨𝐴, 𝐵⟩ ∈ dom 𝐹) | ||
Theorem | nfunsnaov 45167 | If the restriction of a class to a singleton is not a function, its operation value is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (¬ Fun (𝐹 ↾ {⟨𝐴, 𝐵⟩}) → ((𝐴𝐹𝐵)) = V) | ||
Theorem | aovvfunressn 45168 | If the operation value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → Fun (𝐹 ↾ {⟨𝐴, 𝐵⟩})) | ||
Theorem | aovprc 45169 | The value of an operation when the one of the arguments is a proper class, analogous to ovprc 7387. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Rel dom 𝐹 ⇒ ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐹𝐵)) = V) | ||
Theorem | aovrcl 45170 | Reverse closure for an operation value, analogous to afvvv 45126. In contrast to ovrcl 7390, elementhood of the operation's value in a set is required, not containing an element. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Rel dom 𝐹 ⇒ ⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | aovpcov0 45171 | If the alternative value of the operation on an ordered pair is the universal class, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) = V → (𝐴𝐹𝐵) = ∅) | ||
Theorem | aovnuoveq 45172 | The alternative value of the operation on an ordered pair equals the operation's value at this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) ≠ V → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵)) | ||
Theorem | aovvoveq 45173 | The alternative value of the operation on an ordered pair equals the operation's value on this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵)) | ||
Theorem | aov0ov0 45174 | If the alternative value of the operation on an ordered pair is the empty set, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ( ((𝐴𝐹𝐵)) = ∅ → (𝐴𝐹𝐵) = ∅) | ||
Theorem | aovovn0oveq 45175 | If the operation's value at an argument is not the empty set, it equals the value of the alternative operation at this argument. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐴𝐹𝐵) ≠ ∅ → ((𝐴𝐹𝐵)) = (𝐴𝐹𝐵)) | ||
Theorem | aov0nbovbi 45176 | The operation's value on an ordered pair is an element of a set if and only if the alternative value of the operation on this ordered pair is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (∅ ∉ 𝐶 → ( ((𝐴𝐹𝐵)) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶)) | ||
Theorem | aovov0bi 45177 | The operation's value on an ordered pair is the empty set if and only if the alternative value of the operation on this ordered pair is either the empty set or the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐴𝐹𝐵) = ∅ ↔ ( ((𝐴𝐹𝐵)) = ∅ ∨ ((𝐴𝐹𝐵)) = V)) | ||
Theorem | rspceaov 45178* | A frequently used special case of rspc2ev 3590 for operation values, analogous to rspceov 7396. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = ((𝐶𝐹𝐷)) ) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = ((𝑥𝐹𝑦)) ) | ||
Theorem | fnotaovb 45179 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6891. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ( ((𝐶𝐹𝐷)) = 𝑅 ↔ ⟨𝐶, 𝐷, 𝑅⟩ ∈ 𝐹)) | ||
Theorem | ffnaov 45180* | An operation maps to a class to which all values belong, analogous to ffnov 7475. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑥𝐹𝑦)) ∈ 𝐶)) | ||
Theorem | faovcl 45181 | Closure law for an operation, analogous to fovcl 7476. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) ∈ 𝐶) | ||
Theorem | aovmpt4g 45182* | Value of a function given by the maps-to notation, analogous to ovmpt4g 7494. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → ((𝑥𝐹𝑦)) = 𝐶) | ||
Theorem | aoprssdm 45183* | Domain of closure of an operation. In contrast to oprssdm 7527, no additional property for S (¬ ∅ ∈ 𝑆) is required! (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦)) ∈ 𝑆) ⇒ ⊢ (𝑆 × 𝑆) ⊆ dom 𝐹 | ||
Theorem | ndmaovcl 45184 | The "closure" of an operation outside its domain, when the operation's value is a set in contrast to ndmovcl 7531 where it is required that the domain contains the empty set (∅ ∈ 𝑆). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) ∈ 𝑆) & ⊢ ((𝐴𝐹𝐵)) ∈ V ⇒ ⊢ ((𝐴𝐹𝐵)) ∈ 𝑆 | ||
Theorem | ndmaovrcl 45185 | Reverse closure law, in contrast to ndmovrcl 7532 where it is required that the operation's domain doesn't contain the empty set (¬ ∅ ∈ 𝑆), no additional asumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ ( ((𝐴𝐹𝐵)) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) | ||
Theorem | ndmaovcom 45186 | Any operation is commutative outside its domain, analogous to ndmovcom 7533. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) = ((𝐵𝐹𝐴)) ) | ||
Theorem | ndmaovass 45187 | Any operation is associative outside its domain. In contrast to ndmovass 7534 where it is required that the operation's domain doesn't contain the empty set (¬ ∅ ∈ 𝑆), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (( ((𝐴𝐹𝐵)) 𝐹𝐶)) = ((𝐴𝐹 ((𝐵𝐹𝐶)) )) ) | ||
Theorem | ndmaovdistr 45188 | Any operation is distributive outside its domain. In contrast to ndmovdistr 7535 where it is required that the operation's domain doesn't contain the empty set (¬ ∅ ∈ 𝑆), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ dom 𝐺 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) ) | ||
In the following, a second approach is followed to define function values alternately to df-afv 45101. The current definition of the value (𝐹‘𝐴) of a function 𝐹 at an argument 𝐴 (see df-fv 6499) assures that this value is always a set, see fex 7170. This is because this definition can be applied to any classes 𝐹 and 𝐴, and evaluates to the empty set when it is not meaningful (as shown by ndmfv 6872 and fvprc 6829). "(𝐹‘𝐴) is meaningful" means "the class 𝐹 regarded as function is defined at the argument 𝐴" in this context. This is also expressed by 𝐹 defAt 𝐴, see df-dfat 45100. In the theory of partial functions, it is a common case that 𝐹 is not defined at 𝐴. Although it is very convenient for many theorems on functions and their proofs, there are some cases in which from (𝐹‘𝐴) = ∅ alone it cannot be decided/derived whether (𝐹‘𝐴) is meaningful (𝐹 is actually a function which is defined for 𝐴 and really has the function value ∅ at 𝐴) or not. Therefore, additional assumptions are required, such as ∅ ∉ ran 𝐹, ∅ ∈ ran 𝐹, 𝐹 defAt 𝐴, or Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 (see, for example, ndmfvrcl 6873). To avoid such an ambiguity, an alternative definition (𝐹''''𝐴) (see df-afv2 45190) would be possible which evaluates to a set not belonging to the range of 𝐹 ((𝐹''''𝐴) = 𝒫 ∪ ran 𝐹) if it is not meaningful (see ndfatafv2 45192). We say "(𝐹''''𝐴) is not defined (or undefined)" if (𝐹''''𝐴) is not in the range of 𝐹 ((𝐹''''𝐴) ∉ ran 𝐹). Because of afv2ndefb 45205, this is equivalent to ((𝐹''''𝐴) = 𝒫 ∪ ran 𝐹. If (𝐹''''𝐴) is in the range of 𝐹 ((𝐹''''𝐴) ∈ ran 𝐹), we say that "(𝐹''''𝐴) is defined". If ran 𝐹 is a set, we can use the symbol Undef to express that (𝐹''''𝐴) is not defined: (𝐹''''𝐴) = (Undef‘ran 𝐹) (see ndfatafv2undef 45193). We could have used this symbol directly to define the alternate value of a function, which would have the advantage that (𝐹''''𝐴) would always be a set. But first this symbol is defined using the original function value, which would not make it possible to replace the original definition by the alternate definition, and second we would have to assume that ran 𝐹 ∈ V in most of the theorems. To summarize, that means (𝐹''''𝐴) ∉ ran 𝐹 → (𝐹‘𝐴) = ∅ (see afv2ndeffv0 45241), but (𝐹‘𝐴) = ∅ → (𝐹''''𝐴) ∉ ran 𝐹 is not generally valid, see afv2fv0 45246. The alternate definition, however, corresponds to the current definition ((𝐹‘𝐴) = (𝐹''''𝐴)) if the function 𝐹 is defined at 𝐴 (see dfatafv2eqfv 45242). With this definition the following intuitive equivalence holds: (𝐹 defAt 𝐴 ↔ (𝐹''''𝐴) ∈ ran 𝐹), see dfatafv2rnb 45208. An interesting question would be if (𝐹‘𝐴) could be replaced by (𝐹'''𝐴) in most of the theorems based on function values. If we look at the (currently 24) proofs using the definition df-fv 6499 of (𝐹‘𝐴), we see that analogues for the following 7 theorems can be proven using the alternative definition: fveq1 6836-> afv2eq1 45197, fveq2 6837-> afv2eq2 45198, nffv 6847-> nfafv2 45199, csbfv12 6885-> csbafv212g , rlimdm 15367-> rlimdmafv2 45239, tz6.12-1 6860-> tz6.12-1-afv2 45222, fveu 6826-> afv2eu 45219. Six theorems proved by directly using df-fv 6499 are within a mathbox (fvsb 42496, uncov 35954) or not used (rlimdmafv 45158, avril1 29205) or experimental (dfafv2 45113, dfafv22 45240). However, the remaining 11 theorems proved by directly using df-fv 6499 are used more or less often: * fvex 6850: used in about 1600 proofs: Only if the function is defined at the argument, or the range of the function/class is a set, analog theorems can be proven (dfatafv2ex 45194 resp. afv2ex 45195). All of these 1600 proofs have to be checked if one of these two theorems can be used instead of fvex 6850. * fvres 6856: used in about 400 proofs : Only if the function is defined at the argument, an analog theorem can be proven (afv2res 45220). In the undefined case such a theorem cannot exist (without additional assumtions), because the range of (𝐹 ↾ 𝐵) is mostly different from the range of 𝐹, and therefore also the "undefined" values are different. All of these 400 proofs have to be checked if afv2res 45220 can be used instead of fvres 6856. * tz6.12-2 6825 (-> tz6.12-2-afv2 45218): root theorem of many theorems which have not a strict analogue, and which are used many times: ** fvprc 6829 (-> afv2prc 45207), used in 193 proofs, ** tz6.12i 6865 (-> tz6.12i-afv2 45224), used - indirectly via fvbr0 6866 and fvrn0 6867 - in 19 proofs, and in fvclss 7183 used in fvclex 7881 used in fvresex 7882 (which is not used!) and in dcomex 10316 (used in 4 proofs), ** ndmfv 6872 (-> ndmafv2nrn ), used in 124 proofs ** nfunsn 6879 (-> nfunsnafv2 ), used by fvfundmfvn0 6880 (used in 3 proofs), and dffv2 6931 (not used) ** funpartfv 34425, setrec2lem1 46887 (mathboxes) * fv2 6832: only used by elfv 6835, which is only used by fv3 6855, which is not used. * dffv3 6833 (-> dfafv23 ): used by dffv4 6834 (the previous "df-fv"), which now is only used in mathboxes (csbfv12gALTVD 42945), by shftval 14892 (itself used in 11 proofs), by dffv5 34404 (mathbox) and by fvco2 6933 (-> afv2co2 45238). * fvopab5 6975: used only by ajval 29601 (not used) and by adjval 30630, which is used in adjval2 30631 (not used) and in adjbdln 30823 (used in 7 proofs). * zsum 15537: used (via isum 15538, sum0 15540, sumss 15543 and fsumsers 15547) in 76 proofs. * isumshft 15658: used in pserdv2 25711 (used in logtayl 25937, binomcxplemdvsum 42399) , eftlub 15925 (used in 4 proofs), binomcxplemnotnn0 42400 (used in binomcxp 42401 only) and logtayl 25937 (used in 4 proofs). * ovtpos 8139: used in 16 proofs. * zprod 15754: used in 3 proofs: iprod 15755, zprodn0 15756 and prodss 15764 * iprodclim3 15817: not used! As a result of this analysis we can say that the current definition of a function value is crucial for Metamath and cannot be exchanged easily with an alternative definition. While fv2 6832, dffv3 6833, fvopab5 6975, zsum 15537, isumshft 15658, ovtpos 8139 and zprod 15754 are not critical or are, hopefully, also valid for the alternative definition, fvex 6850, fvres 6856 and tz6.12-2 6825 (and the theorems based on them) are essential for the current definition of function values. | ||
Syntax | cafv2 45189 | Extend the definition of a class to include the alternate function value. Read: "the value of 𝐹 at 𝐴 " or "𝐹 of 𝐴". For using several apostrophes as a symbol see comment for cafv 45098. |
class (𝐹''''𝐴) | ||
Definition | df-afv2 45190* | Alternate definition of the value of a function, (𝐹''''𝐴), also known as function application (and called "alternate function value" in the following). In contrast to (𝐹‘𝐴) = ∅ (see comment of df-fv 6499, and especially ndmfv 6872), (𝐹''''𝐴) is guaranteed not to be in the range of 𝐹 if 𝐹 is not defined at 𝐴 (whereas ∅ can be a member of ran 𝐹). (Contributed by AV, 2-Sep-2022.) |
⊢ (𝐹''''𝐴) = if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), 𝒫 ∪ ran 𝐹) | ||
Theorem | dfatafv2iota 45191* | If a function is defined at a class 𝐴 the alternate function value at 𝐴 is the unique value assigned to 𝐴 by the function (analogously to (𝐹‘𝐴)). (Contributed by AV, 2-Sep-2022.) |
⊢ (𝐹 defAt 𝐴 → (𝐹''''𝐴) = (℩𝑥𝐴𝐹𝑥)) | ||
Theorem | ndfatafv2 45192 | The alternate function value at a class 𝐴 if the function is not defined at this set 𝐴. (Contributed by AV, 2-Sep-2022.) |
⊢ (¬ 𝐹 defAt 𝐴 → (𝐹''''𝐴) = 𝒫 ∪ ran 𝐹) | ||
Theorem | ndfatafv2undef 45193 | The alternate function value at a class 𝐴 is undefined if the function, whose range is a set, is not defined at 𝐴. (Contributed by AV, 2-Sep-2022.) |
⊢ ((ran 𝐹 ∈ 𝑉 ∧ ¬ 𝐹 defAt 𝐴) → (𝐹''''𝐴) = (Undef‘ran 𝐹)) | ||
Theorem | dfatafv2ex 45194 | The alternate function value at a class 𝐴 is always a set if the function/class 𝐹 is defined at 𝐴. (Contributed by AV, 6-Sep-2022.) |
⊢ (𝐹 defAt 𝐴 → (𝐹''''𝐴) ∈ V) | ||
Theorem | afv2ex 45195 | The alternate function value is always a set if the range of the function is a set. (Contributed by AV, 2-Sep-2022.) |
⊢ (ran 𝐹 ∈ 𝑉 → (𝐹''''𝐴) ∈ V) | ||
Theorem | afv2eq12d 45196 | Equality deduction for function value, analogous to fveq12d 6844. (Contributed by AV, 4-Sep-2022.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹''''𝐴) = (𝐺''''𝐵)) | ||
Theorem | afv2eq1 45197 | Equality theorem for function value, analogous to fveq1 6836. (Contributed by AV, 4-Sep-2022.) |
⊢ (𝐹 = 𝐺 → (𝐹''''𝐴) = (𝐺''''𝐴)) | ||
Theorem | afv2eq2 45198 | Equality theorem for function value, analogous to fveq2 6837. (Contributed by AV, 4-Sep-2022.) |
⊢ (𝐴 = 𝐵 → (𝐹''''𝐴) = (𝐹''''𝐵)) | ||
Theorem | nfafv2 45199 | Bound-variable hypothesis builder for function value, analogous to nffv 6847. To prove a deduction version of this analogous to nffvd 6849 is not easily possible because a deduction version of nfdfat 45108 cannot be shown easily. (Contributed by AV, 4-Sep-2022.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹''''𝐴) | ||
Theorem | csbafv212g 45200 | Move class substitution in and out of a function value, analogous to csbfv12 6885, with a direct proof proposed by Mario Carneiro, analogous to csbov123 7391. (Contributed by AV, 4-Sep-2022.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐹''''𝐵) = (⦋𝐴 / 𝑥⦌𝐹''''⦋𝐴 / 𝑥⦌𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |