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 = frecs R A G
Assertion fpr1 R Fr A R Po A R Se A F Fn A

Proof

Step Hyp Ref Expression
1 fprr.1 F = frecs R A G
2 eqid 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 = 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
3 2 frrlem1 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 = a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c
4 3 1 fprlem1 R Fr A R Po A R Se A g 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 h 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 b g u b h v u = v
5 3 1 4 frrlem9 R Fr A R Po A R Se A Fun F
6 eqid F Pred R A z z z G F Pred R A z = F Pred R A z z z G F Pred R A z
7 simp1 R Fr A R Po A R Se A R Fr A
8 ssidd R Fr A R Po A R Se A z A Pred R A z Pred R A z
9 fprlem2 R Fr A R Po A R Se A z A y Pred R A z Pred R A y Pred R A z
10 setlikespec z A R Se A Pred R A z V
11 10 ancoms R Se A z A Pred R A z V
12 11 3ad2antl3 R Fr A R Po A R Se A z A Pred R A z V
13 predss Pred R A z A
14 13 a1i R Fr A R Po A R Se A z A Pred R A z A
15 difssd R Fr A R Po A R Se A A dom F A dom F A
16 simpr R Fr A R Po A R Se A A dom F A dom F
17 15 16 jca R Fr A R Po A R Se A A dom F A dom F A A dom F
18 frpomin2 R Fr A R Po A R Se A A dom F A A dom F z A dom F Pred R A dom F z =
19 17 18 syldan R Fr A R Po A R Se A A dom F z A dom F Pred R A dom F z =
20 3 1 4 6 7 8 9 12 14 19 frrlem14 R Fr A R Po A R Se A dom F = A
21 df-fn F Fn A Fun F dom F = A
22 5 20 21 sylanbrc R Fr A R Po A R Se A F Fn A