Metamath Proof Explorer


Theorem fpr1

Description: Law of well-founded recursion over a partial order, part one. Establish the functionality and domain of the recursive function generator. Note that by requiring a partial order we can avoid using the axiom of infinity. (Contributed by Scott Fenton, 11-Sep-2023)

Ref Expression
Hypothesis fprr.1 F=frecsRAG
Assertion fpr1 RFrARPoARSeAFFnA

Proof

Step Hyp Ref Expression
1 fprr.1 F=frecsRAG
2 eqid f|xfFnxxAyxPredRAyxyxfy=yGfPredRAy=f|xfFnxxAyxPredRAyxyxfy=yGfPredRAy
3 2 frrlem1 f|xfFnxxAyxPredRAyxyxfy=yGfPredRAy=a|baFnbbAcbPredRAcbcbac=cGaPredRAc
4 3 1 fprlem1 RFrARPoARSeAgf|xfFnxxAyxPredRAyxyxfy=yGfPredRAyhf|xfFnxxAyxPredRAyxyxfy=yGfPredRAybgubhvu=v
5 3 1 4 frrlem9 RFrARPoARSeAFunF
6 eqid FPredRAzzzGFPredRAz=FPredRAzzzGFPredRAz
7 simp1 RFrARPoARSeARFrA
8 ssidd RFrARPoARSeAzAPredRAzPredRAz
9 fprlem2 RFrARPoARSeAzAyPredRAzPredRAyPredRAz
10 setlikespec zARSeAPredRAzV
11 10 ancoms RSeAzAPredRAzV
12 11 3ad2antl3 RFrARPoARSeAzAPredRAzV
13 predss PredRAzA
14 13 a1i RFrARPoARSeAzAPredRAzA
15 difssd RFrARPoARSeAAdomFAdomFA
16 simpr RFrARPoARSeAAdomFAdomF
17 15 16 jca RFrARPoARSeAAdomFAdomFAAdomF
18 frpomin2 RFrARPoARSeAAdomFAAdomFzAdomFPredRAdomFz=
19 17 18 syldan RFrARPoARSeAAdomFzAdomFPredRAdomFz=
20 3 1 4 6 7 8 9 12 14 19 frrlem14 RFrARPoARSeAdomF=A
21 df-fn FFnAFunFdomF=A
22 5 20 21 sylanbrc RFrARPoARSeAFFnA