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 7028
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 7054, wfr2 7055, and wfr3 7056. (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 7027 . 2  class wrecs ( R ,  A ,  F
)
5 vf . . . . . . . 8  setvar  f
65cv 1443 . . . . . . 7  class  f
7 vx . . . . . . . 8  setvar  x
87cv 1443 . . . . . . 7  class  x
96, 8wfn 5577 . . . . . 6  wff  f  Fn  x
108, 1wss 3404 . . . . . . 7  wff  x  C_  A
11 vy . . . . . . . . . . 11  setvar  y
1211cv 1443 . . . . . . . . . 10  class  y
131, 2, 12cpred 5379 . . . . . . . . 9  class  Pred ( R ,  A , 
y )
1413, 8wss 3404 . . . . . . . 8  wff  Pred ( R ,  A , 
y )  C_  x
1514, 11, 8wral 2737 . . . . . . 7  wff  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x
1610, 15wa 371 . . . . . 6  wff  ( x 
C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)
1712, 6cfv 5582 . . . . . . . 8  class  ( f `
 y )
186, 13cres 4836 . . . . . . . . 9  class  ( f  |`  Pred ( R ,  A ,  y )
)
1918, 3cfv 5582 . . . . . . . 8  class  ( F `
 ( f  |`  Pred ( R ,  A ,  y ) ) )
2017, 19wceq 1444 . . . . . . 7  wff  ( f `
 y )  =  ( F `  (
f  |`  Pred ( R ,  A ,  y )
) )
2120, 11, 8wral 2737 . . . . . 6  wff  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  Pred ( R ,  A ,  y )
) )
229, 16, 21w3a 985 . . . . 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 1663 . . . 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 2437 . . 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 4198 . 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 1444 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  7029  nfwrecs  7030  wfrrel  7041  wfrdmss  7042  wfrdmcl  7044  wfrfun  7046  wfrlem12  7047  wfrlem16  7051  wfrlem17  7052  dfrecs3  7091  csbwrecsg  31728
  Copyright terms: Public domain W3C validator