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 5995). 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 5004  mulpiord 5005  cnmetdval 7887  remetdval 7893  oprcn 7962  bopcnlem2 7967  bopcnlem3 7968  grpsn 8109  ringsn 8148  imsdval 8302  ipfval 8337  oprabvaligg 10424  fnoprvalrn2 10449  subsp 10514  1ded 10614  1cat 10635  ishomb 10659  isfuna 10691

Copyright terms: Public domain