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	⊢ E Fr ∪ ( 𝑅1 “ On )

Proof

Step	Hyp	Ref	Expression
1		rankrelp	⊢ rank RelPres E , E ( ∪ ( 𝑅1 “ On ) , On )
2		onfr	⊢ E Fr On
3		relpfr	⊢ ( rank RelPres E , E ( ∪ ( 𝑅1 “ On ) , On ) → ( E Fr On → E Fr ∪ ( 𝑅1 “ On ) ) )
4	1 2 3	mp2	⊢ E Fr ∪ ( 𝑅1 “ On )