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 applied to all "previous" values of F . (Contributed by Scott Fenton, 18-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 wfr2.1 F = wrecs R A G
2 1 wfr1 R We A R Se A F Fn A
3 2 fndmd R We A R Se A dom F = A
4 3 eleq2d R We A R Se A X dom F X A
5 4 biimpar R We A R Se A X A X dom F
6 1 wfr2a R We A R Se A X dom F F X = G F Pred R A X
7 5 6 syldan R We A R Se A X A F X = G F Pred R A X