Metamath Proof Explorer


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 7 8 10 wfr3
 |-  ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` Pred ( _E , On , x ) ) ) ) -> F = B )
12 6 11 sylan2br
 |-  ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> F = B )
13 12 eqcomd
 |-  ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> B = F )