Metamath Proof Explorer


Theorem wfr2

Description: The Principle of Well-Ordered Recursion, part 2 of 3. Next, we show that the value of F at any X e. A is G recursively applied to all "previous" values of F . (Contributed by Scott Fenton, 18-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses wfr2.1 R We A
wfr2.2 R Se A
wfr2.3 F = wrecs R A G
Assertion wfr2 X A F X = G F Pred R A X

Proof

Step Hyp Ref Expression
1 wfr2.1 R We A
2 wfr2.2 R Se A
3 wfr2.3 F = wrecs R A G
4 eqid F x G F Pred R A x = F x G F Pred R A x
5 1 2 3 4 wfrlem16 dom F = A
6 5 eleq2i X dom F X A
7 1 2 3 wfr2a X dom F F X = G F Pred R A X
8 6 7 sylbir X A F X = G F Pred R A X