Metamath Proof Explorer

Theorem tfr1ALT

Description: Alternate proof of tfr1 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	tfr1ALT	$⊢ F Fn On$

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	wfr1	$⊢ (E We On \land E Se On) \to F Fn On$
7	2 3 6	mp2an	$⊢ F Fn On$