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 | |
|
fprlem.2 | |
||
Assertion | fprlem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fprlem.1 | |
|
2 | fprlem.2 | |
|
3 | vex | |
|
4 | vex | |
|
5 | 3 4 | breldm | |
6 | vex | |
|
7 | 3 6 | breldm | |
8 | elin | |
|
9 | 8 | biimpri | |
10 | 5 7 9 | syl2an | |
11 | id | |
|
12 | 4 | brresi | |
13 | 6 | brresi | |
14 | 12 13 | anbi12i | |
15 | an4 | |
|
16 | 14 15 | bitri | |
17 | 10 10 11 16 | syl21anbrc | |
18 | inss2 | |
|
19 | 1 | frrlem3 | |
20 | 18 19 | sstrid | |
21 | 20 | adantl | |
22 | 21 | adantl | |
23 | simpl1 | |
|
24 | frss | |
|
25 | 22 23 24 | sylc | |
26 | simpl2 | |
|
27 | poss | |
|
28 | 22 26 27 | sylc | |
29 | simpl3 | |
|
30 | sess2 | |
|
31 | 22 29 30 | sylc | |
32 | 1 | frrlem4 | |
33 | 32 | adantl | |
34 | 1 | frrlem4 | |
35 | incom | |
|
36 | 35 | reseq2i | |
37 | fneq12 | |
|
38 | 36 35 37 | mp2an | |
39 | 36 | fveq1i | |
40 | predeq2 | |
|
41 | 35 40 | ax-mp | |
42 | 36 41 | reseq12i | |
43 | 42 | oveq2i | |
44 | 39 43 | eqeq12i | |
45 | 35 44 | raleqbii | |
46 | 38 45 | anbi12i | |
47 | 34 46 | sylibr | |
48 | 47 | ancoms | |
49 | 48 | adantl | |
50 | fpr3g | |
|
51 | 25 28 31 33 49 50 | syl311anc | |
52 | 51 | breqd | |
53 | 52 | biimprd | |
54 | 1 | frrlem2 | |
55 | 54 | ad2antrl | |
56 | funres | |
|
57 | dffun2 | |
|
58 | 2sp | |
|
59 | 58 | sps | |
60 | 57 59 | simplbiim | |
61 | 55 56 60 | 3syl | |
62 | 53 61 | sylan2d | |
63 | 17 62 | syl5 | |