Theorem tfr3ALT

Description: Alternate proof of tfr3 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	tfr3ALT	|- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> B = F )

Proof

Step	Hyp	Ref	Expression
1		tfrALT.1	|- F = recs ( G )
2		predon	|- ( x e. On -> Pred ( _E , On , x ) = x )
3	2	reseq2d	|- ( x e. On -> ( B |` Pred ( _E , On , x ) ) = ( B |` x ) )
4	3	fveq2d	|- ( x e. On -> ( G ` ( B |` Pred ( _E , On , x ) ) ) = ( G ` ( B |` x ) ) )
5	4	eqeq2d	|- ( x e. On -> ( ( B ` x ) = ( G ` ( B |` Pred ( _E , On , x ) ) ) <-> ( B ` x ) = ( G ` ( B |` x ) ) ) )
6	5	ralbiia	|- ( A. x e. On ( B ` x ) = ( G ` ( B |` Pred ( _E , On , x ) ) ) <-> A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) )
7		epweon	|- _E We On
8		epse	|- _E Se On
9		df-recs	|- recs ( G ) = wrecs ( _E , On , G )
10	1 9	eqtri	|- F = wrecs ( _E , On , G )
11	10	wfr3	|- ( ( ( _E We On /\ _E Se On ) /\ ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` Pred ( _E , On , x ) ) ) ) ) -> F = B )
12	7 8 11	mpanl12	|- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` Pred ( _E , On , x ) ) ) ) -> F = B )
13	6 12	sylan2br	|- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> F = B )
14	13	eqcomd	|- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> B = F )