Definition df-opr 3971

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 F and its arguments A and B - will be useful for proving meaningful theorems. For example, if class F is the operation + and arguments A and B are 3 and 2, the expression (3 + 2) can be proved to equal 5 (see 3p2e5 6009). This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets); see oprprc1 3990 and oprprc2 3991. On the other hand, we often find uses for this definition when F is a proper class, such as +o in oav 4156. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 3972.

Assertion

Ref	Expression
df-opr	|- (AFB) = (F` <.A, B>.)

Detailed syntax breakdown of Definition df-opr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	co 3969	. 2 class (AFB)
5	1, 2	cop 2415	. . 3 class <.A, B>.
6	5, 3	cfv 3188	. 2 class (F` <.A, B>.)
7	4, 6	wceq 958	1 wff (AFB) = (F` <.A, B>.)

This definition is referenced by:  opreq 3973  opreq1 3974  opreq2 3975  hbopr 3987  oprex 3989  oprprc1 3990  oprprc2 3991  ffnoprval 4020  eqfnoprval 4022  fnoprval 4023  oprabval 4029  oprabvalig 4030  oprabval6g 4038  oprvalres 4039  foprrn 4041  fnrnoprval 4042  fooprval 4043  fnoprvalrn 4044  oprvalconst2 4046  oprvalex 4047  oprssdm 4048  ndmoprg 4049  1st2val 4101  2nd2val 4102  curry1 4104  elrnoprabg 4130  addpiord 5024  mulpiord 5025  cnmetdval 7899  remetdval 7905  oprcn 7974  bopcnlem2 7979  bopcnlem3 7980  grpsn 8120  ringsn 8159  imsdval 8313  ipfval 8348  oprabvaligg 10435  fnoprvalrn2 10460  subsp 10540  1ded 10642  1cat 10663  ishomb 10687  isfuna 10725

Copyright terms: Public domain