New Foundations Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-frec		Unicode 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 Clos1 0c PProd 1c

Distinct variable groups:   ,   ,

---

Detailed syntax breakdown of Definition df-frec

Step	Hyp	Ref	Expression
1		cF	. . 3
2		cI	. . 3
3	1, 2	cfrec 6309	. 2 FRec
4		c0c 4374	. . . . 5 0c
5	4, 2	cop 4561	. . . 4 0c
6	5	csn 3737	. . 3 0c
7		vx	. . . . 5
8		cvv 2859	. . . . 5
9	7	cv 1641	. . . . . 6
10		c1c 4134	. . . . . 6 1c
11	9, 10	cplc 4375	. . . . 5 1c
12	7, 8, 11	cmpt 5651	. . . 4 1c
13	12, 1	cpprod 5737	. . 3 PProd 1c
14	6, 13	cclos1 5872	. 2 Clos1 0c PProd 1c
15	3, 14	wceq 1642	1 FRec Clos1 0c PProd 1c

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