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 𝐹 = recs ( 𝐺 )
Assertion tfr2ALT ( 𝐴 ∈ On → ( 𝐹𝐴 ) = ( 𝐺 ‘ ( 𝐹𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 tfrALT.1 𝐹 = recs ( 𝐺 )
2 epweon E We On
3 epse E Se On
4 df-recs recs ( 𝐺 ) = wrecs ( E , On , 𝐺 )
5 1 4 eqtri 𝐹 = wrecs ( E , On , 𝐺 )
6 2 3 5 wfr2 ( 𝐴 ∈ On → ( 𝐹𝐴 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( E , On , 𝐴 ) ) ) )
7 predon ( 𝐴 ∈ On → Pred ( E , On , 𝐴 ) = 𝐴 )
8 7 reseq2d ( 𝐴 ∈ On → ( 𝐹 ↾ Pred ( E , On , 𝐴 ) ) = ( 𝐹𝐴 ) )
9 8 fveq2d ( 𝐴 ∈ On → ( 𝐺 ‘ ( 𝐹 ↾ Pred ( E , On , 𝐴 ) ) ) = ( 𝐺 ‘ ( 𝐹𝐴 ) ) )
10 6 9 eqtrd ( 𝐴 ∈ On → ( 𝐹𝐴 ) = ( 𝐺 ‘ ( 𝐹𝐴 ) ) )