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	5	wfr2	⊢ ( ( ( E We On ∧ E Se On ) ∧ 𝐴 ∈ On ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( E , On , 𝐴 ) ) ) )
7	2 3 6	mpanl12	⊢ ( 𝐴 ∈ On → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( E , On , 𝐴 ) ) ) )
8		predon	⊢ ( 𝐴 ∈ On → Pred ( E , On , 𝐴 ) = 𝐴 )
9	8	reseq2d	⊢ ( 𝐴 ∈ On → ( 𝐹 ↾ Pred ( E , On , 𝐴 ) ) = ( 𝐹 ↾ 𝐴 ) )
10	9	fveq2d	⊢ ( 𝐴 ∈ On → ( 𝐺 ‘ ( 𝐹 ↾ Pred ( E , On , 𝐴 ) ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐴 ) ) )
11	7 10	eqtrd	⊢ ( 𝐴 ∈ On → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐴 ) ) )