Metamath Proof Explorer


Theorem fprlem1

Description: Lemma for well-founded recursion with a partial order. Two acceptable functions are compatible. (Contributed by Scott Fenton, 11-Sep-2023)

Ref Expression
Hypotheses fprlem.1 B=f|xfFnxxAyxPredRAyxyxfy=yGfPredRAy
fprlem.2 F=frecsRAG
Assertion fprlem1 RFrARPoARSeAgBhBxguxhvu=v

Proof

Step Hyp Ref Expression
1 fprlem.1 B=f|xfFnxxAyxPredRAyxyxfy=yGfPredRAy
2 fprlem.2 F=frecsRAG
3 vex xV
4 vex uV
5 3 4 breldm xguxdomg
6 vex vV
7 3 6 breldm xhvxdomh
8 elin xdomgdomhxdomgxdomh
9 8 biimpri xdomgxdomhxdomgdomh
10 5 7 9 syl2an xguxhvxdomgdomh
11 id xguxhvxguxhv
12 4 brresi xgdomgdomhuxdomgdomhxgu
13 6 brresi xhdomgdomhvxdomgdomhxhv
14 12 13 anbi12i xgdomgdomhuxhdomgdomhvxdomgdomhxguxdomgdomhxhv
15 an4 xdomgdomhxguxdomgdomhxhvxdomgdomhxdomgdomhxguxhv
16 14 15 bitri xgdomgdomhuxhdomgdomhvxdomgdomhxdomgdomhxguxhv
17 10 10 11 16 syl21anbrc xguxhvxgdomgdomhuxhdomgdomhv
18 inss2 domgdomhdomh
19 1 frrlem3 hBdomhA
20 18 19 sstrid hBdomgdomhA
21 20 adantl gBhBdomgdomhA
22 21 adantl RFrARPoARSeAgBhBdomgdomhA
23 simpl1 RFrARPoARSeAgBhBRFrA
24 frss domgdomhARFrARFrdomgdomh
25 22 23 24 sylc RFrARPoARSeAgBhBRFrdomgdomh
26 simpl2 RFrARPoARSeAgBhBRPoA
27 poss domgdomhARPoARPodomgdomh
28 22 26 27 sylc RFrARPoARSeAgBhBRPodomgdomh
29 simpl3 RFrARPoARSeAgBhBRSeA
30 sess2 domgdomhARSeARSedomgdomh
31 22 29 30 sylc RFrARPoARSeAgBhBRSedomgdomh
32 1 frrlem4 gBhBgdomgdomhFndomgdomhadomgdomhgdomgdomha=aGgdomgdomhPredRdomgdomha
33 32 adantl RFrARPoARSeAgBhBgdomgdomhFndomgdomhadomgdomhgdomgdomha=aGgdomgdomhPredRdomgdomha
34 1 frrlem4 hBgBhdomhdomgFndomhdomgadomhdomghdomhdomga=aGhdomhdomgPredRdomhdomga
35 incom domgdomh=domhdomg
36 35 reseq2i hdomgdomh=hdomhdomg
37 fneq12 hdomgdomh=hdomhdomgdomgdomh=domhdomghdomgdomhFndomgdomhhdomhdomgFndomhdomg
38 36 35 37 mp2an hdomgdomhFndomgdomhhdomhdomgFndomhdomg
39 36 fveq1i hdomgdomha=hdomhdomga
40 predeq2 domgdomh=domhdomgPredRdomgdomha=PredRdomhdomga
41 35 40 ax-mp PredRdomgdomha=PredRdomhdomga
42 36 41 reseq12i hdomgdomhPredRdomgdomha=hdomhdomgPredRdomhdomga
43 42 oveq2i aGhdomgdomhPredRdomgdomha=aGhdomhdomgPredRdomhdomga
44 39 43 eqeq12i hdomgdomha=aGhdomgdomhPredRdomgdomhahdomhdomga=aGhdomhdomgPredRdomhdomga
45 35 44 raleqbii adomgdomhhdomgdomha=aGhdomgdomhPredRdomgdomhaadomhdomghdomhdomga=aGhdomhdomgPredRdomhdomga
46 38 45 anbi12i hdomgdomhFndomgdomhadomgdomhhdomgdomha=aGhdomgdomhPredRdomgdomhahdomhdomgFndomhdomgadomhdomghdomhdomga=aGhdomhdomgPredRdomhdomga
47 34 46 sylibr hBgBhdomgdomhFndomgdomhadomgdomhhdomgdomha=aGhdomgdomhPredRdomgdomha
48 47 ancoms gBhBhdomgdomhFndomgdomhadomgdomhhdomgdomha=aGhdomgdomhPredRdomgdomha
49 48 adantl RFrARPoARSeAgBhBhdomgdomhFndomgdomhadomgdomhhdomgdomha=aGhdomgdomhPredRdomgdomha
50 fpr3g RFrdomgdomhRPodomgdomhRSedomgdomhgdomgdomhFndomgdomhadomgdomhgdomgdomha=aGgdomgdomhPredRdomgdomhahdomgdomhFndomgdomhadomgdomhhdomgdomha=aGhdomgdomhPredRdomgdomhagdomgdomh=hdomgdomh
51 25 28 31 33 49 50 syl311anc RFrARPoARSeAgBhBgdomgdomh=hdomgdomh
52 51 breqd RFrARPoARSeAgBhBxgdomgdomhvxhdomgdomhv
53 52 biimprd RFrARPoARSeAgBhBxhdomgdomhvxgdomgdomhv
54 1 frrlem2 gBFung
55 54 ad2antrl RFrARPoARSeAgBhBFung
56 funres FungFungdomgdomh
57 dffun2 FungdomgdomhRelgdomgdomhxuvxgdomgdomhuxgdomgdomhvu=v
58 2sp uvxgdomgdomhuxgdomgdomhvu=vxgdomgdomhuxgdomgdomhvu=v
59 58 sps xuvxgdomgdomhuxgdomgdomhvu=vxgdomgdomhuxgdomgdomhvu=v
60 57 59 simplbiim Fungdomgdomhxgdomgdomhuxgdomgdomhvu=v
61 55 56 60 3syl RFrARPoARSeAgBhBxgdomgdomhuxgdomgdomhvu=v
62 53 61 sylan2d RFrARPoARSeAgBhBxgdomgdomhuxhdomgdomhvu=v
63 17 62 syl5 RFrARPoARSeAgBhBxguxhvu=v