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=\mathrm{recs}\left(G\right)$$
Assertion	tfr1ALT	$$⊢FFn\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		tfrALT.1	$$⊢F=\mathrm{recs}\left(G\right)$$
2		epweon	$$⊢\mathrm{E}\mathrm{We}\mathrm{On}$$
3		epse	$$⊢\mathrm{E}\mathrm{Se}\mathrm{On}$$
4		df-recs	$$⊢\mathrm{recs}\left(G\right)=\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},G\right)$$
5	1 4	eqtri	$$⊢F=\mathrm{wrecs}\left(\mathrm{E},\mathrm{On},G\right)$$
6	5	wfr1	$$⊢\left(\mathrm{E}\mathrm{We}\mathrm{On}\wedge \mathrm{E}\mathrm{Se}\mathrm{On}\right)\to FFn\mathrm{On}$$
7	2 3 6	mp2an	$$⊢FFn\mathrm{On}$$