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 | x f Fn x x A y x Pred R A y x y x f y = y G f Pred R A y
fprlem.2 F = frecs R A G
Assertion fprlem1 R Fr A R Po A R Se A g B h B x g u x h v u = v

Proof

Step Hyp Ref Expression
1 fprlem.1 B = f | x f Fn x x A y x Pred R A y x y x f y = y G f Pred R A y
2 fprlem.2 F = frecs R A G
3 vex x V
4 vex u V
5 3 4 breldm x g u x dom g
6 vex v V
7 3 6 breldm x h v x dom h
8 elin x dom g dom h x dom g x dom h
9 8 biimpri x dom g x dom h x dom g dom h
10 5 7 9 syl2an x g u x h v x dom g dom h
11 id x g u x h v x g u x h v
12 4 brresi x g dom g dom h u x dom g dom h x g u
13 6 brresi x h dom g dom h v x dom g dom h x h v
14 12 13 anbi12i x g dom g dom h u x h dom g dom h v x dom g dom h x g u x dom g dom h x h v
15 an4 x dom g dom h x g u x dom g dom h x h v x dom g dom h x dom g dom h x g u x h v
16 14 15 bitri x g dom g dom h u x h dom g dom h v x dom g dom h x dom g dom h x g u x h v
17 10 10 11 16 syl21anbrc x g u x h v x g dom g dom h u x h dom g dom h v
18 inss2 dom g dom h dom h
19 1 frrlem3 h B dom h A
20 18 19 sstrid h B dom g dom h A
21 20 adantl g B h B dom g dom h A
22 21 adantl R Fr A R Po A R Se A g B h B dom g dom h A
23 simpl1 R Fr A R Po A R Se A g B h B R Fr A
24 frss dom g dom h A R Fr A R Fr dom g dom h
25 22 23 24 sylc R Fr A R Po A R Se A g B h B R Fr dom g dom h
26 simpl2 R Fr A R Po A R Se A g B h B R Po A
27 poss dom g dom h A R Po A R Po dom g dom h
28 22 26 27 sylc R Fr A R Po A R Se A g B h B R Po dom g dom h
29 simpl3 R Fr A R Po A R Se A g B h B R Se A
30 sess2 dom g dom h A R Se A R Se dom g dom h
31 22 29 30 sylc R Fr A R Po A R Se A g B h B R Se dom g dom h
32 1 frrlem4 g B h B g dom g dom h Fn dom g dom h a dom g dom h g dom g dom h a = a G g dom g dom h Pred R dom g dom h a
33 32 adantl R Fr A R Po A R Se A g B h B g dom g dom h Fn dom g dom h a dom g dom h g dom g dom h a = a G g dom g dom h Pred R dom g dom h a
34 1 frrlem4 h B g B h dom h dom g Fn dom h dom g a dom h dom g h dom h dom g a = a G h dom h dom g Pred R dom h dom g a
35 incom dom g dom h = dom h dom g
36 35 reseq2i h dom g dom h = h dom h dom g
37 fneq12 h dom g dom h = h dom h dom g dom g dom h = dom h dom g h dom g dom h Fn dom g dom h h dom h dom g Fn dom h dom g
38 36 35 37 mp2an h dom g dom h Fn dom g dom h h dom h dom g Fn dom h dom g
39 36 fveq1i h dom g dom h a = h dom h dom g a
40 predeq2 dom g dom h = dom h dom g Pred R dom g dom h a = Pred R dom h dom g a
41 35 40 ax-mp Pred R dom g dom h a = Pred R dom h dom g a
42 36 41 reseq12i h dom g dom h Pred R dom g dom h a = h dom h dom g Pred R dom h dom g a
43 42 oveq2i a G h dom g dom h Pred R dom g dom h a = a G h dom h dom g Pred R dom h dom g a
44 39 43 eqeq12i h dom g dom h a = a G h dom g dom h Pred R dom g dom h a h dom h dom g a = a G h dom h dom g Pred R dom h dom g a
45 35 44 raleqbii a dom g dom h h dom g dom h a = a G h dom g dom h Pred R dom g dom h a a dom h dom g h dom h dom g a = a G h dom h dom g Pred R dom h dom g a
46 38 45 anbi12i h dom g dom h Fn dom g dom h a dom g dom h h dom g dom h a = a G h dom g dom h Pred R dom g dom h a h dom h dom g Fn dom h dom g a dom h dom g h dom h dom g a = a G h dom h dom g Pred R dom h dom g a
47 34 46 sylibr h B g B h dom g dom h Fn dom g dom h a dom g dom h h dom g dom h a = a G h dom g dom h Pred R dom g dom h a
48 47 ancoms g B h B h dom g dom h Fn dom g dom h a dom g dom h h dom g dom h a = a G h dom g dom h Pred R dom g dom h a
49 48 adantl R Fr A R Po A R Se A g B h B h dom g dom h Fn dom g dom h a dom g dom h h dom g dom h a = a G h dom g dom h Pred R dom g dom h a
50 fpr3g R Fr dom g dom h R Po dom g dom h R Se dom g dom h g dom g dom h Fn dom g dom h a dom g dom h g dom g dom h a = a G g dom g dom h Pred R dom g dom h a h dom g dom h Fn dom g dom h a dom g dom h h dom g dom h a = a G h dom g dom h Pred R dom g dom h a g dom g dom h = h dom g dom h
51 25 28 31 33 49 50 syl311anc R Fr A R Po A R Se A g B h B g dom g dom h = h dom g dom h
52 51 breqd R Fr A R Po A R Se A g B h B x g dom g dom h v x h dom g dom h v
53 52 biimprd R Fr A R Po A R Se A g B h B x h dom g dom h v x g dom g dom h v
54 1 frrlem2 g B Fun g
55 54 ad2antrl R Fr A R Po A R Se A g B h B Fun g
56 funres Fun g Fun g dom g dom h
57 dffun2 Fun g dom g dom h Rel g dom g dom h x u v x g dom g dom h u x g dom g dom h v u = v
58 2sp u v x g dom g dom h u x g dom g dom h v u = v x g dom g dom h u x g dom g dom h v u = v
59 58 sps x u v x g dom g dom h u x g dom g dom h v u = v x g dom g dom h u x g dom g dom h v u = v
60 57 59 simplbiim Fun g dom g dom h x g dom g dom h u x g dom g dom h v u = v
61 55 56 60 3syl R Fr A R Po A R Se A g B h B x g dom g dom h u x g dom g dom h v u = v
62 53 61 sylan2d R Fr A R Po A R Se A g B h B x g dom g dom h u x h dom g dom h v u = v
63 17 62 syl5 R Fr A R Po A R Se A g B h B x g u x h v u = v