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	5	wfr2	$⊢ ((E We On \land E Se On) \land A \in On) \to F (A) = G ({F ↾}_{Pred (E, On, A)})$
7	2 3 6	mpanl12	$⊢ A \in On \to F (A) = G ({F ↾}_{Pred (E, On, A)})$
8		predon	$⊢ A \in On \to Pred (E, On, A) = A$
9	8	reseq2d	$⊢ A \in On \to {F ↾}_{Pred (E, On, A)} = {F ↾}_{A}$
10	9	fveq2d	$⊢ A \in On \to G ({F ↾}_{Pred (E, On, A)}) = G ({F ↾}_{A})$
11	7 10	eqtrd	$⊢ A \in On \to F (A) = G ({F ↾}_{A})$