Metamath Proof Explorer


Definition df-frecs

Description: This is the definition for the well-founded recursion generator. Similar to df-wrecs and df-recs , it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a well-founded set-like relationship for its properties, not a well-ordered relationship. This proof requires either a partial order or the axiom of infinity. We develop the theorems twice, once with a partial order and once without. The second development occurs later in the database, after ax-inf has been introduced. (Contributed by Scott Fenton, 23-Dec-2021)

Ref Expression
Assertion df-frecs frecsRAF=f|xfFnxxAyxPredRAyxyxfy=yFfPredRAy

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR classR
1 cA classA
2 cF classF
3 1 0 2 cfrecs classfrecsRAF
4 vf setvarf
5 vx setvarx
6 4 cv setvarf
7 5 cv setvarx
8 6 7 wfn wfffFnx
9 7 1 wss wffxA
10 vy setvary
11 10 cv setvary
12 1 0 11 cpred classPredRAy
13 12 7 wss wffPredRAyx
14 13 10 7 wral wffyxPredRAyx
15 9 14 wa wffxAyxPredRAyx
16 11 6 cfv classfy
17 6 12 cres classfPredRAy
18 11 17 2 co classyFfPredRAy
19 16 18 wceq wfffy=yFfPredRAy
20 19 10 7 wral wffyxfy=yFfPredRAy
21 8 15 20 w3a wfffFnxxAyxPredRAyxyxfy=yFfPredRAy
22 21 5 wex wffxfFnxxAyxPredRAyxyxfy=yFfPredRAy
23 22 4 cab classf|xfFnxxAyxPredRAyxyxfy=yFfPredRAy
24 23 cuni classf|xfFnxxAyxPredRAyxyxfy=yFfPredRAy
25 3 24 wceq wfffrecsRAF=f|xfFnxxAyxPredRAyxyxfy=yFfPredRAy