Definition df-opr 4697

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

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 4695	. 2 class (AFB)
5	1, 2	cop 2870	. . 3 class <.A, B>.
6	5, 3	cfv 3809	. 2 class (F` <.A, B>.)
7	4, 6	wceq 1136	1 wff (AFB) = (F` <.A, B>.)

This definition is referenced by:  opreq 4699  opreq1 4700  opreq2 4701  hbopr 4715  hboprd 4716  oprex 4718  oprprc1 4719  oprprc2 4720  csboprg 4721  fnotoprb 4727  ffnoprv 4754  eqfnoprv 4756  fnoprv 4757  oprabval 4763  oprabvalig 4764  oprabval6g 4773  oprvres 4774  foprrn 4776  fnrnoprv 4777  fooprv 4778  fnoprvrn 4779  oprvconst2 4781  oprvexOLDOLD 4785  oprssdm 4786  ndmoprg 4787  1st2val 4849  2nd2val 4850  elrnoprabg 4877  curry1 4886  curry2 4889  addpiord 5960  mulpiord 5961  cnmetdval 8975  remetdval 8981  oprcn 9050  bopcnlem2 9055  bopcnlem3 9056  grpsn 9135  gaid 9249  ssga 9250  gapmlem 9256  gapm 9257  ringsn 9285  imsdval 9444  vacnlem5 9466  vacnlem6 9467  ipfval 9486  oprabvaligg 9948  oprab2co 9954  subsp 10036  algrp1lem 13533  eucalgval2 13542  eucalgf 13543  eucalginv 13544  eucalg 13547  mulgcdlem2 13549  oprssoprvg 14063  fnoprvpop 14066  fnoprvrn2 14080  prj1 14125  cbcpcp 14230  idtrgrp 14692  invtrgrp 14693  trhom 14697  1ded 14767  1cat 14788  dualalg 14813  ishomb 14819  isfuna 14864  valtar 14942  isseg1 14986  oprabvalg 15388  opropabco 15394  f1opr 15396  txcnoprab 15593  cnresoprab 15597  cnoprab1 15603  cnoprab2 15604  heiborlem18 15654  heiborlem24 15660  heiborlem26 15662  heiborlem29 15665  heiborlem31 15667  heiborlem32 15668  heiborlem35 15671  heiborlem36 15672  heiborlem41 15677  phtpycom 15732  phtpycolem3 15735  phtpycolem4 15736  phtpycolem5 15737  reparphtlem2 15746  pcohtpylem3 15764  pi1bval 15770  pi1fval 15774

Copyright terms: Public domain