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

Definition df-wrecs 7027
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 7053, wfr2 7054, and wfr3 7055. (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 7026 . 2  class wrecs ( R ,  A ,  F
)
5 vf . . . . . . . 8  setvar  f
65cv 1436 . . . . . . 7  class  f
7 vx . . . . . . . 8  setvar  x
87cv 1436 . . . . . . 7  class  x
96, 8wfn 5587 . . . . . 6  wff  f  Fn  x
108, 1wss 3433 . . . . . . 7  wff  x  C_  A
11 vy . . . . . . . . . . 11  setvar  y
1211cv 1436 . . . . . . . . . 10  class  y
131, 2, 12cpred 5389 . . . . . . . . 9  class  Pred ( R ,  A , 
y )
1413, 8wss 3433 . . . . . . . 8  wff  Pred ( R ,  A , 
y )  C_  x
1514, 11, 8wral 2773 . . . . . . 7  wff  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x
1610, 15wa 370 . . . . . 6  wff  ( x 
C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)
1712, 6cfv 5592 . . . . . . . 8  class  ( f `
 y )
186, 13cres 4847 . . . . . . . . 9  class  ( f  |`  Pred ( R ,  A ,  y )
)
1918, 3cfv 5592 . . . . . . . 8  class  ( F `
 ( f  |`  Pred ( R ,  A ,  y ) ) )
2017, 19wceq 1437 . . . . . . 7  wff  ( f `
 y )  =  ( F `  (
f  |`  Pred ( R ,  A ,  y )
) )
2120, 11, 8wral 2773 . . . . . 6  wff  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  Pred ( R ,  A ,  y )
) )
229, 16, 21w3a 982 . . . . 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 1659 . . . 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 2405 . . 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 4213 . 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 1437 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  7028  nfwrecs  7029  wfrrel  7040  wfrdmss  7041  wfrdmcl  7043  wfrfun  7045  wfrlem12  7046  wfrlem16  7050  wfrlem17  7051  dfrecs3  7090
  Copyright terms: Public domain W3C validator