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 e. _V |-> (x +o 1c)), F))

Distinct variable groups:   x,F   x,I

Detailed syntax breakdown of Definition df-frec

Step	Hyp	Ref	Expression
1		cF	. . 3 class F
2		cI	. . 3 class I
3	1, 2	cfrec 6309	. 2 class FRec (F, I)
4		c0c 4374	. . . . 5 class 0c
5	4, 2	cop 4561	. . . 4 class <.0c, I>.
6	5	csn 3737	. . 3 class {<.0c, I>.}
7		vx	. . . . 5 setvar x
8		cvv 2859	. . . . 5 class _V
9	7	cv 1641	. . . . . 6 class x
10		c1c 4134	. . . . . 6 class 1c
11	9, 10	cplc 4375	. . . . 5 class (x +o 1c)
12	7, 8, 11	cmpt 5651	. . . 4 class (x e. _V |-> (x +o 1c))
13	12, 1	cpprod 5737	. . 3 class PProd ((x e. _V |-> (x +o 1c)), F)
14	6, 13	cclos1 5872	. 2 class Clos1 ({<.0c, I>.}, PProd ((x e. _V |-> (x +o 1c)), F))
15	3, 14	wceq 1642	1 wff FRec (F, I) = Clos1 ({<.0c, I>.}, PProd ((x e. _V |-> (x +o 1c)), F))

This definition is referenced by:  freceq12  6311  frecexg  6312  frecxp  6314  dmfrec  6316  fnfreclem2  6318  fnfreclem3  6319  frec0  6321  frecsuc  6322