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

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