New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-frec GIF version

Definition df-frec 6310
 Description: Define the finite recursive function generator. This is a function over Nn that obeys the standard recursion relationship. Definition adapted from theorem XI.3.24 of [Rosser] p. 412. (Contributed by Scott Fenton, 30-Jul-2019.)
Assertion
Ref Expression
df-frec FRec (F, I) = Clos1 ({0c, I}, PProd ((x V (x +c 1c)), F))
Distinct variable groups:   x,F   x,I

Detailed syntax breakdown of Definition df-frec
StepHypRef Expression
1 cF . . 3 class F
2 cI . . 3 class I
31, 2cfrec 6309 . 2 class FRec (F, I)
4 c0c 4374 . . . . 5 class 0c
54, 2cop 4561 . . . 4 class 0c, I
65csn 3737 . . 3 class {0c, I}
7 vx . . . . 5 setvar x
8 cvv 2859 . . . . 5 class V
97cv 1641 . . . . . 6 class x
10 c1c 4134 . . . . . 6 class 1c
119, 10cplc 4375 . . . . 5 class (x +c 1c)
127, 8, 11cmpt 5651 . . . 4 class (x V (x +c 1c))
1312, 1cpprod 5737 . . 3 class PProd ((x V (x +c 1c)), F)
146, 13cclos1 5872 . 2 class Clos1 ({0c, I}, PProd ((x V (x +c 1c)), F))
153, 14wceq 1642 1 wff FRec (F, I) = Clos1 ({0c, I}, PProd ((x V (x +c 1c)), F))
 Colors of variables: wff setvar class This definition is referenced by:  freceq12  6311  frecexg  6312  frecxp  6314  dmfrec  6316  fnfreclem2  6318  fnfreclem3  6319  frec0  6321  frecsuc  6322
 Copyright terms: Public domain W3C validator