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 = recs (G)$
	Assertion	tfr2ALT	$⊢ A \in On \to F (A) = G ({F ↾}_{A})$

Proof

Step	Hyp	Ref	Expression
1		tfrALT.1	$⊢ F = recs (G)$
2		epweon	$⊢ E We On$
3		epse	$⊢ E Se On$
4		df-recs	$⊢ recs (G) = wrecs (E, On, G)$
5	1 4	eqtri	$⊢ F = wrecs (E, On, G)$
6	2 3 5	wfr2	$⊢ A \in On \to F (A) = G ({F ↾}_{Pred (E, On, A)})$
7		predon	$⊢ A \in On \to Pred (E, On, A) = A$
8	7	reseq2d	$⊢ A \in On \to {F ↾}_{Pred (E, On, A)} = {F ↾}_{A}$
9	8	fveq2d	$⊢ A \in On \to G ({F ↾}_{Pred (E, On, A)}) = G ({F ↾}_{A})$
10	6 9	eqtrd	$⊢ A \in On \to F (A) = G ({F ↾}_{A})$