Definition df-opr 3965

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

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 3963	. 2 class (AFB)
5	1, 2	cop 2411	. . 3 class <.A, B>.
6	5, 3	cfv 3182	. 2 class (F` <.A, B>.)
7	4, 6	wceq 956	1 wff (AFB) = (F` <.A, B>.)

This definition is referenced by:  opreq 3967  opreq1 3968  opreq2 3969  hbopr 3981  oprex 3983  oprprc1 3984  oprprc2 3985  ffnoprval 4014  eqfnoprval 4016  fnoprval 4017  oprabval 4023  oprabvalig 4024  oprabval6g 4032  oprvalres 4033  foprrn 4035  fnrnoprval 4036  fooprval 4037  fnoprvalrn 4038  oprvalconst2 4040  oprvalex 4041  oprssdm 4042  ndmoprg 4043  1st2val 4095  2nd2val 4096  curry1 4098  elrnoprabg 4124  addpiord 5012  mulpiord 5013  cnmetdval 7902  remetdval 7908  oprcn 7977  bopcnlem2 7982  bopcnlem3 7983  grpsn 8124  ringsn 8163  imsdval 8317  ipfval 8352  oprabvaligg 10440  fnoprvalrn2 10470  subsp 10554  1ded 10671  1cat 10692  ishomb 10716  isfuna 10754

Copyright terms: Public domain