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