Metamath Proof Explorer


Theorem frrlem2

Description: Lemma for well-founded recursion. An acceptable function is a function. (Contributed by Paul Chapman, 21-Apr-2012)

Ref Expression
Hypothesis frrlem1.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
Assertion frrlem2 g B Fun g

Proof

Step Hyp Ref Expression
1 frrlem1.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 1 frrlem1 B = g | z g Fn z z A w z Pred R A w z w z g w = w G g Pred R A w
3 2 abeq2i g B z g Fn z z A w z Pred R A w z w z g w = w G g Pred R A w
4 fnfun g Fn z Fun g
5 4 3ad2ant1 g Fn z z A w z Pred R A w z w z g w = w G g Pred R A w Fun g
6 5 exlimiv z g Fn z z A w z Pred R A w z w z g w = w G g Pred R A w Fun g
7 3 6 sylbi g B Fun g