Metamath Proof Explorer


Table of Contents - 20.43.4. Alternative definitions of function and operation values

The current definition of the value of a function at an argument (see df-fv) assures that this value is always a set, see fex. 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 and fvprc).

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 , or (see, for example, ndmfvrcl).

To avoid such an ambiguity, an alternative definition (see df-afv) would be possible which evaluates to the universal class () if it is not meaningful (see afvnfundmuv, ndmafv, afvprc and nfunsnafv), and which corresponds to the current definition () if it is (see afvfundmfveq). That means (see afvpcfv0), but 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 . In this context we say "is not defined" instead of "is not meaningful".

With this definition the following intuitive equivalence holds: <-> " 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 of , we see that analogues for the following 8 theorems can be proven using the alternative definition: fveq1-> afveq1, fveq2-> afveq2, nffv-> nfafv, csbfv12-> csbafv12g , fvres-> afvres, rlimdm-> rlimdmafv, tz6.12-1-> tz6.12-1-afv, fveu-> afveu.

Three theorems proved by directly using df-fv are within a mathbox (fvsb) or not used (isumclim3, avril1).

However, the remaining 8 theorems proved by directly using df-fv are used more or less often:

* fvex: used in about 1750 proofs.

* tz6.12-1: root theorem of many theorems which have not a strict analogue, and which are used many times: fvprc (used in about 127 proofs), tz6.12i (used - indirectly via fvbr0 and fvrn0- in 18 proofs, and in fvclss used in fvclex used in fvresex, which is not used!), dcomex (used in 4 proofs), ndmfv (used in 86 proofs) and nfunsn (used by dffv2 which is not used).

* fv2: only used by elfv, which is only used by fv3, which is not used.

* dffv3: used by dffv4 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTVD), by shftval (itself used in 9 proofs), by dffv5 (mathbox) and by fvco2, which has the analogue afvco2.

* fvopab5: used only by ajval (not used) and by adjval (used - indirectly - in 9 proofs).

* zsum: used (via isum, sum0 and fsumsers) in more than 90 proofs.

* isumshft: used in pserdv2 and (via logtayl) 4 other proofs.

* ovtpos: 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, dffv3, fvopab5, zsum, isumshft and ovtpos are not critical or are, hopefully, also valid for the alternative definition, fvex and tz6.12-1 (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.

For additional details, see https://groups.google.com/g/metamath/c/cteNUppB6A4.

  1. wdfat
  2. cafv
  3. caov
  4. df-dfat
  5. df-afv
  6. df-aov
  7. Restricted quantification (extension)
    1. ralbinrald
  8. The universal class (extension)
    1. nvelim
  9. Introduce the Axiom of Power Sets (extension)
    1. alneu
    2. eu2ndop1stv
  10. Predicate "defined at"
    1. dfateq12d
    2. nfdfat
    3. dfdfat2
    4. fundmdfat
    5. dfatprc
    6. dfatelrn
  11. Alternative definition of the value of a function
    1. dfafv2
    2. afveq12d
    3. afveq1
    4. afveq2
    5. nfafv
    6. csbafv12g
    7. afvfundmfveq
    8. afvnfundmuv
    9. ndmafv
    10. afvvdm
    11. nfunsnafv
    12. afvvfunressn
    13. afvprc
    14. afvvv
    15. afvpcfv0
    16. afvnufveq
    17. afvvfveq
    18. afv0fv0
    19. afvfvn0fveq
    20. afv0nbfvbi
    21. afvfv0bi
    22. afveu
    23. fnbrafvb
    24. fnopafvb
    25. funbrafvb
    26. funopafvb
    27. funbrafv
    28. funbrafv2b
    29. dfafn5a
    30. dfafn5b
    31. fnrnafv
    32. afvelrnb
    33. afvelrnb0
    34. dfaimafn
    35. dfaimafn2
    36. afvelima
    37. afvelrn
    38. fnafvelrn
    39. fafvelrn
    40. ffnafv
    41. afvres
    42. tz6.12-afv
    43. tz6.12-1-afv
    44. dmfcoafv
    45. afvco2
    46. rlimdmafv
  12. Alternative definition of the value of an operation
    1. aoveq123d
    2. nfaov
    3. csbaovg
    4. aovfundmoveq
    5. aovnfundmuv
    6. ndmaov
    7. ndmaovg
    8. aovvdm
    9. nfunsnaov
    10. aovvfunressn
    11. aovprc
    12. aovrcl
    13. aovpcov0
    14. aovnuoveq
    15. aovvoveq
    16. aov0ov0
    17. aovovn0oveq
    18. aov0nbovbi
    19. aovov0bi
    20. rspceaov
    21. fnotaovb
    22. ffnaov
    23. faovcl
    24. aovmpt4g
    25. aoprssdm
    26. ndmaovcl
    27. ndmaovrcl
    28. ndmaovcom
    29. ndmaovass
    30. ndmaovdistr