Home | Metamath
Proof Explorer Theorem List (p. 434 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | reuf1od 43301* | There is exactly one element in each of two isomorphic sets. (Contributed by AV, 19-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵) & ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | euoreqb 43302* | There is a set which is equal to one of two other sets iff the other sets are equal. (Contributed by AV, 24-Jan-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | 2reu3 43303* | Double restricted existential uniqueness, analogous to 2eu3 2735. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) | ||
Theorem | 2reu7 43304* | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2741. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑)) | ||
Theorem | 2reu8 43305* | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2742. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!𝑥 ∈ 𝐴∃!𝑦 ∈ 𝐵 using 2reu7 43304. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑)) | ||
Theorem | 2reu8i 43306* | Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 43305. The involved wffs depend on the setvar variables as follows: ph(x,y), ta(v,y), ch(x,w), th(v,w), et(x,b), ps(a,b), ze(a,w) (Contributed by AV, 1-Apr-2023.) |
⊢ (𝑥 = 𝑣 → (𝜑 ↔ 𝜏)) & ⊢ (𝑥 = 𝑣 → (𝜒 ↔ 𝜃)) & ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑏 → (𝜑 ↔ 𝜂)) & ⊢ (𝑥 = 𝑎 → (𝜒 ↔ 𝜁)) & ⊢ (((𝜒 → 𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤) & ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))) | ||
Theorem | 2reuimp0 43307* | Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification. The involved wffs depend on the setvar variables as follows: ph(a,b), th(a,c), ch(d,b), ta(d,c), et(a,e), ps(a,f) (Contributed by AV, 13-Mar-2023.) |
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒)) & ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂)) & ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑 → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))) | ||
Theorem | 2reuimp 43308* | Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification if the class of the quantified elements is not empty. (Contributed by AV, 13-Mar-2023.) |
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒)) & ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂)) & ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓)) ⇒ ⊢ ((𝑉 ≠ ∅ ∧ ∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝜒 ∧ (𝜏 → 𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑 ∧ 𝑒 = 𝑓))))) | ||
The current definition of the value (𝐹‘𝐴) of a function 𝐹 at an argument 𝐴 (see df-fv 6357) assures that this value is always a set, see fex 6983. 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 6694 and fvprc 6657). 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 𝐹 or Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 (see, for example, ndmfvrcl 6695). To avoid such an ambiguity, an alternative definition (𝐹'''𝐴) (see df-afv 43313) would be possible which evaluates to the universal class ((𝐹'''𝐴) = V) if it is not meaningful (see afvnfundmuv 43332, ndmafv 43333, afvprc 43337 and nfunsnafv 43335), and which corresponds to the current definition ((𝐹‘𝐴) = (𝐹'''𝐴)) if it is (see afvfundmfveq 43331). That means (𝐹'''𝐴) = V → (𝐹‘𝐴) = ∅ (see afvpcfv0 43339), but (𝐹‘𝐴) = ∅ → (𝐹'''𝐴) = V is not generally valid. In the theory of partial functions, it is a common case that 𝐹 is not defined at 𝐴, which also would result in (𝐹'''𝐴) = V. In this context we say (𝐹'''𝐴) "is not defined" instead of "is not meaningful". With this definition the following intuitive equivalence holds: (𝐹'''𝐴) ∈ V <-> "(𝐹'''𝐴) is meaningful/defined". 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 19) proofs using the definition df-fv 6357 of (𝐹‘𝐴), we see that analogues for the following 8 theorems can be proven using the alternative definition: fveq1 6663-> afveq1 43327, fveq2 6664-> afveq2 43328, nffv 6674-> nfafv 43329, csbfv12 6707-> csbafv12g , fvres 6683-> afvres 43365, rlimdm 14902-> rlimdmafv 43370, tz6.12-1 6686-> tz6.12-1-afv 43367, fveu 6655-> afveu 43346. Three theorems proved by directly using df-fv 6357 are within a mathbox (fvsb 40777) or not used (isumclim3 15108, avril1 28236). However, the remaining 8 theorems proved by directly using df-fv 6357 are used more or less often: * fvex 6677: used in about 1750 proofs. * tz6.12-1 6686: root theorem of many theorems which have not a strict analogue, and which are used many times: fvprc 6657 (used in about 127 proofs), tz6.12i 6690 (used - indirectly via fvbr0 6691 and fvrn0 6692- in 18 proofs, and in fvclss 6995 used in fvclex 7654 used in fvresex 7655, which is not used!), dcomex 9863 (used in 4 proofs), ndmfv 6694 (used in 86 proofs) and nfunsn 6701 (used by dffv2 6750 which is not used). * fv2 6659: only used by elfv 6662, which is only used by fv3 6682, which is not used. * dffv3 6660: used by dffv4 6661 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTVD 41226), by shftval 14427 (itself used in 9 proofs), by dffv5 33380 (mathbox) and by fvco2 6752, which has the analogue afvco2 43369. * fvopab5 6794: used only by ajval 28632 (not used) and by adjval 29661 (used - indirectly - in 9 proofs). * zsum 15069: used (via isum 15070, sum0 15072 and fsumsers 15079) in more than 90 proofs. * isumshft 15188: used in pserdv2 25012 and (via logtayl 25237) 4 other proofs. * ovtpos 7901: used in 14 proofs. 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 6659, dffv3 6660, fvopab5 6794, zsum 15069, isumshft 15188 and ovtpos 7901 are not critical or are, hopefully, also valid for the alternative definition, fvex 6677 and tz6.12-1 6686 (and the theorems based on them) are essential for the current definition of function values. With the same arguments, an alternative definition of operation values ((𝐴𝑂𝐵)) could be meaningful to avoid ambiguities, see df-aov 43314. For additional details, see https://groups.google.com/g/metamath/c/cteNUppB6A4 43314. | ||
Syntax | wdfat 43309 | Extend the definition of a wff to include the "defined at" predicate. Read: "(the function) 𝐹 is defined at (the argument) 𝐴". In a previous version, the token "def@" was used. However, since the @ is used (informally) as a replacement for $ in commented out sections that may be deleted some day. While there is no violation of any standard to use the @ in a token, it could make the search for such commented-out sections slightly more difficult. (See remark of Norman Megill at https://groups.google.com/g/metamath/c/cteNUppB6A4). |
wff 𝐹 defAt 𝐴 | ||
Syntax | cafv 43310 | Extend the definition of a class to include the value of a function. Read: "the value of 𝐹 at 𝐴 " or "𝐹 of 𝐴". In a previous version, the symbol " ' " was used. However, since the similarity with the symbol ‘ used for the current definition of a function's value (see df-fv 6357), which, by the way, was intended to visualize that in many cases ‘ and " ' " are exchangeable, makes reading the theorems, especially those which uses both definitions as dfafv2 43325, very difficult, 3 apostrophes ''' are used now so that it's easier to distinguish from df-fv 6357 and df-ima 5562. And not three backticks ( three times ‘) since that would be annoying to escape in a comment. (See remark of Norman Megill and Gerard Lang at https://groups.google.com/g/metamath/c/cteNUppB6A4 5562). |
class (𝐹'''𝐴) | ||
Syntax | caov 43311 | Extend class notation to include the value of an operation 𝐹 (such as +) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by a pair of parentheses in contrast to the current definition, see df-ov 7153. |
class ((𝐴𝐹𝐵)) | ||
Definition | df-dfat 43312 | Definition of the predicate that determines if some class 𝐹 is defined as function for an argument 𝐴 or, in other words, if the function value for some class 𝐹 for an argument 𝐴 is defined. We say that 𝐹 is defined at 𝐴 if a 𝐹 is a function restricted to the member 𝐴 of its domain. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) | ||
Definition | df-afv 43313* | Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹‘𝐴) = ∅ (see df-fv 6357 and ndmfv 6694), (𝐹'''𝐴) = 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 43314 | Define the value of an operation. In contrast to df-ov 7153, the alternative definition for a function value (see df-afv 43313) 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 43315* | Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 = 𝑋) & ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ 𝜃)) | ||
Theorem | nvelim 43316 | If a class is the universal class it doesn't belong to any class, generalization of nvel 5212. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐴 = V → ¬ 𝐴 ∈ 𝐵) | ||
Theorem | alneu 43317 | 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 43318* | 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 43319 | Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 defAt 𝐴 ↔ 𝐺 defAt 𝐵)) | ||
Theorem | nfdfat 43320 | 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 43321* | 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 43322 | A function is defined at any element of its domain. (Contributed by AV, 2-Sep-2022.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 𝐹 defAt 𝐴) | ||
Theorem | dfatprc 43323 | A function is not defined at a proper class. (Contributed by AV, 1-Sep-2022.) |
⊢ (¬ 𝐴 ∈ V → ¬ 𝐹 defAt 𝐴) | ||
Theorem | dfatelrn 43324 | 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 43325 | 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 43326 | Equality deduction for function value, analogous to fveq12d 6671. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹'''𝐴) = (𝐺'''𝐵)) | ||
Theorem | afveq1 43327 | Equality theorem for function value, analogous to fveq1 6663. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐹 = 𝐺 → (𝐹'''𝐴) = (𝐺'''𝐴)) | ||
Theorem | afveq2 43328 | Equality theorem for function value, analogous to fveq1 6663. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐴 = 𝐵 → (𝐹'''𝐴) = (𝐹'''𝐵)) | ||
Theorem | nfafv 43329 | Bound-variable hypothesis builder for function value, analogous to nffv 6674. To prove a deduction version of this analogous to nffvd 6676 is not easily possible because a deduction version of nfdfat 43320 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹'''𝐴) | ||
Theorem | csbafv12g 43330 | Move class substitution in and out of a function value, analogous to csbfv12 6707, with a direct proof proposed by Mario Carneiro, analogous to csbov123 7192. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐹'''𝐵) = (⦋𝐴 / 𝑥⦌𝐹'''⦋𝐴 / 𝑥⦌𝐵)) | ||
Theorem | afvfundmfveq 43331 | 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 43332 | 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 43333 | The value of a class outside its domain is the universe, compare with ndmfv 6694. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹'''𝐴) = V) | ||
Theorem | afvvdm 43334 | 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 43335 | If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 6701. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹'''𝐴) = V) | ||
Theorem | afvvfunressn 43336 | 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 43337 | A function's value at a proper class is the universe, compare with fvprc 6657. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ 𝐴 ∈ V → (𝐹'''𝐴) = V) | ||
Theorem | afvvv 43338 | 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 43339 | 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 43340 | 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 43341 | 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 43342 | 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 43343 | 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 43344 | 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 43345 | 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 43346* | The value of a function at a unique point, analogous to fveu 6655. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹'''𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥}) | ||
Theorem | fnbrafvb 43347 | Equivalence of function value and binary relation, analogous to fnbrfvb 6712. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ 𝐵𝐹𝐶)) | ||
Theorem | fnopafvb 43348 | Equivalence of function value and ordered pair membership, analogous to fnopfvb 6713. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹'''𝐵) = 𝐶 ↔ 〈𝐵, 𝐶〉 ∈ 𝐹)) | ||
Theorem | funbrafvb 43349 | Equivalence of function value and binary relation, analogous to funbrfvb 6714. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹'''𝐴) = 𝐵 ↔ 𝐴𝐹𝐵)) | ||
Theorem | funopafvb 43350 | Equivalence of function value and ordered pair membership, analogous to funopfvb 6715. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹'''𝐴) = 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝐹)) | ||
Theorem | funbrafv 43351 | The second argument of a binary relation on a function is the function's value, analogous to funbrfv 6710. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹'''𝐴) = 𝐵)) | ||
Theorem | funbrafv2b 43352 | Function value in terms of a binary relation, analogous to funbrfv2b 6717. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (Fun 𝐹 → (𝐴𝐹𝐵 ↔ (𝐴 ∈ dom 𝐹 ∧ (𝐹'''𝐴) = 𝐵))) | ||
Theorem | dfafn5a 43353* | Representation of a function in terms of its values, analogous to dffn5 6718 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹'''𝑥))) | ||
Theorem | dfafn5b 43354* | Representation of a function in terms of its values, analogous to dffn5 6718 (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 43355* | The range of a function expressed as a collection of the function's values, analogous to fnrnfv 6719. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹'''𝑥)}) | ||
Theorem | afvelrnb 43356* | A member of a function's range is a value of the function, analogous to fvelrnb 6720 with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝐵)) | ||
Theorem | afvelrnb0 43357* | A member of a function's range is a value of the function, only one direction of implication of fvelrnb 6720. (Contributed by Alexander van der Vekens, 1-Jun-2017.) |
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝐵)) | ||
Theorem | dfaimafn 43358* | Alternate definition of the image of a function, analogous to dfimafn 6722. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝐹'''𝑥) = 𝑦}) | ||
Theorem | dfaimafn2 43359* | Alternate definition of the image of a function as an indexed union of singletons of function values, analogous to dfimafn2 6723. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = ∪ 𝑥 ∈ 𝐴 {(𝐹'''𝑥)}) | ||
Theorem | afvelima 43360* | Function value in an image, analogous to fvelima 6725. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹'''𝑥) = 𝐴) | ||
Theorem | afvelrn 43361 | A function's value belongs to its range, analogous to fvelrn 6838. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹'''𝐴) ∈ ran 𝐹) | ||
Theorem | fnafvelrn 43362 | A function's value belongs to its range, analogous to fnfvelrn 6842. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹'''𝐵) ∈ ran 𝐹) | ||
Theorem | fafvelrn 43363 | A function's value belongs to its codomain, analogous to ffvelrn 6843. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹'''𝐶) ∈ 𝐵) | ||
Theorem | ffnafv 43364* | A function maps to a class to which all values belong, analogous to ffnfv 6876. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹'''𝑥) ∈ 𝐵)) | ||
Theorem | afvres 43365 | The value of a restricted function, analogous to fvres 6683. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)'''𝐴) = (𝐹'''𝐴)) | ||
Theorem | tz6.12-afv 43366* | Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 6687. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ ((〈𝐴, 𝑦〉 ∈ 𝐹 ∧ ∃!𝑦〈𝐴, 𝑦〉 ∈ 𝐹) → (𝐹'''𝐴) = 𝑦) | ||
Theorem | tz6.12-1-afv 43367* | Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12-1 6686. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹'''𝐴) = 𝑦) | ||
Theorem | dmfcoafv 43368 | Domains of a function composition, analogous to dmfco 6751. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺'''𝐴) ∈ dom 𝐹)) | ||
Theorem | afvco2 43369 | Value of a function composition, analogous to fvco2 6752. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = (𝐹'''(𝐺'''𝑋))) | ||
Theorem | rlimdmafv 43370 | Two ways to express that a function has a limit, analogous to rlimdm 14902. (Contributed by Alexander van der Vekens, 27-Nov-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 '''𝐹))) | ||
Theorem | aoveq123d 43371 | Equality deduction for operation value, analogous to oveq123d 7171. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐶)) = ((𝐵𝐺𝐷)) ) | ||
Theorem | nfaov 43372 | Bound-variable hypothesis builder for operation value, analogous to nfov 7180. To prove a deduction version of this analogous to nfovd 7179 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 43329). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 ((𝐴𝐹𝐵)) | ||
Theorem | csbaovg 43373 | Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌ ((𝐵𝐹𝐶)) = ((⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶)) ) | ||
Theorem | aovfundmoveq 43374 | 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 43375 | 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 43376 | The value of an operation outside its domain, analogous to ndmafv 43333. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (¬ 〈𝐴, 𝐵〉 ∈ dom 𝐹 → ((𝐴𝐹𝐵)) = V) | ||
Theorem | ndmaovg 43377 | The value of an operation outside its domain, analogous to ndmovg 7325. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((dom 𝐹 = (𝑅 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → ((𝐴𝐹𝐵)) = V) | ||
Theorem | aovvdm 43378 | 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 43379 | 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 43380 | 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 43381 | The value of an operation when the one of the arguments is a proper class, analogous to ovprc 7188. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Rel dom 𝐹 ⇒ ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐹𝐵)) = V) | ||
Theorem | aovrcl 43382 | Reverse closure for an operation value, analogous to afvvv 43338. In contrast to ovrcl 7191, 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 43383 | 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 43384 | 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 43385 | 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 43386 | 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 43387 | 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 43388 | 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 43389 | 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 43390* | A frequently used special case of rspc2ev 3634 for operation values, analogous to rspceov 7197. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = ((𝐶𝐹𝐷)) ) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = ((𝑥𝐹𝑦)) ) | ||
Theorem | fnotaovb 43391 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6713. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ( ((𝐶𝐹𝐷)) = 𝑅 ↔ 〈𝐶, 𝐷, 𝑅〉 ∈ 𝐹)) | ||
Theorem | ffnaov 43392* | An operation maps to a class to which all values belong, analogous to ffnov 7272. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑥𝐹𝑦)) ∈ 𝐶)) | ||
Theorem | faovcl 43393 | Closure law for an operation, analogous to fovcl 7273. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) ∈ 𝐶) | ||
Theorem | aovmpt4g 43394* | Value of a function given by the maps-to notation, analogous to ovmpt4g 7291. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → ((𝑥𝐹𝑦)) = 𝐶) | ||
Theorem | aoprssdm 43395* | Domain of closure of an operation. In contrast to oprssdm 7323, no additional property for S (¬ ∅ ∈ 𝑆) is required! (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦)) ∈ 𝑆) ⇒ ⊢ (𝑆 × 𝑆) ⊆ dom 𝐹 | ||
Theorem | ndmaovcl 43396 | The "closure" of an operation outside its domain, when the operation's value is a set in contrast to ndmovcl 7327 where it is required that the domain contains the empty set (∅ ∈ 𝑆). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) ∈ 𝑆) & ⊢ ((𝐴𝐹𝐵)) ∈ V ⇒ ⊢ ((𝐴𝐹𝐵)) ∈ 𝑆 | ||
Theorem | ndmaovrcl 43397 | Reverse closure law, in contrast to ndmovrcl 7328 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 43398 | Any operation is commutative outside its domain, analogous to ndmovcom 7329. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ dom 𝐹 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵)) = ((𝐵𝐹𝐴)) ) | ||
Theorem | ndmaovass 43399 | Any operation is associative outside its domain. In contrast to ndmovass 7330 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 43400 | Any operation is distributive outside its domain. In contrast to ndmovdistr 7331 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 𝐺 = (𝑆 × 𝑆) ⇒ ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐺 ((𝐵𝐹𝐶)) )) = (( ((𝐴𝐺𝐵)) 𝐹 ((𝐴𝐺𝐶)) )) ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |