This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tfr2ALT

Description: Alternate proof of tfr2 using well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis tfrALT.1 
|- F = recs ( G )
Assertion tfr2ALT 
|- ( A e. On -> ( F ` A ) = ( G ` ( F |` A ) ) )

Proof

Step Hyp Ref Expression
1 tfrALT.1 
 |-  F = recs ( G )
2 epweon 
 |-  _E We On
3 epse 
 |-  _E Se On
4 df-recs 
 |-  recs ( G ) = wrecs ( _E , On , G )
5 1 4 eqtri 
 |-  F = wrecs ( _E , On , G )
6 5 wfr2 
 |-  ( ( ( _E We On /\ _E Se On ) /\ A e. On ) -> ( F ` A ) = ( G ` ( F |` Pred ( _E , On , A ) ) ) )
7 2 3 6 mpanl12 
 |-  ( A e. On -> ( F ` A ) = ( G ` ( F |` Pred ( _E , On , A ) ) ) )
8 predon 
 |-  ( A e. On -> Pred ( _E , On , A ) = A )
9 8 reseq2d 
 |-  ( A e. On -> ( F |` Pred ( _E , On , A ) ) = ( F |` A ) )
10 9 fveq2d 
 |-  ( A e. On -> ( G ` ( F |` Pred ( _E , On , A ) ) ) = ( G ` ( F |` A ) ) )
11 7 10 eqtrd 
 |-  ( A e. On -> ( F ` A ) = ( G ` ( F |` A ) ) )