MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-wrecs Structured version   Visualization version   Unicode version

Definition df-wrecs 7046
Description: Here we define the well-founded recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function  F, a relationship  R, and a base set  A, this definition generates a function  G  = wrecs ( R ,  A ,  F ) that has property that, at any point  x  e.  A,  ( G `  x )  =  ( F `  ( G  |  `  Pred ( R ,  A ,  x ) ) ). See wfr1 7072, wfr2 7073, and wfr3 7074. (Contributed by Scott Fenton, 7-Jun-2018.) (New usage is discouraged.)
Assertion
Ref Expression
df-wrecs  |- wrecs ( R ,  A ,  F
)  =  U. {
f  |  E. x
( f  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x )  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  Pred ( R ,  A , 
y ) ) ) ) }
Distinct variable groups:    R, f, x, y    A, f, x, y    f, F, x, y

Detailed syntax breakdown of Definition df-wrecs
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
3 cF . . 3  class  F
41, 2, 3cwrecs 7045 . 2  class wrecs ( R ,  A ,  F
)
5 vf . . . . . . . 8  setvar  f
65cv 1451 . . . . . . 7  class  f
7 vx . . . . . . . 8  setvar  x
87cv 1451 . . . . . . 7  class  x
96, 8wfn 5584 . . . . . 6  wff  f  Fn  x
108, 1wss 3390 . . . . . . 7  wff  x  C_  A
11 vy . . . . . . . . . . 11  setvar  y
1211cv 1451 . . . . . . . . . 10  class  y
131, 2, 12cpred 5386 . . . . . . . . 9  class  Pred ( R ,  A , 
y )
1413, 8wss 3390 . . . . . . . 8  wff  Pred ( R ,  A , 
y )  C_  x
1514, 11, 8wral 2756 . . . . . . 7  wff  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x
1610, 15wa 376 . . . . . 6  wff  ( x 
C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)
1712, 6cfv 5589 . . . . . . . 8  class  ( f `
 y )
186, 13cres 4841 . . . . . . . . 9  class  ( f  |`  Pred ( R ,  A ,  y )
)
1918, 3cfv 5589 . . . . . . . 8  class  ( F `
 ( f  |`  Pred ( R ,  A ,  y ) ) )
2017, 19wceq 1452 . . . . . . 7  wff  ( f `
 y )  =  ( F `  (
f  |`  Pred ( R ,  A ,  y )
) )
2120, 11, 8wral 2756 . . . . . 6  wff  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  Pred ( R ,  A ,  y )
) )
229, 16, 21w3a 1007 . . . . 5  wff  ( f  Fn  x  /\  (
x  C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  Pred ( R ,  A ,  y )
) ) )
2322, 7wex 1671 . . . 4  wff  E. x
( f  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x )  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  Pred ( R ,  A , 
y ) ) ) )
2423, 5cab 2457 . . 3  class  { f  |  E. x ( f  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) }
2524cuni 4190 . 2  class  U. {
f  |  E. x
( f  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x )  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  Pred ( R ,  A , 
y ) ) ) ) }
264, 25wceq 1452 1  wff wrecs ( R ,  A ,  F
)  =  U. {
f  |  E. x
( f  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x )  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  Pred ( R ,  A , 
y ) ) ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  wrecseq123  7047  nfwrecs  7048  wfrrel  7059  wfrdmss  7060  wfrdmcl  7062  wfrfun  7064  wfrlem12  7065  wfrlem16  7069  wfrlem17  7070  dfrecs3  7109  csbwrecsg  31798
  Copyright terms: Public domain W3C validator