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 ) ) )