Metamath Proof Explorer


Theorem wfr3

Description: The principle of Well-Ordered Recursion, part 3 of 3. 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 wfr1 and wfr2 is identical to F . (Contributed by Scott Fenton, 18-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses wfr3.1
|- R We A
wfr3.2
|- R Se A
wfr3.3
|- F = wrecs ( R , A , G )
Assertion wfr3
|- ( ( H Fn A /\ A. z e. A ( H ` z ) = ( G ` ( H |` Pred ( R , A , z ) ) ) ) -> F = H )

Proof

Step Hyp Ref Expression
1 wfr3.1
 |-  R We A
2 wfr3.2
 |-  R Se A
3 wfr3.3
 |-  F = wrecs ( R , A , G )
4 1 2 pm3.2i
 |-  ( R We A /\ R Se A )
5 1 2 3 wfr1
 |-  F Fn A
6 1 2 3 wfr2
 |-  ( z e. A -> ( F ` z ) = ( G ` ( F |` Pred ( R , A , z ) ) ) )
7 6 rgen
 |-  A. z e. A ( F ` z ) = ( G ` ( F |` Pred ( R , A , z ) ) )
8 5 7 pm3.2i
 |-  ( F Fn A /\ A. z e. A ( F ` z ) = ( G ` ( F |` Pred ( R , A , z ) ) ) )
9 wfr3g
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Fn A /\ A. z e. A ( F ` z ) = ( G ` ( F |` Pred ( R , A , z ) ) ) ) /\ ( H Fn A /\ A. z e. A ( H ` z ) = ( G ` ( H |` Pred ( R , A , z ) ) ) ) ) -> F = H )
10 4 8 9 mp3an12
 |-  ( ( H Fn A /\ A. z e. A ( H ` z ) = ( G ` ( H |` Pred ( R , A , z ) ) ) ) -> F = H )