Metamath Proof Explorer


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 R1 On

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 E Fr 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 E Fr R1 On