Definition df-opr 3904

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 5905). 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 3923 and oprprc2 3924. On the other hand, we often find uses for this definition when F is a proper class, such as +o in oav 4088. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 3905.

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 3902	. 2 class (AFB)
5	1, 2	cop 2382	. . 3 class <.A, B>.
6	5, 3	cfv 3145	. 2 class (F` <.A, B>.)
7	4, 6	wceq 1099	1 wff (AFB) = (F` <.A, B>.)

This definition is referenced by:  opreq 3906  opreq1 3907  opreq2 3908  hbopr 3920  oprex 3922  oprprc1 3923  oprprc2 3924  ffnoprval 3953  eqfnoprval 3955  fnoprval 3956  oprabval 3962  oprabvalig 3963  oprabval6g 3971  oprvalres 3972  foprrn 3974  fnrnoprval 3975  fooprval 3976  fnoprvalrn 3977  oprvalconst2 3979  oprvalex 3980  oprssdm 3981  ndmoprg 3982  ndmoprgOLD 3983  1st2val 4033  2nd2val 4034  curry1 4036  elrnoprabg 4062  addpiord 4935  mulpiord 4936  cnmetdval 7789  remetdval 7795  oprcn 7859  bopcnlem2 7864  bopcnlem3 7865  grpsn 8009  ringsn 8048  imsdval 8192  ipfval 8221  oprabvaligg 8700  fnoprvalrn2 8725  subsp 8779  1ded 8865  1cat 8886  ishomb 8910  isfuna 8940

Copyright terms: Public domain