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 , a relationship , and a base set , this definition generates a function wrecs that has property that, at any point , . 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
Distinct variable groups:   ,,,   ,,,   ,,,

Detailed syntax breakdown of Definition df-wrecs
StepHypRef Expression
1 cA . . 3
2 cR . . 3
3 cF . . 3
41, 2, 3cwrecs 7027 . 2 wrecs
5 vf . . . . . . . 8
65cv 1443 . . . . . . 7
7 vx . . . . . . . 8
87cv 1443 . . . . . . 7
96, 8wfn 5577 . . . . . 6
108, 1wss 3404 . . . . . . 7
11 vy . . . . . . . . . . 11
1211cv 1443 . . . . . . . . . 10
131, 2, 12cpred 5379 . . . . . . . . 9
1413, 8wss 3404 . . . . . . . 8
1514, 11, 8wral 2737 . . . . . . 7
1610, 15wa 371 . . . . . 6
1712, 6cfv 5582 . . . . . . . 8
186, 13cres 4836 . . . . . . . . 9
1918, 3cfv 5582 . . . . . . . 8
2017, 19wceq 1444 . . . . . . 7
2120, 11, 8wral 2737 . . . . . 6
229, 16, 21w3a 985 . . . . 5
2322, 7wex 1663 . . . 4
2423, 5cab 2437 . . 3
2524cuni 4198 . 2
264, 25wceq 1444 1 wrecs
 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