Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wrecs Structured version   Unicode version

Definition df-wrecs 27668
Description: Here we define the well-founded recursive function generator. This is similar to recs, but works with arbitrary well-founded relationships. (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 27667 . 2  class wrecs ( R ,  A ,  F
)
5 vf . . . . . . . 8  setvar  f
65cv 1368 . . . . . . 7  class  f
7 vx . . . . . . . 8  setvar  x
87cv 1368 . . . . . . 7  class  x
96, 8wfn 5408 . . . . . 6  wff  f  Fn  x
108, 1wss 3323 . . . . . . 7  wff  x  C_  A
11 vy . . . . . . . . . . 11  setvar  y
1211cv 1368 . . . . . . . . . 10  class  y
131, 2, 12cpred 27575 . . . . . . . . 9  class  Pred ( R ,  A , 
y )
1413, 8wss 3323 . . . . . . . 8  wff  Pred ( R ,  A , 
y )  C_  x
1514, 11, 8wral 2710 . . . . . . 7  wff  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x
1610, 15wa 369 . . . . . 6  wff  ( x 
C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)
1712, 6cfv 5413 . . . . . . . 8  class  ( f `
 y )
186, 13cres 4837 . . . . . . . . 9  class  ( f  |`  Pred ( R ,  A ,  y )
)
1918, 3cfv 5413 . . . . . . . 8  class  ( F `
 ( f  |`  Pred ( R ,  A ,  y ) ) )
2017, 19wceq 1369 . . . . . . 7  wff  ( f `
 y )  =  ( F `  (
f  |`  Pred ( R ,  A ,  y )
) )
2120, 11, 8wral 2710 . . . . . 6  wff  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  Pred ( R ,  A ,  y )
) )
229, 16, 21w3a 965 . . . . 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 1586 . . . 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 2424 . . 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 4086 . 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 1369 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  27669  nfwrecs  27670  wfrlem6  27680  wfrlem7  27681  wfrlem9  27683  wfrlem11  27685  wfrlem12  27686  wfrlem16  27690
  Copyright terms: Public domain W3C validator