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 F=recsG
Assertion tfr2ALT AOnFA=GFA

Proof

Step Hyp Ref Expression
1 tfrALT.1 F=recsG
2 epweon EWeOn
3 epse ESeOn
4 df-recs recsG=wrecsEOnG
5 1 4 eqtri F=wrecsEOnG
6 5 wfr2 EWeOnESeOnAOnFA=GFPredEOnA
7 2 3 6 mpanl12 AOnFA=GFPredEOnA
8 predon AOnPredEOnA=A
9 8 reseq2d AOnFPredEOnA=FA
10 9 fveq2d AOnGFPredEOnA=GFA
11 7 10 eqtrd AOnFA=GFA