Definition df-opr 4023

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 6068). 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 4042 and oprprc2 4043. On the other hand, we often find uses for this definition when F is a proper class, such as +_o in oav 4208. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 4024.

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 4021	. 2 class (AFB)
5	1, 2	cop 2463	. . 3 class ⟨A, B⟩
6	5, 3	cfv 3239	. 2 class (F ‘⟨A, B⟩)
7	4, 6	wceq 997	1 wff (AFB) = (F ‘⟨A, B⟩)

This definition is referenced by:  opreq 4025  opreq1 4026  opreq2 4027  hbopr 4039  oprex 4041  oprprc1 4042  oprprc2 4043  ffnoprval 4072  eqfnoprval 4074  fnoprval 4075  oprabval 4081  oprabvalig 4082  oprabval6g 4090  oprvalres 4091  foprrn 4093  fnrnoprval 4094  fooprval 4095  fnoprvalrn 4096  oprvalconst2 4098  oprvalex 4099  oprssdm 4100  ndmoprg 4101  1st2val 4153  2nd2val 4154  curry1 4156  elrnoprabg 4182  addpiord 5077  mulpiord 5078  cnmetdval 7987  remetdval 7993  oprcn 8062  bopcnlem2 8067  bopcnlem3 8068  grpsn 8208  ringsn 8247  imsdval 8401  ipfval 8436  oprabvaligg 10526  fnoprvalrn2 10551  subsp 10648  1ded 10753  1cat 10774  ishomb 10798  isfuna 10838

Copyright terms: Public domain