Definition df-opr 3950

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

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 3948	. 2 class (AFB)
5	1, 2	cop 2401	. . 3 class <.A, B>.
6	5, 3	cfv 3172	. 2 class (F` <.A, B>.)
7	4, 6	wceq 953	1 wff (AFB) = (F` <.A, B>.)

This definition is referenced by:  opreq 3952  opreq1 3953  opreq2 3954  hbopr 3966  oprex 3968  oprprc1 3969  oprprc2 3970  ffnoprval 3999  eqfnoprval 4001  fnoprval 4002  oprabval 4008  oprabvalig 4009  oprabval6g 4017  oprvalres 4018  foprrn 4020  fnrnoprval 4021  fooprval 4022  fnoprvalrn 4023  oprvalconst2 4025  oprvalex 4026  oprssdm 4027  ndmoprg 4028  ndmoprgOLD 4029  1st2val 4079  2nd2val 4080  curry1 4082  elrnoprabg 4108  addpiord 4984  mulpiord 4985  cnmetdval 7841  remetdval 7847  oprcn 7911  bopcnlem2 7916  bopcnlem3 7917  grpsn 8061  ringsn 8100  imsdval 8255  ipfval 8286  oprabvaligg 10341  fnoprvalrn2 10366  subsp 10429  1ded 10515  1cat 10536  ishomb 10560  isfuna 10592

Copyright terms: Public domain