Definition df-frec 6311

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 6310	. 2 class FRec (F, I)
4		c0c 4375	. . . . 5 class 0c
5	4, 2	cop 4562	. . . 4 class <.0c, I>.
6	5	csn 3738	. . 3 class {<.0c, I>.}
7		vx	. . . . 5 setvar x
8		cvv 2860	. . . . 5 class _V
9	7	cv 1641	. . . . . 6 class x
10		c1c 4135	. . . . . 6 class 1c
11	9, 10	cplc 4376	. . . . 5 class (x +o 1c)
12	7, 8, 11	cmpt 5652	. . . 4 class (x e. _V |-> (x +o 1c))
13	12, 1	cpprod 5738	. . 3 class PProd ((x e. _V |-> (x +o 1c)), F)
14	6, 13	cclos1 5873	. 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  6312  frecexg  6313  frecxp  6315  dmfrec  6317  fnfreclem2  6319  fnfreclem3  6320  frec0  6322  frecsuc  6323