Theorem wffr

Description: The class of well-founded sets is well-founded. Lemma I.9.24(2) of Kunen2 p. 53. (Contributed by Eric Schmidt, 11-Oct-2025)

	Ref	Expression
Assertion	wffr	$$⊢\mathrm{E}\mathrm{Fr}\bigcup R_1\left[\mathrm{On}\right]$$

Proof

Step	Hyp	Ref	Expression
1		rankrelp	Could not format rank RelPres _E , _E ( U. ( R1 " On ) , On ) : No typesetting found for |- rank RelPres _E , _E ( U. ( R1 " On ) , On ) with typecode |-
2		onfr	$$⊢\mathrm{E}\mathrm{Fr}\mathrm{On}$$
3		relpfr	Could not format ( rank RelPres _E , _E ( U. ( R1 " On ) , On ) -> ( _E Fr On -> _E Fr U. ( R1 " On ) ) ) : No typesetting found for |- ( rank RelPres _E , _E ( U. ( R1 " On ) , On ) -> ( _E Fr On -> _E Fr U. ( R1 " On ) ) ) with typecode |-
4	1 2 3	mp2	$$⊢\mathrm{E}\mathrm{Fr}\bigcup R_1\left[\mathrm{On}\right]$$