Metamath Proof Explorer


Theorem fpr3

Description: Law of well-founded recursion over a partial order, part three. Finally, we show that F is unique. We do this by showing that any function H with the same properties we proved of F in fpr1 and fpr2 is identical to F . (Contributed by Scott Fenton, 11-Sep-2023)

Ref Expression
Hypothesis fprr.1 F = frecs R A G
Assertion fpr3 R Fr A R Po A R Se A H Fn A z A H z = z G H Pred R A z F = H

Proof

Step Hyp Ref Expression
1 fprr.1 F = frecs R A G
2 simpl R Fr A R Po A R Se A H Fn A z A H z = z G H Pred R A z R Fr A R Po A R Se A
3 1 fpr1 R Fr A R Po A R Se A F Fn A
4 1 fpr2 R Fr A R Po A R Se A z A F z = z G F Pred R A z
5 4 ralrimiva R Fr A R Po A R Se A z A F z = z G F Pred R A z
6 3 5 jca R Fr A R Po A R Se A F Fn A z A F z = z G F Pred R A z
7 6 adantr R Fr A R Po A R Se A H Fn A z A H z = z G H Pred R A z F Fn A z A F z = z G F Pred R A z
8 simpr R Fr A R Po A R Se A H Fn A z A H z = z G H Pred R A z H Fn A z A H z = z G H Pred R A z
9 fpr3g R Fr A R Po A R Se A F Fn A z A F z = z G F Pred R A z H Fn A z A H z = z G H Pred R A z F = H
10 2 7 8 9 syl3anc R Fr A R Po A R Se A H Fn A z A H z = z G H Pred R A z F = H