| Description: Define the value of an
operation. Definition of operation value in
[Enderton] p. 79. Note that the syntax
is simply three class expressions
in a row bracketed by parentheses. There are 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. For example, if
class 𝐹 is the operation + and arguments 𝐴 and 𝐵 are 3
and 2, the expression (3 +
2) can be proved to equal 5 (see
3p2e5 12409). This definition is well-defined, although
not very meaningful,
when classes 𝐴 and/or 𝐵 are proper classes (i.e.
are not sets);
see ovprc1 7462 and ovprc2 7463. On the other hand, we often find uses for
this definition when 𝐹 is a proper class, such as +o in oav 8505.
𝐹 is normally equal to a class of
nested ordered pairs of the form
defined by df-oprab 7427. (Contributed by NM,
28-Feb-1995.) |
