Metamath Proof Explorer

Theorem tfr3ALT

Description: Alternate proof of tfr3 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	tfr3ALT	$⊢ (B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B = F$

Proof

Step	Hyp	Ref	Expression
1		tfrALT.1	$⊢ F = recs (G)$
2		predon	$⊢ x \in On \to Pred (E, On, x) = x$
3	2	reseq2d	$⊢ x \in On \to {B ↾}_{Pred (E, On, x)} = {B ↾}_{x}$
4	3	fveq2d	$⊢ x \in On \to G ({B ↾}_{Pred (E, On, x)}) = G ({B ↾}_{x})$
5	4	eqeq2d	$⊢ x \in On \to (B (x) = G ({B ↾}_{Pred (E, On, x)}) \leftrightarrow B (x) = G ({B ↾}_{x}))$
6	5	ralbiia	$⊢ \forall x \in On B (x) = G ({B ↾}_{Pred (E, On, x)}) \leftrightarrow \forall x \in On B (x) = G ({B ↾}_{x})$
7		epweon	$⊢ E We On$
8		epse	$⊢ E Se On$
9		df-recs	$⊢ recs (G) = wrecs (E, On, G)$
10	1 9	eqtri	$⊢ F = wrecs (E, On, G)$
11	10	wfr3	$⊢ ((E We On \land E Se On) \land (B Fn On \land \forall x \in On B (x) = G ({B ↾}_{Pred (E, On, x)}))) \to F = B$
12	7 8 11	mpanl12	$⊢ (B Fn On \land \forall x \in On B (x) = G ({B ↾}_{Pred (E, On, x)})) \to F = B$
13	6 12	sylan2br	$⊢ (B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to F = B$
14	13	eqcomd	$⊢ (B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B = F$